diff options
| -rw-r--r-- | _CoqProject | 4 | ||||
| -rw-r--r-- | src/Assembly/Vectorize.v | 6 | ||||
| -rw-r--r-- | src/Experiments/EncodingLemmas.v (renamed from src/Experiments/DerivationsOptionRectLetInEncoding.v) | 47 | ||||
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 24 | ||||
| -rw-r--r-- | src/Specific/GF1305.v | 1 | ||||
| -rw-r--r-- | src/Specific/GF25519.v | 19 | ||||
| -rw-r--r-- | src/Util/LetIn.v | 47 | ||||
| -rw-r--r-- | src/Util/Notations.v | 1 |
8 files changed, 64 insertions, 85 deletions
diff --git a/_CoqProject b/_CoqProject index 797f2a12c..a14a022f2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -35,8 +35,8 @@ src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v src/Encoding/PointEncodingPre.v -src/Experiments/DerivationsOptionRectLetInEncoding.v src/Experiments/EdDSARefinement.v +src/Experiments/EncodingLemmas.v src/Experiments/GenericFieldPow.v src/ModularArithmetic/ExtPow2BaseMulProofs.v src/ModularArithmetic/ExtendedBaseVector.v @@ -63,6 +63,7 @@ src/ModularArithmetic/Montgomery/ZBounded.v src/ModularArithmetic/Montgomery/ZProofs.v src/Reflection/CommonSubexpressionElimination.v src/Reflection/Inline.v +src/Reflection/InlineInterp.v src/Reflection/InlineWf.v src/Reflection/InputSyntax.v src/Reflection/InterpProofs.v @@ -99,6 +100,7 @@ src/Util/GlobalSettings.v src/Util/HProp.v src/Util/Isomorphism.v src/Util/IterAssocOp.v +src/Util/LetIn.v src/Util/ListUtil.v src/Util/Logic.v src/Util/NatUtil.v diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v index 08e9ee356..b8262d5d5 100644 --- a/src/Assembly/Vectorize.v +++ b/src/Assembly/Vectorize.v @@ -4,11 +4,7 @@ Require Import Coq.Logic.ProofIrrelevance Coq.setoid_ring.Ring Coq.Lists.List Co Require Import Crypto.Util.Notations. 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. - -Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)). +Require Export Crypto.Util.LetIn. Section Vector. Import ListNotations. diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/EncodingLemmas.v index 83de8a4fd..639a80f1b 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/EncodingLemmas.v @@ -13,6 +13,7 @@ Require Import Crypto.Util.IterAssocOp Crypto.Util.WordUtil. Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Require Import Coq.ZArith.Zdiv. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.LetIn. Require Export Crypto.Util.FixCoqMistakes. Local Open Scope equiv_scope. @@ -26,17 +27,6 @@ Definition path_sig {A P} {RA:relation A} {Rsig:relation (@sig A P)} : Rsig x (exist _ y0 (HP _ _ pf (proj2_sig x))). Proof. destruct x. eapply H. assumption. Defined. -Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. -Global Instance Let_In_Proper_changebody {A P R} {Reflexive_R:@Reflexive P R} - : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)). -Proof. - lazy; intros; try congruence. - subst; auto. -Qed. - -Lemma Let_In_Proper_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB) f} - : Proper (RA ==> RB) (fun x => Let_In x f). -Proof. intuition. Qed. Ltac fold_identity_lambdas := repeat match goal with @@ -44,46 +34,11 @@ Ltac fold_identity_lambdas := | |- appcontext [fun x => ?f x] => change (fun x => f x) with f in * end. -Local Ltac replace_let_in_with_Let_In := - match goal with - | [ |- context G[let x := ?y in @?z x] ] - => let G' := context G[Let_In y z] in change G' - end. - -Local Ltac Let_In_app fn := - match goal with - | [ |- appcontext G[Let_In (fn ?x) ?f] ] - => change (Let_In (fn x) f) with (Let_In x (fun y => f (fn y))); cbv beta - end. - Lemma if_map : forall {T U} (f:T->U) (b:bool) (x y:T), (if b then f x else f y) = f (if b then x else y). Proof. destruct b; trivial. Qed. -Lemma pull_Let_In {B C} (f : B -> C) A (v : A) (b : A -> B) - : Let_In v (fun v' => f (b v')) = f (Let_In v b). -Proof. - reflexivity. -Qed. - -Lemma Let_app_In {A B T} (g:A->B) (f:B->T) (x:A) : - @Let_In _ (fun _ => T) (g x) f = - @Let_In _ (fun _ => T) x (fun p => f (g x)). -Proof. reflexivity. Qed. - -Lemma Let_app_In' : forall {A B T} {R} {R_equiv:@Equivalence T R} - (g : A -> B) (f : B -> T) (x : A) - f' (f'_ok: forall z, f' z === f (g z)), - Let_In (g x) f === Let_In x f'. -Proof. intros; cbv [Let_In]; rewrite f'_ok; reflexivity. Qed. -Definition unfold_Let_In {A B} x (f:A->B) : Let_In x f = let y := x in f y := eq_refl. - -Lemma Let_app2_In {A B C D T} (g1:A->C) (g2:B->D) (f:C*D->T) (x:A) (y:B) : - @Let_In _ (fun _ => T) (g1 x, g2 y) f = - @Let_In _ (fun _ => T) (x, y) (fun p => f ((g1 (fst p), g2 (snd p)))). -Proof. reflexivity. Qed. - Lemma funexp_proj {T T'} `{@Equivalence T' RT'} (proj : T -> T') (f : T -> T) diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 2d4bb525f..eda2a584d 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -11,6 +11,7 @@ Require Import Crypto.ModularArithmetic.ModularBaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystemProofs. Require Import Coq.Lists.List. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.AdditionChainExponentiation. Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil Crypto.Util.CaseUtil. Import ListNotations. @@ -54,9 +55,6 @@ Definition zeros_opt := Eval compute in (@zeros). Definition bit_index_opt := Eval compute in bit_index. Definition digit_index_opt := Eval compute in digit_index. -Definition Let_In {A P} (x : A) (f : forall y : A, P y) - := let y := x in f y. - (* Some automation that comes in handy when constructing base parameters *) Ltac opt_step := match goal with @@ -160,23 +158,6 @@ Ltac kill_precondition H := forward H; [abstract (try exact eq_refl; clear; cbv; intros; repeat break_or_hyp; intuition)|]; subst_precondition. -Lemma Let_In_push : forall {A B C} (g : A -> B) (f : B -> C) x, - f (Let_In x g) = Let_In x (fun y => f (g y)). -Proof. - intros. - cbv [Let_In]. - reflexivity. -Qed. - -Lemma Let_In_ext : forall {A B} (f g : A -> B) x, - (forall x, f x = g x) -> - Let_In x g = Let_In x f. -Proof. - intros. - cbv [Let_In]. - congruence. -Qed. - Section Carries. Context `{prm : PseudoMersenneBaseParams} (* allows caller to precompute k and c *) @@ -680,7 +661,7 @@ Proof. + destruct a. apply IHy1. econstructor; try assumption. - apply H0; rewrite H; reflexivity. + apply H0; eapply Proper_nth_default; eauto; reflexivity. Qed. Section PowInv. @@ -748,7 +729,6 @@ Section PowInv. Definition inv_opt_correct x : eq (inv_opt x) (inv chain chain_correct x) := Eval cbv [proj2_sig inv_opt_sig] in (proj2_sig (inv_opt_sig x)). - End PowInv. Section Conversion. diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v index 74fc1d704..306dd4b28 100644 --- a/src/Specific/GF1305.v +++ b/src/Specific/GF1305.v @@ -9,6 +9,7 @@ Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 74d722c57..d98781f9f 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -9,6 +9,8 @@ Require Import Coq.Lists.List Crypto.Util.ListUtil. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Tactics. +Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Decidable. Require Import Crypto.Algebra. @@ -369,13 +371,10 @@ Proof. cbv [conditional_subtract_modulus_opt]. rewrite !modulus_digits_subst. cbv - [from_list_default]. - rewrite Let_In_push. - do 20 (erewrite Let_In_ext; [ | - repeat match goal with - | |- _ => progress intros; try apply Let_In_ext - | |- _ = from_list_default _ _ (Let_In _ _) => etransitivity; try (rewrite Let_In_push; reflexivity) - | |- from_list_default _ _ (Let_In _ _) = _ => etransitivity; try (rewrite Let_In_push; reflexivity) - end; reflexivity ]). + (* TODO(jgross,jadep): use Reflective linearization here? *) + repeat ( + set_evars; rewrite app_Let_In_nd; subst_evars; + eapply Proper_Let_In_nd_changebody; [reflexivity|intro]). cbv [from_list_default from_list_default']. reflexivity. Defined. @@ -438,10 +437,8 @@ Definition sqrt_sig (f : fe25519) : Proof. eexists. cbv [sqrt_5mod8_opt]. - apply Let_In_ext. - intros. - do 2 rewrite <-mul_correct. - rewrite <-eqb_correct. + apply Proper_Let_In_nd_changebody; [reflexivity|intro]. + set_evars. rewrite <-!mul_correct, <-eqb_correct. subst_evars. reflexivity. Defined. diff --git a/src/Util/LetIn.v b/src/Util/LetIn.v new file mode 100644 index 000000000..479d3a454 --- /dev/null +++ b/src/Util/LetIn.v @@ -0,0 +1,47 @@ +Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. +Require Import Crypto.Util.Tactics. + +Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y. +Notation "'Let' x := y 'in' f" := (Let_In y (fun x => f)) + (format "'[' 'Let' x := y 'in' ']' '/' '[' f ']'", + at level 200, f at level 200). + +Global Instance Proper_Let_In_nd_changebody {A P R} {Reflexive_R:@Reflexive P R} + : Proper (eq ==> pointwise_relation _ R ==> R) (@Let_In A (fun _ => P)). +Proof. lazy; intros; subst; auto; congruence. Qed. + +(* FIXME: it adding this as a typeclass instance makes typeclass + resolution loop in ModularBaseystemOpt *) +Lemma Proper_Let_In_nd_changevalue {A B} RA {RB} (f:A->B) {Proper_f:Proper (RA==>RB) f} + : Proper (RA ==> RB) (fun x => Let_In x f). +Proof. intuition. Qed. + +Lemma app_Let_In_nd {A B C} (f:B -> C) : forall (e:A) (C:A -> B), + f (Let_In e C) = Let_In e (fun v => f (C v)). +Proof. intros. cbv [Let_In]. reflexivity. Qed. + +Class _call_let_in_to_Let_In {T} (e:T) := _let_in_to_Let_In_return : T. +(* : forall T, gallina T -> gallina T, structurally recursive in the argument *) +Ltac let_in_to_Let_In e := + lazymatch e with + | let x := ?ex in @?eC x => + let ex := let_in_to_Let_In ex in + let eC := let_in_to_Let_In eC in + constr:(Let_In ex eC) + | ?f ?x => + let f := let_in_to_Let_In f in + let x := let_in_to_Let_In x in + constr:(f x) + | (fun x : ?T => ?C) => + lazymatch constr:(fun (x : T) => (_ : _call_let_in_to_Let_In C)) + (* [C] here above is an open term that references "x" by name *) + with fun x => @?C x => C end (* match drops the type cast *) + | ?x => x + end. +Hint Extern 0 (_call_let_in_to_Let_In ?e) => ( + let e := let_in_to_Let_In e in eexact e +) : typeclass_instances. +Ltac change_let_in_with_Let_In := + let g := get_goal in + let g' := let_in_to_Let_In g in + change g'.
\ No newline at end of file diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 0b248cd6e..166130824 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -63,3 +63,4 @@ Reserved Notation "'slet' x := A 'in' b" (at level 200, b at level 200, format "'slet' x := A 'in' '//' b"). Reserved Notation "'λ' x .. y , t" (at level 200, x binder, y binder, right associativity). Reserved Notation "'λn' x .. y , t" (at level 200, right associativity). +(* FIXME: breaks Reflection.Syntax: Reserved Notation "'Let' x := y 'in' f" (at level 200, f at level 200). *)
\ No newline at end of file |