Remove unfolding, rewrite -> setoid_rewrite

Moving the [scalar] argument to the beginning of [iter_op] makes
inference of the [Proper] lemmas a bit easier.

Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows
[setoid_rewrite] to work; since [setoid_rewrite] does more unfolding
than [rewrite], we no longer need to unfold things to make the [rewrite]
work.

1 files changed, 5 insertions, 3 deletions

diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v
index 6e61d0ae2..ebecba606 100644
--- a/src/Specific/Ed25519.v
+++ b/src/Specific/Ed25519.v
@@ -311,6 +311,9 @@ Section Ed25519Frep.
     := repeat first [ reflexivity
                     | apply f_equal ].
 
+
+  Local Existing Instance eq_Reflexive. (* To get some of the [setoid_rewrite]s below to work, we need to infer [Reflexive eq] before [Reflexive Equivalence.equiv] *)
+
   Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}.
   Proof.
     eexists; intros.
@@ -534,9 +537,8 @@ Section Ed25519Frep.
       set_evars; erewrite (f_equal2 (@weqb b)); subst_evars; [|reflexivity|symmetry]. Focus 2. {
         unfold twistedToExtended.
         rewrite F_mul_0_l.
-        unfold curve25519params, q. (* TODO: do we really wanna do it here? *)
-        rewrite <-(rcFOK 0%F).
-        rewrite <-(rcFOK 1%F).
+        setoid_rewrite <- (rcFOK 0%F). (* setoid_rewrite, to bypass needing to unfold things *)
+        setoid_rewrite <-(rcFOK 1%F).
         match goal with |- context [?x] => match x with (fst (proj1_sig B)) => rewrite <-(rcFOK x) end end.
         match goal with |- context [?x] => match x with (snd (proj1_sig B)) => rewrite <-(rcFOK x) end end.
         autorewrite with FRepOperations. (* breaks reflexivity; use [reflexivity_when_unification_is_stupid_about_evars] instead *)