diff options
author | Jason Gross <jasongross9@gmail.com> | 2016-07-22 15:33:31 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-07-22 15:33:31 -0700 |
commit | 2abb4b5ea3440d478540aad852cfe81e65596189 (patch) | |
tree | 3851f94e613e595bc99da6c932ec99e033694fa3 /src/Experiments/DerivationsOptionRectLetInEncoding.v | |
parent | 29bb3dd531be45ba7960b34ef759b44436e48905 (diff) | |
parent | 4519b114c66b184611068b2cc9bdad644f4a5a47 (diff) |
Merge pull request #37 from JasonGross/fix-intuition
Redesign intuition, speeding up overall compilation by 20%
Diffstat (limited to 'src/Experiments/DerivationsOptionRectLetInEncoding.v')
-rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 15 |
1 files changed, 8 insertions, 7 deletions
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. |