diff options
author | Jason Gross <jgross@mit.edu> | 2016-05-24 12:08:06 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:44:48 -0400 |
commit | 59492b73586b761cf6089ec12345c63983dd7021 (patch) | |
tree | 2d30b66300223e5a05d8a200c4b350e2fbed1968 /src | |
parent | abc8b6fcd8ec0043b9f43bcbfb32b7030fb27421 (diff) |
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.
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/Ed25519.v | 8 | ||||
-rw-r--r-- | src/Util/IterAssocOp.v | 10 |
2 files changed, 10 insertions, 8 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 *) diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 5e23bb987..6116312e1 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -5,12 +5,12 @@ Local Open Scope equiv_scope. Generalizable All Variables. Section IterAssocOp. Context `{Equivalence T} + {scalar : Type} (op:T->T->T) {op_proper:Proper (equiv==>equiv==>equiv) op} (assoc: forall a b c, op a (op b c) === op (op a b) c) (neutral:T) (neutral_l : forall a, op neutral a === a) (neutral_r : forall a, op a neutral === a) - {scalar : Type} (testbit : scalar -> nat -> bool) (scToN : scalar -> N) (testbit_spec : forall x i, testbit x i = N.testbit_nat (scToN x) i). @@ -63,7 +63,7 @@ Section IterAssocOp. | S i' => (i', if testbit sc i' then op a acc2 else acc2) end. - Definition iter_op sc a bound : T := + Definition iter_op sc a bound : T := snd (funexp (test_and_op sc a) (bound, neutral) bound). Definition test_and_op_inv sc a (s : nat * T) := @@ -152,8 +152,8 @@ Section IterAssocOp. Lemma iter_op_termination : forall sc a bound, N.size_nat (scToN sc) <= bound -> - test_and_op_inv sc a - (funexp (test_and_op sc a) (bound, neutral) bound) -> + test_and_op_inv sc a + (funexp (test_and_op sc a) (bound, neutral) bound) -> iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a. Proof. unfold test_and_op_inv, iter_op; simpl; intros ? ? ? ? Hinv. @@ -183,7 +183,7 @@ Section IterAssocOp. rewrite Nat2N.id. auto. Qed. - + Lemma iter_op_spec : forall sc a bound, N.size_nat (scToN sc) <= bound -> iter_op sc a bound === nat_iter_op (N.to_nat (scToN sc)) a. Proof. |