Fixed unsimplified multiplication definitions in Specific by separating out the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions.

1 files changed, 22 insertions, 4 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index badc17963..6298941db 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -111,25 +111,43 @@ Definition sub_correct (f g : fe25519)
   Eval cbv beta iota delta [proj1_sig sub_sig] in
   proj2_sig (sub_sig f g).
 
-Definition mul_sig (f g : fe25519) :
+Definition mul_simpl_sig (f g : fe25519) :
   { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
 Proof.
-  rewrite <-appify2_correct.
   cbv [fe25519] in *.
-  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end.
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
 Defined.
 
+Definition mul_simpl (f g : fe25519) : fe25519 :=
+  Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in
+  proj1_sig (mul_simpl_sig f g).
+
+Definition mul_simpl_correct (f g : fe25519)
+  : mul_simpl f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
+  Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in
+  proj2_sig (mul_simpl_sig f g).
+
+Definition mul_sig (f g : fe25519) :
+  { fg : fe25519 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+Proof.
+  eexists.
+  rewrite <- mul_simpl_correct.
+  rewrite <-appify2_correct.
+  cbv.
+  reflexivity.
+Defined.
+
 Definition mul (f g : fe25519) : fe25519 :=
   Eval cbv beta iota delta [proj1_sig mul_sig] in
   proj1_sig (mul_sig f g).
 
 Definition mul_correct (f g : fe25519)
   : mul f g = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g :=
-  Eval cbv beta iota delta [proj1_sig add_sig] in
+  Eval cbv beta iota delta [proj1_sig mul_sig] in
   proj2_sig (mul_sig f g).
 
 Import Morphisms.