Derive EdDSA.verify from equational specification

Experiments/SpecEd25519 will come back soon

1 files changed, 19 insertions, 0 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.