diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-09-16 13:31:40 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-09-16 19:00:06 -0400 |
commit | 1ea69cd53ff8472bb23c338d0e3fcac0a1f9ada5 (patch) | |
tree | 14379b1df13a789daf454f29324661ebb85c9f0c /src/Util | |
parent | 7d139ded819549c587b169e6ef54d411bc543cd4 (diff) |
Derive EdDSA.verify from equational specification
Experiments/SpecEd25519 will come back soon
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Logic.v | 19 | ||||
-rw-r--r-- | src/Util/Option.v | 52 | ||||
-rw-r--r-- | src/Util/Relations.v | 29 | ||||
-rw-r--r-- | src/Util/WordUtil.v | 4 |
4 files changed, 85 insertions, 19 deletions
diff --git a/src/Util/Logic.v b/src/Util/Logic.v new file mode 100644 index 000000000..d518069a9 --- /dev/null +++ b/src/Util/Logic.v @@ -0,0 +1,19 @@ +Require Import Crypto.Util.FixCoqMistakes. + +(* WHY does this solve goals that [intuition] does not solve? *) +Ltac logic := + repeat match goal with + | |- _ => intro + | H:exists _, _ |- _ => destruct H + | H:_ /\ _ |- _ => destruct H + | |- _ => solve [eauto] + | |- _ => split + end. + +Lemma exists_and_indep_l {A B} P Q : + (exists a b, P a /\ Q a b) <-> (exists a:A, P a /\ exists b:B, Q a b). +Proof. logic. Qed. + +Lemma exists_and_indep_r {A B} P Q : + (exists a b, Q a b /\ P a) <-> (exists a:A, P a /\ exists b:B, Q a b). +Proof. logic. Qed. diff --git a/src/Util/Option.v b/src/Util/Option.v index df922f8c1..98e172ad4 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -1,18 +1,42 @@ Require Import Coq.Classes.Morphisms. +Require Import Coq.Relations.Relation_Definitions. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Crypto.Util.Logic. -Global Instance option_rect_Proper_nd {A T} - : Proper ((pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@option_rect A (fun _ => T)). -Proof. - intros ?? H ??? [|]??; subst; simpl; congruence. -Qed. +Definition option_eq {A} eq (x y : option A) := + match x with + | None => y = None + | Some ax => match y with + | None => False + | Some ay => eq ax ay + end + end. -Global Instance option_rect_Proper_nd' {A T} - : Proper ((pointwise_relation _ eq) ==> eq ==> forall_relation (fun _ => eq)) (@option_rect A (fun _ => T)). +Global Instance Equivalence_option_eq {T} {R} {Equivalence_R:@Equivalence T R} + : Equivalence (option_eq R). Proof. - intros ?? H ??? [|]; subst; simpl; congruence. + split; cbv; repeat (break_match || intro || intuition congruence || + solve [ reflexivity | symmetry; eassumption | etransitivity; eassumption ] ). Qed. -Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?T))) => exact (@option_rect_Proper_nd' A T) : typeclass_instances. + +Global Instance Proper_option_rect_nd_changebody + {A B:Type} {RB:relation B} {a:option A} + : Proper (pointwise_relation _ RB ==> RB ==> RB) (fun S N => option_rect (fun _ => B) S N a). +Proof. cbv; repeat (intro || break_match); intuition. Qed. + +(* FIXME: there used to be a typeclass resolution hint here, something like + Hint Extern 1 (Proper _ (@option_rect ?A (fun _ => ?B))) => exact (@Proper_option_rect_nd_changebody A B _ _) : typeclass_instances. + but I could not get it working after generalizing [RB] from [Logic.eq] ~ andreser *) + +Global Instance Proper_option_rect_nd_changevalue + {A B RA RB} some {Proper_some: Proper (RA==>RB) some} + : Proper (RB ==> option_eq RA ==> RB) (@option_rect A (fun _ => B) some). +Proof. cbv; repeat (intro || break_match || f_equiv || intuition congruence). Qed. + +Lemma option_rect_false_returns_true_iff {T} (f:T->bool) (o:option T) : + option_rect (fun _ => bool) f false o = true <-> exists s:T, o = Some s /\ f s = true. +Proof. unfold option_rect; break_match; logic; congruence. Qed. Lemma option_rect_option_map : forall {A B C} (f:A->B) some none v, option_rect (fun _ => C) (fun x => some (f x)) none v = option_rect (fun _ => C) some none (option_map f v). @@ -42,7 +66,6 @@ Ltac commute_option_rect_Let_In := (* pull let binders out side of option_rect p end. *) -(** TODO: possibly move me, remove local *) Ltac replace_option_match_with_option_rect := idtac; lazymatch goal with @@ -61,15 +84,6 @@ Ltac simpl_option_rect := (* deal with [option_rect _ _ _ None] and [option_rect => change (option_rect P S N (Some x)) with (S x); cbv beta end. -Definition option_eq {A} eq (x y : option A) := - match x with - | None => y = None - | Some ax => match y with - | None => False - | Some ay => eq ax ay - end - end. - Definition option_leq_to_eq {A} (x y : option A) : x = y -> option_eq eq x y. Proof. destruct x; intro; subst; simpl; reflexivity. Qed. diff --git a/src/Util/Relations.v b/src/Util/Relations.v new file mode 100644 index 000000000..aa280db26 --- /dev/null +++ b/src/Util/Relations.v @@ -0,0 +1,29 @@ +Require Import Crypto.Util.FixCoqMistakes. +Require Import Crypto.Util.Logic. +Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. + +Lemma symmetry_iff {T} {R} {Rsym:@Symmetric T R} x y: R x y <-> R y x. + intuition eauto using symmetry. +Qed. + +Lemma and_rewrite_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB} + (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a + : (RB (f a) ref /\ P a (f a)) <-> (RB (f a) ref /\ P a ref). +Proof. + logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. +Qed. + +Lemma and_rewriteleft_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB} + (f:A->B) ref P {Proper_P: Proper (RA==>RB==>iff) P} a + : (RB ref (f a) /\ P a (f a)) <-> (RB ref (f a) /\ P a ref). +Proof. + logic; match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. +Qed. + +Lemma exists_and_equiv_r {A} {RA} {Equivalence_RA:Equivalence RA} + P {Proper_P: Proper (RA==>iff) P} (ref:A) + : (exists a, P a /\ RA a ref) <-> P ref. +Proof. + logic; try match goal with [H:_|-_] => (rewrite H || rewrite <-H); assumption end. + repeat (assumption||reflexivity||econstructor); assumption. (* WHY the last [assumption]?*) +Qed. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 6a8831b14..9e88c1731 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -59,3 +59,7 @@ Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with | eq_refl => w end)); abstract omega. Defined. + +Lemma combine_eq_iff {a b} (A:word a) (B:word b) C : + combine A B = C <-> A = split1 a b C /\ B = split2 a b C. +Proof. intuition; subst; auto using split1_combine, split2_combine, combine_split. Qed. |