From 1ea69cd53ff8472bb23c338d0e3fcac0a1f9ada5 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Fri, 16 Sep 2016 13:31:40 -0400 Subject: Derive EdDSA.verify from equational specification Experiments/SpecEd25519 will come back soon --- src/Util/Relations.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 src/Util/Relations.v (limited to 'src/Util/Relations.v') 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. -- cgit v1.2.3