diff options
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 1 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pre.v | 3 | ||||
| -rw-r--r-- | src/MxDHRepChange.v | 9 | ||||
| -rw-r--r-- | src/NewBaseSystem.v | 4 | ||||
| -rw-r--r-- | src/Tactics/VerdiTactics.v | 122 | ||||
| -rw-r--r-- | src/Util/AdditionChainExponentiation.v | 2 | ||||
| -rw-r--r-- | src/Util/ListUtil.v | 42 | ||||
| -rw-r--r-- | src/Util/NumTheoryUtil.v | 4 | ||||
| -rw-r--r-- | src/Util/ZUtil.v | 1 |
9 files changed, 91 insertions, 97 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index aba07fb46..d5fa958b4 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -3,7 +3,6 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Algebra Crypto.Algebra Crypto.Util.Decidable. Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Coq.Logic.Eqdep_dec. -Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.Classes.Morphisms. Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tuple Crypto.Util.Notations. diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 7320b16bf..c8b5a9740 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -1,7 +1,6 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Numbers.BinNums Coq.ZArith.Zdiv Coq.ZArith.Znumtheory. Require Import Coq.Logic.Eqdep_dec. Require Import Coq.Logic.EqdepFacts. -Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.omega.Omega. Require Import Crypto.Util.NumTheoryUtil. Require Import Crypto.Tactics.VerdiTactics. @@ -138,4 +137,4 @@ Next Obligation. replace (Z.succ (m - 2)) with (m-1) by omega. rewrite (Zmod_small 1) by omega. apply (fermat_little m Hm a Ha). -Qed. +Qed.
\ No newline at end of file diff --git a/src/MxDHRepChange.v b/src/MxDHRepChange.v index 995c11409..ef2d06f5f 100644 --- a/src/MxDHRepChange.v +++ b/src/MxDHRepChange.v @@ -1,6 +1,6 @@ Require Import Crypto.Spec.MxDH. Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.Ring Crypto.Algebra.Field. -Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tuple Crypto.Util.Prod. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.BreakMatch. @@ -121,7 +121,7 @@ Section MxDHRepChange. Proper (loopiter_eq ==> eq ==> loopiter_eq) (loopiter K Kzero Kone Kadd Ksub Kmul Kinv Ka24 Kcswap a b c). Proof using Kcswap_correct Keq_dec impl_field. unfold loopiter; intros [? ?] [? ?] [[[] []] ?]; repeat intro ; cbv [fst snd] in * |-; subst. - repeat VerdiTactics.break_match; subst; repeat (VerdiTactics.find_injection; intros; subst). + repeat (break_match; break_match_hyps). split; [|reflexivity]. etransitivity; [|etransitivity]; [ | eapply Proper_ladderstep | ]; [eapply eq_subrelation; [ exact _ | symmetry; eassumption ] @@ -129,8 +129,7 @@ Section MxDHRepChange. | eapply eq_subrelation; [exact _ | eassumption ] ]; rewrite !Kcswap_correct in *; match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end; - repeat (VerdiTactics.find_injection; intros; subst); - split; simpl; eauto. + destruct_head prod; inversion_prod; subst; eauto. Qed. Lemma MxDHRepChange b (x:F) : @@ -152,7 +151,7 @@ Section MxDHRepChange. { destruct_head' prod; destruct Hrel as [[[] []] ?]; simpl in *; subst. rewrite !Fcswap_correct, !Kcswap_correct in *. match goal with [H: (if ?b then _ else _) = _ |- _] => destruct b end; - repeat (VerdiTactics.find_injection; intros; subst); + destruct_head prod; inversion_prod; subst; repeat match goal with [H: Keq (FtoK ?x) (?kx)|- _ ] => rewrite <- H end; t. } diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index 4dec23846..4611cf6ed 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -244,7 +244,6 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.omega.Omega. Require Import Coq.ZArith.BinIntDef. Local Open Scope Z_scope. -Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Tactics.Algebra_syntax.Nsatz. Require Import Crypto.Util.Decidable Crypto.Util.LetIn. Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil Crypto.Util.Sigma. @@ -582,7 +581,8 @@ Module B. Proof using Type*. induction i; cbv [id]; simpl place_cps; break_match; autorewrite with cancel_pair; - try find_apply_lem_hyp Z_div_exact_full_2; nsatz || auto. + try match goal with [H:_|-_] => apply Z_div_exact_full_2 in H end; + nsatz || auto. Qed. Definition from_associational_cps n (p:list limb) diff --git a/src/Tactics/VerdiTactics.v b/src/Tactics/VerdiTactics.v index 546acf10e..4060fc675 100644 --- a/src/Tactics/VerdiTactics.v +++ b/src/Tactics/VerdiTactics.v @@ -26,17 +26,17 @@ THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) -Ltac subst_max := +Ltac subst_max := idtac "VerdiTactics is deprecated in fiat-crypto"; repeat match goal with | [ H : ?X = _ |- _ ] => subst X | [H : _ = ?X |- _] => subst X end. -Ltac inv H := inversion H; subst_max. -Ltac invc H := inv H; clear H. -Ltac invcs H := invc H; simpl in *. +Ltac inv H := idtac "VerdiTactics is deprecated in fiat-crypto"; inversion H; subst_max. +Ltac invc H := idtac "VerdiTactics is deprecated in fiat-crypto"; inv H; clear H. +Ltac invcs H := idtac "VerdiTactics is deprecated in fiat-crypto"; invc H; simpl in *. -Ltac break_if := +Ltac break_if := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ |- context [ if ?X then _ else _ ] ] => match type of X with @@ -50,7 +50,7 @@ Ltac break_if := end end. -Ltac break_match_hyp := +Ltac break_match_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : context [ match ?X with _ => _ end ] |- _] => match type of X with @@ -59,7 +59,7 @@ Ltac break_match_hyp := end end. -Ltac break_match_goal := +Ltac break_match_goal := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ |- context [ match ?X with _ => _ end ] ] => match type of X with @@ -68,66 +68,66 @@ Ltac break_match_goal := end end. -Ltac break_match := break_match_goal || break_match_hyp. +Ltac break_match := idtac "VerdiTactics is deprecated in fiat-crypto"; break_match_goal || break_match_hyp. -Ltac break_exists := +Ltac break_exists := idtac "VerdiTactics is deprecated in fiat-crypto"; repeat match goal with | [H : exists _, _ |- _ ] => destruct H end. -Ltac break_exists_exists := +Ltac break_exists_exists := idtac "VerdiTactics is deprecated in fiat-crypto"; repeat match goal with | H:exists _, _ |- _ => let x := fresh "x" in destruct H as [x]; exists x end. -Ltac break_and := +Ltac break_and := idtac "VerdiTactics is deprecated in fiat-crypto"; repeat match goal with | [H : _ /\ _ |- _ ] => destruct H end. -Ltac solve_by_inversion' tac := +Ltac solve_by_inversion' tac := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [H : _ |- _] => solve [inv H; tac] end. -Ltac solve_by_inversion := solve_by_inversion' auto. +Ltac solve_by_inversion := idtac "VerdiTactics is deprecated in fiat-crypto"; solve_by_inversion' auto. -Ltac apply_fun f H:= +Ltac apply_fun f H:= idtac "VerdiTactics is deprecated in fiat-crypto"; match type of H with | ?X = ?Y => assert (f X = f Y) end. -Ltac conclude H tac := +Ltac conclude H tac := idtac "VerdiTactics is deprecated in fiat-crypto"; (let H' := fresh in match type of H with | ?P -> _ => assert P as H' by (tac) end; specialize (H H'); clear H'). -Ltac concludes := +Ltac concludes := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?P -> _ |- _ ] => conclude H auto end. -Ltac forward H := +Ltac forward H := idtac "VerdiTactics is deprecated in fiat-crypto"; let H' := fresh in match type of H with | ?P -> _ => assert P as H' end. -Ltac forwards := +Ltac forwards := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?P -> _ |- _ ] => forward H end. -Ltac find_contradiction := +Ltac find_contradiction := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?X = _, H' : ?X = _ |- _ ] => rewrite H in H'; solve_by_inversion end. -Ltac find_rewrite := +Ltac find_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?X _ _ _ _ = _, H' : ?X _ _ _ _ = _ |- _ ] => rewrite H in H' | [ H : ?X = _, H' : ?X = _ |- _ ] => rewrite H in H' @@ -135,31 +135,31 @@ Ltac find_rewrite := | [ H : ?X = _ |- context [ ?X ] ] => rewrite H end. -Ltac find_rewrite_lem lem := +Ltac find_rewrite_lem lem := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _ ] => rewrite lem in H; [idtac] end. -Ltac find_rewrite_lem_by lem t := +Ltac find_rewrite_lem_by lem t := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _ ] => rewrite lem in H by t end. -Ltac find_erewrite_lem lem := +Ltac find_erewrite_lem lem := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _] => erewrite lem in H by eauto end. -Ltac find_reverse_rewrite := +Ltac find_reverse_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ = ?X _ _ _ _, H' : ?X _ _ _ _ = _ |- _ ] => rewrite <- H in H' | [ H : _ = ?X, H' : context [ ?X ] |- _ ] => rewrite <- H in H' | [ H : _ = ?X |- context [ ?X ] ] => rewrite <- H end. -Ltac find_inversion := +Ltac find_inversion := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?X _ _ _ _ _ _ = ?X _ _ _ _ _ _ |- _ ] => invc H | [ H : ?X _ _ _ _ _ = ?X _ _ _ _ _ |- _ ] => invc H @@ -169,7 +169,7 @@ Ltac find_inversion := | [ H : ?X _ = ?X _ |- _ ] => invc H end. -Ltac prove_eq := +Ltac prove_eq := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?X ?x1 ?x2 ?x3 = ?X ?y1 ?y2 ?y3 |- _ ] => assert (x1 = y1) by congruence; @@ -185,75 +185,75 @@ Ltac prove_eq := clear H end. -Ltac tuple_inversion := +Ltac tuple_inversion := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : (_, _, _, _) = (_, _, _, _) |- _ ] => invc H | [ H : (_, _, _) = (_, _, _) |- _ ] => invc H | [ H : (_, _) = (_, _) |- _ ] => invc H end. -Ltac f_apply H f := +Ltac f_apply H f := idtac "VerdiTactics is deprecated in fiat-crypto"; match type of H with | ?X = ?Y => assert (f X = f Y) by (rewrite H; auto) end. -Ltac break_let := +Ltac break_let := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : context [ (let (_,_) := ?X in _) ] |- _ ] => destruct X eqn:? | [ |- context [ (let (_,_) := ?X in _) ] ] => destruct X eqn:? end. -Ltac break_or_hyp := +Ltac break_or_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ \/ _ |- _ ] => invc H end. -Ltac copy_apply lem H := +Ltac copy_apply lem H := idtac "VerdiTactics is deprecated in fiat-crypto"; let x := fresh in pose proof H as x; apply lem in x. -Ltac copy_eapply lem H := +Ltac copy_eapply lem H := idtac "VerdiTactics is deprecated in fiat-crypto"; let x := fresh in pose proof H as x; eapply lem in x. -Ltac conclude_using tac := +Ltac conclude_using tac := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?P -> _ |- _ ] => conclude H tac end. -Ltac find_higher_order_rewrite := +Ltac find_higher_order_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ = _ |- _ ] => rewrite H in * | [ H : forall _, _ = _ |- _ ] => rewrite H in * | [ H : forall _ _, _ = _ |- _ ] => rewrite H in * end. -Ltac find_reverse_higher_order_rewrite := +Ltac find_reverse_higher_order_rewrite := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ = _ |- _ ] => rewrite <- H in * | [ H : forall _, _ = _ |- _ ] => rewrite <- H in * | [ H : forall _ _, _ = _ |- _ ] => rewrite <- H in * end. -Ltac clean := +Ltac clean := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?X = ?X |- _ ] => clear H end. -Ltac find_apply_hyp_goal := +Ltac find_apply_hyp_goal := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _ ] => solve [apply H] end. -Ltac find_copy_apply_lem_hyp lem := +Ltac find_copy_apply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _ ] => copy_apply lem H end. -Ltac find_apply_hyp_hyp := +Ltac find_apply_hyp_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : forall _, _ -> _, H' : _ |- _ ] => @@ -262,7 +262,7 @@ Ltac find_apply_hyp_hyp := apply H in H'; auto; [idtac] end. -Ltac find_copy_apply_hyp_hyp := +Ltac find_copy_apply_hyp_hyp := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : forall _, _ -> _, H' : _ |- _ ] => @@ -271,17 +271,17 @@ Ltac find_copy_apply_hyp_hyp := copy_apply H H'; auto; [idtac] end. -Ltac find_apply_lem_hyp lem := +Ltac find_apply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _ ] => apply lem in H end. -Ltac find_eapply_lem_hyp lem := +Ltac find_eapply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _ ] => eapply lem in H end. -Ltac insterU H := +Ltac insterU H := idtac "VerdiTactics is deprecated in fiat-crypto"; match type of H with | forall _ : ?T, _ => let x := fresh "x" in @@ -290,18 +290,18 @@ Ltac insterU H := clear x; specialize (H x') end. -Ltac find_insterU := +Ltac find_insterU := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : forall _, _ |- _ ] => insterU H end. -Ltac eapply_prop P := +Ltac eapply_prop P := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | H : P _ |- _ => eapply H end. -Ltac isVar t := +Ltac isVar t := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | v : _ |- _ => match t with @@ -309,15 +309,15 @@ Ltac isVar t := end end. -Ltac remGen t := +Ltac remGen t := idtac "VerdiTactics is deprecated in fiat-crypto"; let x := fresh in let H := fresh in remember t as x eqn:H; generalize dependent H. -Ltac remGenIfNotVar t := first [isVar t| remGen t]. +Ltac remGenIfNotVar t := idtac "VerdiTactics is deprecated in fiat-crypto"; first [isVar t| remGen t]. -Ltac rememberNonVars H := +Ltac rememberNonVars H := idtac "VerdiTactics is deprecated in fiat-crypto"; match type of H with | _ ?a ?b ?c ?d ?e => remGenIfNotVar a; @@ -341,7 +341,7 @@ Ltac rememberNonVars H := remGenIfNotVar a end. -Ltac generalizeEverythingElse H := +Ltac generalizeEverythingElse H := idtac "VerdiTactics is deprecated in fiat-crypto"; repeat match goal with | [ x : ?T |- _ ] => first [ @@ -354,48 +354,48 @@ Ltac generalizeEverythingElse H := revert x] end. -Ltac prep_induction H := +Ltac prep_induction H := idtac "VerdiTactics is deprecated in fiat-crypto"; rememberNonVars H; generalizeEverythingElse H. -Ltac econcludes := +Ltac econcludes := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?P -> _ |- _ ] => conclude H eauto end. -Ltac find_copy_eapply_lem_hyp lem := +Ltac find_copy_eapply_lem_hyp lem := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : _ |- _ ] => copy_eapply lem H end. -Ltac apply_prop_hyp P Q := +Ltac apply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : context [ P ], H' : context [ Q ] |- _ ] => apply H in H' end. -Ltac eapply_prop_hyp P Q := +Ltac eapply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : context [ P ], H' : context [ Q ] |- _ ] => eapply H in H' end. -Ltac copy_eapply_prop_hyp P Q := +Ltac copy_eapply_prop_hyp P Q := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : context [ P ], H' : context [ Q ] |- _ ] => copy_eapply H H' end. -Ltac find_false := +Ltac find_false := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | H : _ -> False |- _ => exfalso; apply H end. -Ltac injc H := +Ltac injc H := idtac "VerdiTactics is deprecated in fiat-crypto"; injection H; clear H; intro; subst_max. -Ltac find_injection := +Ltac find_injection := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : ?X _ _ _ _ _ _ = ?X _ _ _ _ _ _ |- _ ] => injc H | [ H : ?X _ _ _ _ _ = ?X _ _ _ _ _ |- _ ] => injc H @@ -405,10 +405,10 @@ Ltac find_injection := | [ H : ?X _ = ?X _ |- _ ] => injc H end. -Ltac aggresive_rewrite_goal := +Ltac aggresive_rewrite_goal := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with H : _ |- _ => rewrite H end. -Ltac break_exists_name x := +Ltac break_exists_name x := idtac "VerdiTactics is deprecated in fiat-crypto"; match goal with | [ H : exists _, _ |- _ ] => destruct H as [x H] end. diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index fc082a54a..110a756ea 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -2,8 +2,8 @@ Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations. Require Import Coq.Numbers.BinNums Coq.NArith.BinNat. Require Import Crypto.Util.ListUtil. Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. -Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.Option. +Require Import Crypto.Util.Tactics.BreakMatch. Section AddChainExp. Function fold_chain {T} (id:T) (op:T->T->T) (is:list (nat*nat)) (acc:list T) {struct is} : T := diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 32c6dbdf7..a9987ffde 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1,11 +1,12 @@ Require Import Coq.Lists.List. -Require Import Coq.omega.Omega. +Require Import Coq.omega.Omega Lia. Require Import Coq.Arith.Peano_dec. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.Util.NatUtil. Require Export Crypto.Util.FixCoqMistakes. +Require Export Crypto.Util.Tactics.BreakMatch. +Require Export Crypto.Util.Tactics.DestructHead. Create HintDb distr_length discriminated. Create HintDb simpl_set_nth discriminated. @@ -552,8 +553,7 @@ Lemma splice_nth_equiv_update_nth : forall {T} n f d (xs:list T), then update_nth n f xs else xs ++ (f d)::nil. Proof. - induction n, xs; boring_list. - do 2 break_if; auto; omega. + induction n, xs; boring_list; break_match; auto; omega. Qed. Lemma splice_nth_equiv_update_nth_update : forall {T} n f d (xs:list T), @@ -561,8 +561,7 @@ Lemma splice_nth_equiv_update_nth_update : forall {T} n f d (xs:list T), splice_nth n (f (nth_default d xs n)) xs = update_nth n f xs. Proof. intros. - rewrite splice_nth_equiv_update_nth. - break_if; auto; omega. + rewrite splice_nth_equiv_update_nth; break_match; auto; omega. Qed. Lemma splice_nth_equiv_update_nth_snoc : forall {T} n f d (xs:list T), @@ -570,8 +569,7 @@ Lemma splice_nth_equiv_update_nth_snoc : forall {T} n f d (xs:list T), splice_nth n (f (nth_default d xs n)) xs = xs ++ (f d)::nil. Proof. intros. - rewrite splice_nth_equiv_update_nth. - break_if; auto; omega. + rewrite splice_nth_equiv_update_nth; break_match; auto; omega. Qed. Definition IMPOSSIBLE {T} : list T. exact nil. Qed. @@ -688,7 +686,7 @@ Qed. Lemma In_nth_error_value : forall {T} xs (x:T), In x xs -> exists n, nth_error xs n = Some x. Proof. - induction xs; nth_tac; break_or_hyp. + induction xs; nth_tac; destruct_head or; subst. - exists 0; reflexivity. - edestruct IHxs; eauto. exists (S x0). eauto. Qed. @@ -1115,11 +1113,11 @@ Hint Resolve @nth_default_in_bounds : simpl_nth_default. Lemma cons_eq_head : forall {T} (x y:T) xs ys, x::xs = y::ys -> x=y. Proof. - intros; solve_by_inversion. + intros; congruence. Qed. Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys. Proof. - intros; solve_by_inversion. + intros; congruence. Qed. Lemma map_nth_default_always {A B} (f : A -> B) (n : nat) (x : A) (l : list A) @@ -1238,8 +1236,8 @@ Lemma update_nth_nth_default_full : forall {A} (d:A) n f l i, else d. Proof. induction n; (destruct l; simpl in *; [ intros; destruct i; simpl; try reflexivity; omega | ]); - intros; repeat break_if; subst; try destruct i; - repeat first [ progress break_if + intros; repeat break_match; subst; try destruct i; + repeat first [ progress break_match | progress subst | progress boring | progress autorewrite with simpl_nth_default @@ -1251,7 +1249,7 @@ Hint Rewrite @update_nth_nth_default_full : push_nth_default. Lemma update_nth_nth_default : forall {A} (d:A) n f l i, (0 <= i < length l)%nat -> nth_default d (update_nth n f l) i = if (eq_nat_dec i n) then f (nth_default d l i) else nth_default d l i. -Proof. intros; rewrite update_nth_nth_default_full; repeat break_if; boring. Qed. +Proof. intros; rewrite update_nth_nth_default_full; repeat break_match; boring. Qed. Hint Rewrite @update_nth_nth_default using (omega || distr_length; omega) : push_nth_default. @@ -1527,23 +1525,23 @@ Proof. induction ls1, ls2. + cbv [map2 length min]. intros. - break_if; try omega. + break_match; try omega. apply nth_default_nil. + cbv [map2 length min]. intros. - break_if; try omega. + break_match; try omega. apply nth_default_nil. + cbv [map2 length min]. intros. - break_if; try omega. + break_match; try omega. apply nth_default_nil. + simpl. destruct i. - intros. rewrite !nth_default_cons. - break_if; auto; omega. + break_match; auto; omega. - intros. rewrite !nth_default_cons_S. rewrite IHls1 with (d1 := d1) (d2 := d2). - repeat break_if; auto; omega. + repeat break_match; auto; omega. Qed. Lemma map2_cons : forall A B C (f : A -> B -> C) ls1 ls2 a b, @@ -1655,15 +1653,15 @@ Lemma nth_default_firstn : forall {A} (d : A) l i n, then if lt_dec i n then nth_default d l i else d else nth_default d l i. Proof. - induction n; intros; break_if; autorewrite with push_nth_default; auto; try omega. + induction n; intros; break_match; autorewrite with push_nth_default; auto; try omega. + rewrite (firstn_succ d) by omega. - autorewrite with push_nth_default; repeat (break_if; distr_length); + autorewrite with push_nth_default; repeat (break_match_hyps; break_match; distr_length); rewrite Min.min_l in * by omega; try omega. - apply IHn; omega. - replace i with n in * by omega. rewrite Nat.sub_diag. autorewrite with push_nth_default; auto. - - rewrite nth_default_out_of_bounds; distr_length; auto. + + rewrite nth_default_out_of_bounds; break_match_hyps; distr_length; auto; lia. + rewrite firstn_all2 by omega. auto. Qed. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index 05ce4a0de..2ccb0455f 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -2,8 +2,8 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZAr Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil. Require Import Coqprime.Zp. -Require Import Crypto.Tactics.VerdiTactics. Require Export Crypto.Util.FixCoqMistakes. +Require Export Crypto.Util.Tactics. Local Open Scope Z. (* TODO: move somewhere else for lemmas about Coqprime? *) @@ -284,7 +284,7 @@ Proof. intros. destruct (Z.prime_odd_or_2 p prime_p); intuition. rewrite <- Zdiv2_div. - pose proof (Zdiv2_odd_eqn p); break_if; congruence || omega. + pose proof (Zdiv2_odd_eqn p); break_match; break_match_hyps; congruence || omega. Qed. Lemma minus1_square_1mod4 : forall (p : Z) (prime_p : prime p), diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 5e59daab9..91c350d9f 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -11,7 +11,6 @@ Require Import Crypto.Util.Bool. Require Import Crypto.Util.Notations. Require Import Coq.Lists.List. Require Export Crypto.Util.FixCoqMistakes. -(*Require Export Crypto.Tactics.VerdiTactics.*) Import Nat. Local Open Scope Z. |