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, 3 deletions

diff --git a/src/Specific/GF1305.v b/src/Specific/GF1305.v
index 74f914616..077c98954 100644
--- a/src/Specific/GF1305.v
+++ b/src/Specific/GF1305.v
@@ -115,16 +115,35 @@ Definition sub_correct (f g : fe1305)
   Eval cbv beta iota delta [proj1_sig sub_sig] in
   proj2_sig (sub_sig f g). (* Coq 8.4 : 10s *)
 
-Definition mul_sig (f g : fe1305) :
+Definition mul_simpl_sig (f g : fe1305) :
   { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
 Proof.
-  rewrite <-appify2_correct. (* Coq 8.4 : 5s; changes the [repeat match ... => destruct] below from 25s to 8s *)
   cbv [fe1305] in *.
-  repeat match goal with [p : (_*Z)%type |- _ ] => destruct p end. (* 8s *)
+  repeat match goal with p : (_ * Z)%type |- _ => destruct p end.
   eexists.
   cbv.
   autorewrite with zsimplify.
   reflexivity.
+Defined.
+
+Definition mul_simpl (f g : fe1305) : fe1305 :=
+  Eval cbv beta iota delta [proj1_sig mul_simpl_sig] in
+  proj1_sig (mul_simpl_sig f g).
+
+Definition mul_simpl_correct (f g : fe1305)
+  : 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 : fe1305) :
+  { fg : fe1305 | fg = ModularBaseSystemInterface.mul (k_ := k_) (c_ := c_) f g}.
+Proof.
+  eexists.
+  rewrite <-mul_simpl_correct.
+  rewrite <-appify2_correct.
+  cbv.
+  autorewrite with zsimplify.
+  reflexivity.
 Defined. (* Coq 8.4 : 14s *)
 
 Definition mul (f g : fe1305) : fe1305 :=