From 5d7b2bc9a4e902d3c3aa7a3625ffda6eb127011f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Jul 2016 12:58:36 -0700 Subject: Revert "Add more ZUtil automation" This reverts commit 29bb3dd531be45ba7960b34ef759b44436e48905. [intuition] is stupid and terrible. Fix upcoming. --- src/Util/ZUtil.v | 15 +++------------ 1 file changed, 3 insertions(+), 12 deletions(-) diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 4032871c1..077ad25a8 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -27,24 +27,15 @@ Hint Rewrite Z.div_mul Z.div_1_l Z.div_same Z.mod_same Z.div_small Z.mod_small Z (** "push" means transform [-f x] to [f (-x)]; "pull" means go the other way *) Create HintDb push_Zopp discriminated. Create HintDb pull_Zopp discriminated. -Create HintDb push_Zpow discriminated. -Create HintDb pull_Zpow discriminated. -Create HintDb push_Zmul discriminated. -Create HintDb pull_Zmul discriminated. -Hint Extern 1 => autorewrite with push_Zopp in * : push_Zopp. -Hint Extern 1 => autorewrite with pull_Zopp in * : pull_Zopp. -Hint Extern 1 => autorewrite with push_Zpow in * : push_Zpow. -Hint Extern 1 => autorewrite with pull_Zpow in * : pull_Zpow. -Hint Extern 1 => autorewrite with push_Zmul in * : push_Zmul. -Hint Extern 1 => autorewrite with pull_Zmul in * : pull_Zmul. Hint Rewrite Z.div_opp_l_nz Z.div_opp_l_z using lia : pull_Zopp. Hint Rewrite Z.mul_opp_l : pull_Zopp. Hint Rewrite <- Z.opp_add_distr : pull_Zopp. Hint Rewrite <- Z.div_opp_l_nz Z.div_opp_l_z using lia : push_Zopp. Hint Rewrite <- Z.mul_opp_l : push_Zopp. Hint Rewrite Z.opp_add_distr : push_Zopp. -Hint Rewrite Z.pow_sub_r Z.pow_div_l using lia : push_Zpow. -Hint Rewrite <- Z.pow_sub_r Z.pow_div_l using lia : pull_Zpow. + +Create HintDb push_Zmul discriminated. +Create HintDb pull_Zmul discriminated. Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : push_Zmul. Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul. -- cgit v1.2.3 From 4519b114c66b184611068b2cc9bdad644f4a5a47 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 22 Jul 2016 13:45:17 -0700 Subject: Make the library 20% faster: [auto with *] is evil I do hereby revoke the privilege of [intuition] to grab random hints from random databases. This privilege is reserved for [debug_intuition], which comes with a warning about not being used in production code. This tactic is useful in conjunction with `Print Hint *`, to discover what hint databases the hints were grabbed from. (Suggestions for renaming [debug_intuition] welcome.) Any file using [intuition] must [Require Export Crypto.Util.FixCoqMistakes.]. It's possible we could lift this restriction by compiling [FixCoqMistakes] separately, and passing along `-require FixCoqMistakes` to Coq. Should we do this? After | File Name | Before || Change ------------------------------------------------------------------------------------ 3m29.54s | Total | 4m33.13s || -1m03.59s ------------------------------------------------------------------------------------ 0m03.75s | BaseSystemProofs | 0m43.84s || -0m40.09s 0m42.57s | CompleteEdwardsCurve/ExtendedCoordinates | 0m34.48s || +0m08.09s 0m03.04s | Util/ListUtil | 0m11.18s || -0m08.14s 0m01.62s | ModularArithmetic/PrimeFieldTheorems | 0m09.53s || -0m07.90s 0m00.87s | Util/NumTheoryUtil | 0m07.61s || -0m06.74s 0m01.61s | Encoding/PointEncodingPre | 0m06.93s || -0m05.31s 0m51.95s | Specific/GF25519 | 0m47.52s || +0m04.42s 0m12.30s | Experiments/SpecEd25519 | 0m11.29s || +0m01.01s 0m09.22s | Specific/GF1305 | 0m08.17s || +0m01.05s 0m03.48s | CompleteEdwardsCurve/Pre | 0m04.77s || -0m01.28s 0m02.70s | Assembly/State | 0m04.09s || -0m01.38s 0m01.55s | ModularArithmetic/ModularArithmeticTheorems | 0m02.93s || -0m01.38s 0m01.16s | Assembly/Pseudize | 0m02.34s || -0m01.17s 0m15.67s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m16.37s || -0m00.70s 0m06.02s | Algebra | 0m06.67s || -0m00.65s 0m05.90s | Experiments/GenericFieldPow | 0m06.68s || -0m00.77s 0m04.65s | WeierstrassCurve/Pre | 0m05.27s || -0m00.61s 0m03.93s | ModularArithmetic/Pow2BaseProofs | 0m03.94s || -0m00.00s 0m03.70s | ModularArithmetic/Tutorial | 0m03.85s || -0m00.14s 0m02.83s | ModularArithmetic/ModularBaseSystemOpt | 0m02.84s || -0m00.00s 0m02.74s | Experiments/EdDSARefinement | 0m01.80s || +0m00.94s 0m02.35s | Util/ZUtil | 0m02.51s || -0m00.15s 0m01.86s | Assembly/Wordize | 0m02.32s || -0m00.45s 0m01.23s | ModularArithmetic/ExtendedBaseVector | 0m01.20s || +0m00.03s 0m01.21s | BaseSystem | 0m01.63s || -0m00.41s 0m01.03s | Experiments/SpecificCurve25519 | 0m00.98s || +0m00.05s 0m01.01s | ModularArithmetic/ModularBaseSystemProofs | 0m01.11s || -0m00.10s 0m00.95s | ModularArithmetic/BarrettReduction/Z | 0m01.38s || -0m00.42s 0m00.92s | Experiments/DerivationsOptionRectLetInEncoding | 0m01.81s || -0m00.89s 0m00.85s | ModularArithmetic/ModularBaseSystemField | 0m00.86s || -0m00.01s 0m00.82s | ModularArithmetic/ModularBaseSystemListProofs | 0m00.79s || +0m00.02s 0m00.80s | Assembly/QhasmEvalCommon | 0m00.93s || -0m00.13s 0m00.73s | Spec/EdDSA | 0m00.59s || +0m00.14s 0m00.72s | Util/Tuple | 0m00.71s || +0m00.01s 0m00.70s | Util/IterAssocOp | 0m00.72s || -0m00.02s 0m00.67s | Encoding/ModularWordEncodingTheorems | 0m00.71s || -0m00.03s 0m00.66s | Assembly/Pipeline | 0m00.64s || +0m00.02s 0m00.65s | Testbit | 0m00.65s || +0m00.00s 0m00.65s | Assembly/PseudoConversion | 0m00.65s || +0m00.00s 0m00.64s | Util/AdditionChainExponentiation | 0m00.63s || +0m00.01s 0m00.63s | ModularArithmetic/ExtPow2BaseMulProofs | 0m00.64s || -0m00.01s 0m00.63s | Assembly/Pseudo | 0m00.65s || -0m00.02s 0m00.62s | ModularArithmetic/ModularBaseSystem | 0m00.57s || +0m00.05s 0m00.61s | ModularArithmetic/ModularBaseSystemList | 0m00.57s || +0m00.04s 0m00.60s | Encoding/ModularWordEncodingPre | 0m00.69s || -0m00.08s 0m00.60s | ModularArithmetic/PseudoMersenneBaseParamProofs | 0m00.59s || +0m00.01s 0m00.56s | Assembly/StringConversion | 0m00.56s || +0m00.00s 0m00.54s | Spec/ModularWordEncoding | 0m00.61s || -0m00.06s 0m00.54s | Assembly/QhasmUtil | 0m00.46s || +0m00.08s 0m00.52s | Assembly/Qhasm | 0m00.53s || -0m00.01s 0m00.48s | Assembly/AlmostQhasm | 0m00.52s || -0m00.04s 0m00.48s | ModularArithmetic/Pre | 0m00.48s || +0m00.00s 0m00.46s | Assembly/Vectorize | 0m00.72s || -0m00.25s 0m00.45s | Spec/WeierstrassCurve | 0m00.44s || +0m00.01s 0m00.44s | Assembly/AlmostConversion | 0m00.44s || +0m00.00s 0m00.43s | ModularArithmetic/Pow2Base | 0m00.51s || -0m00.08s 0m00.42s | ModularArithmetic/PseudoMersenneBaseParams | 0m00.38s || +0m00.03s 0m00.41s | Spec/CompleteEdwardsCurve | 0m00.43s || -0m00.02s 0m00.34s | Spec/ModularArithmetic | 0m00.36s || -0m00.01s 0m00.03s | Util/FixCoqMistakes | N/A || +0m00.03s 0m00.02s | Util/Notations | 0m00.04s || -0m00.02s 0m00.02s | Util/Tactics | 0m00.02s || +0m00.00s --- _CoqProject | 1 + src/Algebra.v | 1 + src/Assembly/Pseudize.v | 17 ++++---- src/Assembly/Pseudo.v | 12 ++--- src/Assembly/QhasmEvalCommon.v | 51 +++++++++++----------- src/Assembly/QhasmUtil.v | 13 +++--- src/Assembly/State.v | 32 +++++++------- src/Assembly/Vectorize.v | 6 ++- src/Assembly/Wordize.v | 20 +++++---- src/BaseSystem.v | 5 ++- .../CompleteEdwardsCurveTheorems.v | 5 ++- src/CompleteEdwardsCurve/ExtendedCoordinates.v | 3 +- src/Encoding/PointEncodingPre.v | 14 +++--- .../DerivationsOptionRectLetInEncoding.v | 15 ++++--- src/Experiments/GenericFieldPow.v | 1 + src/ModularArithmetic/ModularArithmeticTheorems.v | 9 +++- src/ModularArithmetic/ModularBaseSystemOpt.v | 3 +- src/ModularArithmetic/ModularBaseSystemProofs.v | 1 + src/ModularArithmetic/Pow2BaseProofs.v | 3 +- src/ModularArithmetic/Pre.v | 1 + src/ModularArithmetic/PrimeFieldTheorems.v | 1 + src/Util/FixCoqMistakes.v | 13 ++++++ src/Util/ListUtil.v | 7 +-- src/Util/Notations.v | 1 + src/Util/NumTheoryUtil.v | 1 + src/Util/Tactics.v | 1 + src/Util/Tuple.v | 3 +- src/Util/ZUtil.v | 9 ++-- 28 files changed, 148 insertions(+), 101 deletions(-) create mode 100644 src/Util/FixCoqMistakes.v diff --git a/_CoqProject b/_CoqProject index 187ea6541..f4a6f121b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -64,6 +64,7 @@ src/Tactics/Algebra_syntax/Nsatz.v src/Util/AdditionChainExponentiation.v src/Util/CaseUtil.v src/Util/Decidable.v +src/Util/FixCoqMistakes.v src/Util/IterAssocOp.v src/Util/ListUtil.v src/Util/NatUtil.v diff --git a/src/Algebra.v b/src/Algebra.v index 5a2ea19a4..f71807fff 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -5,6 +5,7 @@ Require Import Crypto.Util.Notations. Require Coq.Numbers.Natural.Peano.NPeano. Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope. Require Crypto.Tactics.Algebra_syntax.Nsatz. +Require Export Crypto.Util.FixCoqMistakes. Module Import ModuloCoq8485. Import NPeano Nat. diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v index c167dd6a1..ea14dc52e 100644 --- a/src/Assembly/Pseudize.v +++ b/src/Assembly/Pseudize.v @@ -1,7 +1,8 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith NPeano List Sumbool Compare_dec Omega. -Require Import QhasmCommon QhasmEvalCommon QhasmUtil Pseudo State. -Require Export Wordize Vectorize. +Require Import Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.Lists.List Coq.Bool.Sumbool Coq.Arith.Compare_dec Coq.omega.Omega. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.Pseudo Crypto.Assembly.State. +Require Export Crypto.Assembly.Wordize Crypto.Assembly.Vectorize. +Require Export Crypto.Util.FixCoqMistakes. Import Pseudo ListNotations StateCommon EvalUtil ListState. @@ -34,8 +35,8 @@ Section Conversion. replace (k mod n) with k by ( assert (n <> 0) as NZ by omega; pose proof (Nat.div_mod k n NZ); - replace (k mod n) with (k - n * (k / n)) by intuition; - rewrite (Nat.div_small k n); intuition). + replace (k mod n) with (k - n * (k / n)) by intuition auto with zarith; + rewrite (Nat.div_small k n); intuition auto with zarith). autounfold; simpl. destruct (nth_error x k); simpl; try inversion H0; intuition. @@ -48,8 +49,8 @@ Section Conversion. intros; autounfold; simpl. unfold indexize; destruct (le_dec n 0), (le_dec len 0); - try replace n with 0 in * by intuition; - try replace len with 0 in * by intuition; + try replace n with 0 in * by intuition auto with zarith; + try replace len with 0 in * by intuition auto with zarith; autounfold; simpl in *; rewrite H; autounfold; simpl; rewrite NToWord_wordToN; intuition. @@ -247,7 +248,7 @@ Section Conversion. simpl; intuition. Qed. - Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := + Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := {p: @Pseudo w s n m | forall x: (list (word w)), List.length x = n -> exists m' c', pseudoEval p (x, TripleM.empty N, None) = Some (f x, m', c')}. diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v index e3f1e63ff..b8aae4521 100644 --- a/src/Assembly/Pseudo.v +++ b/src/Assembly/Pseudo.v @@ -1,6 +1,7 @@ -Require Import QhasmCommon QhasmUtil State. -Require Import Language QhasmEvalCommon. -Require Import List Compare_dec Omega. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State. +Require Import Crypto.Assembly.Language Crypto.Assembly.QhasmEvalCommon. +Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.omega.Omega. +Require Export Crypto.Util.FixCoqMistakes. Module Pseudo <: Language. Import EvalUtil ListState. @@ -96,7 +97,7 @@ Module Pseudo <: Language. else pseudoEval r st )) | PFunExp n p e => - (fix funexpseudo (e': nat) (st': ListState w) := + (fix funexpseudo (e': nat) (st': ListState w) := match e' with | O => Some st' | S e'' => @@ -116,7 +117,7 @@ Module Pseudo <: Language. Definition indexize {n: nat} (x: nat): Index n. intros; destruct (le_dec n 0). - - exists 0; abstract intuition. + - exists 0; abstract intuition auto with zarith. - exists (x mod n)%nat; abstract ( pose proof (Nat.mod_bound_pos x n); omega). Defined. @@ -179,4 +180,3 @@ Module Pseudo <: Language. Close Scope pseudo_notations. End Pseudo. - diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v index 4c64d8681..9760dc869 100644 --- a/src/Assembly/QhasmEvalCommon.v +++ b/src/Assembly/QhasmEvalCommon.v @@ -1,7 +1,8 @@ -Require Import QhasmCommon QhasmUtil State. -Require Import ZArith Sumbool. +Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State. +Require Import Coq.ZArith.ZArith Coq.Bool.Sumbool. Require Import Bedrock.Word. -Require Import Logic.Eqdep_dec ProofIrrelevance. +Require Import Coq.Logic.Eqdep_dec Coq.Logic.ProofIrrelevance. +Require Export Crypto.Util.FixCoqMistakes. Module EvalUtil. Definition evalTest {n} (o: TestOp) (a b: word n): bool := @@ -78,13 +79,13 @@ Module EvalUtil. Proof. induction a; unfold getWidth; simpl; intuition. Qed. Lemma width_eq {n} (a b: Width n): a = b. - Proof. + Proof. assert (Some a = Some b) as H by ( replace (Some a) with (getWidth n) by (rewrite getWidth_eq; intuition); replace (Some b) with (getWidth n) by (rewrite getWidth_eq; intuition); intuition). inversion H; intuition. - Qed. + Qed. (* Mapping Conversions *) @@ -102,29 +103,29 @@ Module EvalUtil. Definition mapping_dec {n} (a b: Mapping n): {a = b} + {a <> b}. refine (match (a, b) as p' return (a, b) = p' -> _ with - | (regM v, regM v') => fun _ => + | (regM v, regM v') => fun _ => if (Nat.eq_dec (regName v) (regName v')) then left _ else right _ - | (stackM v, stackM v') => fun _ => + | (stackM v, stackM v') => fun _ => if (Nat.eq_dec (stackName v) (stackName v')) then left _ else right _ - | (constM v, constM v') => fun _ => + | (constM v, constM v') => fun _ => if (Nat.eq_dec (constValueN v) (constValueN v')) then left _ else right _ - | (memM _ v i, memM _ v' i') => fun _ => - if (Nat.eq_dec (memName v) (memName v')) + | (memM _ v i, memM _ v' i') => fun _ => + if (Nat.eq_dec (memName v) (memName v')) then if (Nat.eq_dec (memLength v) (memLength v')) then if (Nat.eq_dec (proj1_sig i) (proj1_sig i')) then left _ else right _ else right _ else right _ | _ => fun _ => right _ - end (eq_refl (a, b))); + end (eq_refl (a, b))); try destruct v, v'; subst; unfold regName, stackName, constValueN, memName, memLength in *; repeat progress (try apply f_equal; subst; match goal with @@ -158,10 +159,10 @@ Module EvalUtil. | [ H: proj1_sig ?a <> proj1_sig ?b |- _ ] => let l0 := fresh in let l1 := fresh in destruct a, b; simpl in H; subst - | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => + | [ H: existT ?a ?b _ = existT ?a ?b _ |- _ ] => apply (inj_pair2_eq_dec _ Nat.eq_dec) in H; subst; intuition - | [ H: exist _ _ _ = exist _ _ _ |- _ ] => + | [ H: exist _ _ _ = exist _ _ _ |- _ ] => inversion H; subst; intuition (* Single specialized wordToNat proof *) @@ -176,12 +177,12 @@ Module EvalUtil. Definition dec_lt (a b: nat): {(a < b)%nat} + {(a >= b)%nat}. assert ({(a true}) - by abstract (destruct (a if (Nat.eq_dec O (wordToNat v)) then Some true - else Some false) + else Some false) | CReg n o a b => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => Some (evalTest o va vb))) - | CConst n o a c => + | CConst n o a c => omap (getReg a state) (fun va => Some (evalTest o va (constValueW c))) end. @@ -245,35 +246,35 @@ Module QhasmEval. let (v', co) := (evalIntOp o va vb) in Some (setCarryOpt co (setReg a v' state)))) - | IOpMem _ _ o r m i => + | IOpMem _ _ o r m i => omap (getReg r state) (fun va => omap (getMem m i state) (fun vb => let (v', co) := (evalIntOp o va vb) in Some (setCarryOpt co (setReg r v' state)))) - | DOp _ o a b (Some x) => + | DOp _ o a b (Some x) => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => let (low, high) := (evalDualOp o va vb) in Some (setReg x high (setReg a low state)))) - | DOp _ o a b None => + | DOp _ o a b None => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => let (low, high) := (evalDualOp o va vb) in Some (setReg a low state))) - | ROp _ o r i => + | ROp _ o r i => omap (getReg r state) (fun v => let v' := (evalRotOp o v i) in Some (setReg r v' state)) - | COp _ o a b => + | COp _ o a b => omap (getReg a state) (fun va => omap (getReg b state) (fun vb => match (getCarry state) with | None => None - | Some c0 => + | Some c0 => let (v', c') := (evalCarryOp o va vb c0) in Some (setCarry c' (setReg a v' state)) end)) @@ -281,7 +282,7 @@ Module QhasmEval. Definition evalAssignment (a: Assignment) (state: State): option State := match a with - | ARegMem _ _ r m i => + | ARegMem _ _ r m i => omap (getMem m i state) (fun v => Some (setReg r v state)) | AMemReg _ _ m i r => omap (getReg r state) (fun v => Some (setMem m i v state)) @@ -289,7 +290,7 @@ Module QhasmEval. omap (getReg b state) (fun v => Some (setStack a v state)) | ARegStack _ a b => omap (getStack b state) (fun v => Some (setReg a v state)) - | ARegReg _ a b => + | ARegReg _ a b => omap (getReg b state) (fun v => Some (setReg a v state)) | AConstInt _ r c => Some (setReg r (constValueW c) state) diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index acf2b5c31..1ab894e94 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -1,6 +1,7 @@ -Require Import ZArith NArith NPeano. -Require Import QhasmCommon. +Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano. +Require Import Crypto.Assembly.QhasmCommon. Require Export Bedrock.Word. +Require Export Crypto.Util.FixCoqMistakes. Delimit Scope nword_scope with w. Local Open Scope nword_scope. @@ -14,12 +15,12 @@ Section Util. Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k. refine (split1 k (n - k) (convS w _)). - abstract (replace n with (k + (n - k)) by omega; intuition). + abstract (replace n with (k + (n - k)) by omega; intuition auto with arith). Defined. Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k. refine (split2 (n - k) k (convS w _)). - abstract (replace n with (k + (n - k)) by omega; intuition). + abstract (replace n with (k + (n - k)) by omega; intuition auto with zarith). Defined. Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n. @@ -61,7 +62,7 @@ Section Util. refine match (le_dec m n) with | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x)) | right p => (extend _ x, _) - end; try abstract intuition. + end; try abstract intuition auto with zarith. replace (n - m) with O by abstract omega; exact WO. Defined. @@ -75,4 +76,4 @@ Section Util. Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity). End Util. -Close Scope nword_scope. \ No newline at end of file +Close Scope nword_scope. diff --git a/src/Assembly/State.v b/src/Assembly/State.v index 8602c7f96..3467a5cad 100644 --- a/src/Assembly/State.v +++ b/src/Assembly/State.v @@ -1,12 +1,14 @@ -Require Export String List Logic. +Require Export Coq.Strings.String Coq.Lists.List Coq.Init.Logic. Require Export Bedrock.Word. -Require Import ZArith NArith NPeano Ndec. -Require Import Compare_dec Omega. -Require Import OrderedType Coq.Structures.OrderedTypeEx. -Require Import FMapPositive FMapFullAVL JMeq. +Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec. +Require Import Coq.Arith.Compare_dec Coq.omega.Omega. +Require Import Coq.Structures.OrderedType Coq.Structures.OrderedTypeEx. +Require Import Coq.FSets.FMapPositive Coq.FSets.FMapFullAVL Coq.Logic.JMeq. -Require Import QhasmUtil QhasmCommon. +Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmCommon. + +Require Export Crypto.Util.FixCoqMistakes. (* We want to use pairs and triples as map keys: *) @@ -50,16 +52,16 @@ Module Pair_as_OT <: UsualOrderedType. destruct (Nat_as_OT.compare x0 y0); unfold Nat_as_OT.lt, Nat_as_OT.eq in *. - - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition). + - apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition auto with zarith). - destruct (Nat_as_OT.compare x1 y1); unfold Nat_as_OT.lt, Nat_as_OT.eq in *. + apply LT; abstract (unfold lt; simpl; destruct (Nat.eq_dec x0 y0); intuition). - + apply EQ; abstract (unfold lt; simpl; subst; intuition). - + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition). + + apply EQ; abstract (unfold lt; simpl; subst; intuition auto with relations). + + apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith). - - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition). + - apply GT; abstract (unfold lt; simpl; destruct (Nat.eq_dec y0 x0); intuition auto with zarith). Defined. Definition eq_dec (a b: t): {a = b} + {a <> b}. @@ -69,14 +71,14 @@ Module Pair_as_OT <: UsualOrderedType. - right; abstract ( unfold lt in *; simpl in *; destruct (Nat.eq_dec a0 b0); intuition; - inversion H; intuition). + inversion H; intuition auto with zarith). - left; abstract (inversion e; intuition). - right; abstract ( unfold lt in *; simpl in *; destruct (Nat.eq_dec b0 a0); intuition; - inversion H; intuition). + inversion H; intuition auto with zarith). Defined. End Pair_as_OT. @@ -132,7 +134,7 @@ Module Triple_as_OT <: UsualOrderedType. unfold Nat_as_OT.lt, Nat_as_OT.eq, lt, eq in *; destruct (Nat.eq_dec (get0 x) (get0 y)); destruct (Nat.eq_dec (get1 x) (get1 y)); - simpl; intuition). + simpl; intuition auto with zarith). Ltac compare_eq x y := abstract ( @@ -163,14 +165,14 @@ Module Triple_as_OT <: UsualOrderedType. - right; abstract ( unfold lt, get0, get1, get2 in *; simpl in *; destruct (Nat.eq_dec a0 b0), (Nat.eq_dec a1 b1); - intuition; inversion H; intuition). + intuition; inversion H; intuition auto with zarith). - left; abstract (inversion e; intuition). - right; abstract ( unfold lt, get0, get1, get2 in *; simpl in *; destruct (Nat.eq_dec b0 a0), (Nat.eq_dec b1 a1); - intuition; inversion H; intuition). + intuition; inversion H; intuition auto with zarith). Defined. End Triple_as_OT. diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v index d2fca3ce6..4eed28aad 100644 --- a/src/Assembly/Vectorize.v +++ b/src/Assembly/Vectorize.v @@ -1,6 +1,8 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NPeano NArith PArith Ndigits Compare_dec Arith. -Require Import ProofIrrelevance Ring List Omega. +Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.Arith.Compare_dec Coq.Arith.Arith. +Require Import Coq.Logic.ProofIrrelevance Coq.setoid_ring.Ring Coq.Lists.List Coq.omega.Omega. + +Require Export Crypto.Util.FixCoqMistakes. Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. diff --git a/src/Assembly/Wordize.v b/src/Assembly/Wordize.v index bac25db71..5e27a93b7 100644 --- a/src/Assembly/Wordize.v +++ b/src/Assembly/Wordize.v @@ -1,9 +1,11 @@ Require Export Bedrock.Word Bedrock.Nomega. -Require Import NArith PArith Ndigits Nnat NPow NPeano Ndec. -Require Import Compare_dec Omega. -Require Import FunctionalExtensionality ProofIrrelevance. -Require Import QhasmUtil QhasmEvalCommon. +Require Import Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.NArith.Nnat Coq.Numbers.Natural.Abstract.NPow Coq.Numbers.Natural.Peano.NPeano Coq.NArith.Ndec. +Require Import Coq.Arith.Compare_dec Coq.omega.Omega. +Require Import Coq.Logic.FunctionalExtensionality Coq.Logic.ProofIrrelevance. +Require Import Crypto.Assembly.QhasmUtil Crypto.Assembly.QhasmEvalCommon. + +Require Export Crypto.Util.FixCoqMistakes. Hint Rewrite wordToN_nat Nat2N.inj_add N2Nat.inj_add Nat2N.inj_mul N2Nat.inj_mul Npow2_nat : N. @@ -18,7 +20,7 @@ Section WordizeUtil. intros; unfold break in *; destruct (le_dec m n); inversion H; subst; clear H; simpl. Admitted. - + Lemma mask_wand : forall (n: nat) (x: word n) m b, (& (mask (N.to_nat m) x) < b)%N -> (& (x ^& (@NToWord n (N.ones m))) < b)%N. @@ -33,7 +35,7 @@ Section WordizeUtil. Qed. Lemma word_param_eq: forall n m, word n = word m -> n = m. - Proof. (* TODO: How do we prove this *) Admitted. + Proof. (* TODO: How do we prove this *) Admitted. Lemma word_conv_eq: forall {n m} (y: word m) p, &y = &(@convS (word m) (word n) y p). @@ -153,7 +155,7 @@ Section WordizeUtil. - intros; simpl; replace (a + 0) with a; nomega. - intros. - replace (a + S b) with (S a + b) by intuition. + replace (a + S b) with (S a + b) by intuition auto with zarith. rewrite (IHb (S a)); simpl; clear IHb. induction (Npow2 a), (Npow2 b); simpl; intuition. rewrite Pos.mul_xO_r; intuition. @@ -180,7 +182,7 @@ Section Wordization. rewrite wordToN_NToWord; intuition. apply (N.lt_le_trans _ (b + &y)%N _). - - apply N.add_lt_le_mono; try assumption; intuition. + - apply N.add_lt_le_mono; try assumption; intuition auto with relations. - replace (Npow2 n) with (b + Npow2 n - b)%N by nomega. replace (b + Npow2 n - b)%N with (b + (Npow2 n - b))%N by ( @@ -402,7 +404,7 @@ Ltac wordize_ast := | [ |- _ = _ ] => reflexivity end. -Ltac lt_crush := try abstract (clear; vm_compute; intuition). +Ltac lt_crush := try abstract (clear; vm_compute; intuition auto with zarith). (** Bounding Tactics **) diff --git a/src/BaseSystem.v b/src/BaseSystem.v index 840713168..48b6468cf 100644 --- a/src/BaseSystem.v +++ b/src/BaseSystem.v @@ -3,6 +3,7 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Notations. +Require Export Crypto.Util.FixCoqMistakes. Import Nat. Local Open Scope Z. @@ -140,11 +141,11 @@ Section PolynomialBaseCoefs. unfold bi. replace (Z.pos b1 ^ Z.of_nat (S i)) with (Z.pos b1 * (Z.pos b1 ^ Z.of_nat i)) by - (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition). + (rewrite Nat2Z.inj_succ; rewrite <- Z.pow_succ_r; intuition auto with zarith). replace (Z.pos b1 * Z.pos b1 ^ Z.of_nat i / Z.pos b1 ^ Z.of_nat i) with (Z.pos b1); auto. rewrite Z_div_mult_full; auto. - apply Z.pow_nonzero; intuition. + apply Z.pow_nonzero; intuition auto with lia. Qed. Lemma poly_base_good: diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index 1d8b730cb..dbfdb023e 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -5,8 +5,9 @@ Require Import Crypto.CompleteEdwardsCurve.Pre. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.Classes.Morphisms. -Require Import Relation_Definitions. +Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tuple Crypto.Util.Notations Crypto.Util.Tactics. +Require Export Crypto.Util.FixCoqMistakes. Module E. Import Group ScalarMult Ring Field CompleteEdwardsCurve.E. @@ -57,7 +58,7 @@ Module E. apply H; try common_denominator; [rewrite <-Hx; ring | ..]. - + Ltac bash_step := let addCompletePlus := constr:(edwardsAddCompletePlus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in let addCompleteMinus := constr:(edwardsAddCompleteMinus(char_gt_2:=char_gt_2)(d_nonsquare:=nonsquare_d)(a_square:=square_a)(a_nonzero:=nonzero_a)) in diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index f3820aeac..ac3523889 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -5,9 +5,10 @@ Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.Compl Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.Classes.Morphisms. -Require Import Relation_Definitions. +Require Import Coq.Relations.Relation_Definitions. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Notations. +Require Export Crypto.Util.FixCoqMistakes. Module Extended. Section ExtendedCoordinates. diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index 2ad567c92..e6305f798 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -11,6 +11,8 @@ Require Import Crypto.Algebra. Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic. +Require Export Crypto.Util.FixCoqMistakes. + Generalizable All Variables. Section PointEncodingPre. Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}. @@ -22,7 +24,7 @@ Section PointEncodingPre. Local Notation "x '^' 2" := (x*x) (at level 30). Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). - + Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}. Definition F_eqb x y := if eq_dec x y then true else false. Lemma F_eqb_iff : forall x y, F_eqb x y = true <-> x == y. @@ -64,7 +66,7 @@ Section PointEncodingPre. symmetry. apply E.solve_correct; eassumption. Qed. - + (* TODO : move? *) Lemma square_opp : forall x : F, (opp x ^2) == (x ^2). Proof. @@ -97,7 +99,7 @@ Section PointEncodingPre. let p := (if Bool.eqb (whd w) (sign_bit x) then x else opp x, y) in if (andb (F_eqb x 0) (whd w)) then None (* special case for 0, since its opposite has the same sign; if the sign bit of 0 is 1, produce None.*) - else Some p + else Some p else None end. @@ -112,7 +114,7 @@ Section PointEncodingPre. destruct x as [x1 x2]. destruct y as [y1 y2]. match goal with - | |- {prod_eq _ _ (?x1, ?x2) (?y1,?y2)} + {not (prod_eq _ _ (?x1, ?x2) (?y1,?y2))} => + | |- {prod_eq _ _ (?x1, ?x2) (?y1,?y2)} + {not (prod_eq _ _ (?x1, ?x2) (?y1,?y2))} => destruct (A_eq_dec x1 y1); destruct (A_eq_dec x2 y2) end; unfold prod_eq; intuition. Qed. @@ -162,7 +164,7 @@ Section PointEncodingPre. Definition point_eq (p q : point) : Prop := prod_eq eq eq (proj1_sig p) (proj1_sig q). Definition option_point_eq := option_eq (point_eq). - + Lemma option_point_eq_iff : forall p q, option_point_eq (Some p) (Some q) <-> option_coordinates_eq (Some (proj1_sig p)) (Some (proj1_sig q)). @@ -214,7 +216,7 @@ Section PointEncodingPre. Proof. unfold prod_eq; intros. repeat break_let. - intuition; etransitivity; eauto. + intuition auto with relations; etransitivity; eauto. Qed. Lemma option_coordinates_eq_sym : forall p q, option_coordinates_eq p q -> diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 4f51f299d..3ae1daa75 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -2,17 +2,18 @@ Require Import Coq.omega.Omega. Require Import Bedrock.Word. Require Import Crypto.Spec.EdDSA. Require Import Crypto.Tactics.VerdiTactics. -Require Import BinNat BinInt NArith Crypto.Spec.ModularArithmetic. -Require Import ModularArithmetic.ModularArithmeticTheorems. -Require Import ModularArithmetic.PrimeFieldTheorems. +Require Import Coq.NArith.BinNat Coq.ZArith.BinInt Coq.NArith.NArith Crypto.Spec.ModularArithmetic. +Require Import Crypto.ModularArithmetic.ModularArithmeticTheorems. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.Spec.CompleteEdwardsCurve. Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding. Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil. Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Require Import Zdiv. +Require Import Coq.ZArith.Zdiv. Require Import Crypto.Util.Tuple. +Require Export Crypto.Util.FixCoqMistakes. Local Open Scope equiv_scope. Generalizable All Variables. @@ -98,7 +99,7 @@ Qed. Global Instance pair_Equivalence {A B} `{@Equivalence A RA} `{@Equivalence B RB} : @Equivalence (A*B) (fun x y => fst x = fst y /\ snd x === snd y). Proof. - constructor; repeat intro; intuition; try congruence. + constructor; repeat intro; intuition auto with relations; try congruence. match goal with [H : _ |- _ ] => solve [rewrite H; auto] end. Qed. @@ -205,7 +206,7 @@ Proof. intros. case_eq (eqb a b); intros. { eapply eqb_iff; trivial. } - { specialize (eqb_iff a b). rewrite H in eqb_iff. intuition. } + { specialize (eqb_iff a b). rewrite H in eqb_iff. intuition auto with bool. } Qed. Definition eqb_eq_dec {T} (eqb:T->T->bool) (eqb_iff:forall a b, eqb a b = true <-> a = b) : @@ -281,4 +282,4 @@ End with_unqualified_modulo2. Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y. Proof. split; eauto using F_eqb_eq, F_eqb_complete. -Qed. \ No newline at end of file +Qed. diff --git a/src/Experiments/GenericFieldPow.v b/src/Experiments/GenericFieldPow.v index b3d83dbe8..0fe092f6a 100644 --- a/src/Experiments/GenericFieldPow.v +++ b/src/Experiments/GenericFieldPow.v @@ -1,5 +1,6 @@ Require Import Coq.setoid_ring.Cring. Require Import Coq.omega.Omega. +Require Export Crypto.Util.FixCoqMistakes. Generalizable All Variables. diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index a1d47ae8f..be9307b50 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -9,6 +9,8 @@ Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. Require Export Crypto.Util.IterAssocOp. +Require Export Crypto.Util.FixCoqMistakes. + Section ModularArithmeticPreliminaries. Context {m:Z}. Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F. @@ -76,13 +78,16 @@ Ltac eq_remove_proofs := lazymatch goal with simpl in *; apply Q; clear Q end. +(** TODO FIXME(from jgross): This tactic is way too powerful for + arcane reasons. It should not be using so many databases with + [intuition]. *) Ltac Fdefn := intros; repeat match goal with [ x : F _ |- _ ] => destruct x end; try eq_remove_proofs; demod; rewrite ?Z.mul_1_l; - intuition; demod; try solve [ f_equal; intuition ]. + intuition auto with zarith lia relations typeclass_instances; demod; try solve [ f_equal; intuition auto with zarith lia relations typeclass_instances ]. Local Open Scope F_scope. @@ -139,7 +144,7 @@ Section FandZ. Lemma ZToField_small_nonzero : forall z, (0 < z < m)%Z -> ZToField z <> (0:F m). Proof. - intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition. + intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition auto with zarith. Qed. Require Crypto.Algebra. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 7c171faf7..a0e1eb06b 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -15,6 +15,7 @@ Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Require Import Coq.QArith.QArith Coq.QArith.Qround. Require Import Crypto.Tactics.VerdiTactics. +Require Export Crypto.Util.FixCoqMistakes. Local Open Scope Z. Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := { @@ -662,4 +663,4 @@ Section Canonicalization. auto using freeze_opt_preserves_rep. Qed. *) -End Canonicalization. \ No newline at end of file +End Canonicalization. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index e6351dc17..1fe262577 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -17,6 +17,7 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil Crypt Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. +Require Export Crypto.Util.FixCoqMistakes. Local Open Scope Z_scope. Local Opaque add_to_nth carry_simple. diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 9255f033f..a9b9fbdfc 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -4,6 +4,7 @@ Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. Require Import Crypto.Util.Tactics. Require Import Crypto.ModularArithmetic.Pow2Base Crypto.BaseSystemProofs. +Require Export Crypto.Util.FixCoqMistakes. Require Crypto.BaseSystem. Local Open Scope Z_scope. @@ -784,7 +785,7 @@ Section carrying. (* TODO : move? *) Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. Proof. - induction x; simpl; intuition. + induction x; simpl; intuition auto with arith lia. Qed. Lemma nth_default_carry_gen_full fc fi d i n us diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index 5e61278f6..8566d30ab 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -5,6 +5,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Coq.omega.Omega. Require Import Crypto.Util.NumTheoryUtil. Require Import Crypto.Tactics.VerdiTactics. +Require Export Crypto.Util.FixCoqMistakes. Lemma Z_mod_mod x m : x mod m = (x mod m) mod m. symmetry. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 8d594e8ce..8d47e36ed 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -10,6 +10,7 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics. +Require Export Crypto.Util.FixCoqMistakes. Require Crypto.Algebra. Existing Class prime. diff --git a/src/Util/FixCoqMistakes.v b/src/Util/FixCoqMistakes.v new file mode 100644 index 000000000..abacfa580 --- /dev/null +++ b/src/Util/FixCoqMistakes.v @@ -0,0 +1,13 @@ +(** * Fixes *) + +(** Coq is poorly designed in some ways. We fix some of these issues + in this file. *) + +(** [intuition] means [intuition auto with *]. This is very wrong and + fragile and slow. We make [intuition] mean [intuition auto]. *) +Tactic Notation "intuition" tactic3(tactic) := intuition tactic. +Tactic Notation "intuition" := intuition auto. + +(** A version of [intuition] that allows you to see how the old + [intuition] tactic solves the proof. *) +Ltac debug_intuition := idtac "Warning: debug_intuition should not be used in production code."; intuition debug auto with *. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index 1032e1dc2..74c2b8537 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -5,6 +5,7 @@ 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. Create HintDb distr_length discriminated. Create HintDb simpl_set_nth discriminated. @@ -72,14 +73,14 @@ Definition splice_nth {T} n (x:T) xs := firstn n xs ++ x :: skipn (S n) xs. Hint Unfold splice_nth. Ltac boring := - simpl; intuition; + simpl; intuition auto with zarith datatypes; repeat match goal with | [ H : _ |- _ ] => rewrite H; clear H | [ |- appcontext[match ?pf with end] ] => solve [ case pf ] | _ => progress autounfold in * | _ => progress autorewrite with core | _ => progress simpl in * - | _ => progress intuition + | _ => progress intuition auto with zarith datatypes end; eauto. Ltac boring_list := @@ -1133,7 +1134,7 @@ Proof. induction n as [|n IHn]; destruct l as [|? l]; autorewrite with simpl_sum_firstn; simpl; try omega. { specialize (IHn l). destruct n; simpl; autorewrite with simpl_sum_firstn simpl_nth_default in *; - intuition. } + intuition auto with zarith. } Qed. Hint Resolve sum_firstn_nonnegative : znonzero. diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 4526e6dce..3aa80406b 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -1,4 +1,5 @@ (** * Reserved Notations *) +Require Export Crypto.Util.FixCoqMistakes. (** Putting them all together in one file prevents conflicts. Coq's parser (camlpX) is really bad at conflicting notation levels and diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index c16b87639..29fedaa9b 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -3,6 +3,7 @@ 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. Local Open Scope Z. (* TODO: move somewhere else for lemmas about Coqprime? *) diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index c881478dd..5ff9d203c 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -1,4 +1,5 @@ (** * Generic Tactics *) +Require Export Crypto.Util.FixCoqMistakes. (** Test if a tactic succeeds, but always roll-back the results *) Tactic Notation "test" tactic3(tac) := diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 05d47b7f8..15a248afe 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -1,6 +1,7 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. Require Import Crypto.Util.Decidable. +Require Export Crypto.Util.FixCoqMistakes. Fixpoint tuple' T n : Type := match n with @@ -194,4 +195,4 @@ Definition apply {R T} (n:nat) : function R T n -> tuple T n -> R := match n with | O => fun r _ => r | S n' => fun f x => apply' n' f x - end. \ No newline at end of file + end. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 077ad25a8..294e9d8f2 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -3,6 +3,7 @@ Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPe Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Notations. Require Import Coq.Lists.List. +Require Export Crypto.Util.FixCoqMistakes. Import Nat. Local Open Scope Z. @@ -68,7 +69,7 @@ Module Z. Proof. intros; rewrite Z.gt_lt_iff. apply Z.div_str_pos. - split; intuition. + split; intuition auto with omega. apply Z.divide_pos_le; try (apply Zmod_divide); omega. Qed. @@ -172,7 +173,7 @@ Module Z. rewrite div_mul' in divide_a by auto. replace (b * k) with (k * b) in divide_a by ring. replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. - rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). + rewrite Z.mul_cancel_l in divide_a by (intuition auto with nia; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). eapply Zdivide_intro; eauto. Qed. @@ -424,7 +425,7 @@ Module Z. omega. + intros. destruct (Z_lt_le_dec x n); try omega. - intuition. + intuition auto with zarith lia. left. rewrite shiftr_succ. replace (n - Z.succ x) with (Z.pred (n - x)) by omega. @@ -563,7 +564,7 @@ Module Z. destruct (in_inv In_list); subst. + apply Z.le_max_l. + etransitivity. - - apply IHl; auto; intuition. + - apply IHl; auto; intuition auto with datatypes. - apply Z.le_max_r. Qed. -- cgit v1.2.3