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/Logic.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 src/Util/Logic.v (limited to 'src/Util/Logic.v') 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. -- cgit v1.2.3