rewrite ExtendedCoordinates, fix Ed25519

3 files changed, 45 insertions, 13 deletions

diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index 7f580380f..c1c514171 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -115,10 +115,11 @@ Section Homomorphism_rev.
           {phi'_inv : forall a, phi' (inv a) = INV (phi' a)}
           {phi'_id : phi' id = ID}.
 
-  Local Instance group_from_redundant_representation
-    : @group H eq op id inv.
+  Lemma group_from_redundant_representation
+    : @group H eq op id inv /\ @Monoid.is_homomorphism G EQ OP H eq op phi /\ @Monoid.is_homomorphism H eq op G EQ OP phi'.
   Proof.
     repeat match goal with
+           | [ H : _/\_ |- _ ] => destruct H; try clear H
            | [ H : group |- _ ] => destruct H; try clear H
            | [ H : monoid |- _ ] => destruct H; try clear H
            | [ H : is_associative |- _ ] => destruct H; try clear H
@@ -132,7 +133,7 @@ Section Homomorphism_rev.
            | [ H : eq _ _ |- _ ] => apply phi'_eq in H
            | [ |- eq _ _ ] => apply phi'_eq
            | [ H : EQ _ _ |- _ ] => rewrite H
-           | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id by reflexivity
+           | _ => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id, ?phi'_phi_id by reflexivity
            | [ H : _ |- _ ] => progress erewrite ?phi'_op, ?phi'_inv, ?phi'_id in H by reflexivity
            | _ => solve [ eauto ]
            end.
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 066886e83..8110ad5cd 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -19,7 +19,6 @@ Module IntegralDomain.
   Module _LargeCharacteristicReflective.
     Section ReflectiveNsatzSideConditionProver.
       Import BinInt BinNat BinPos.
-      Lemma N_one_le_pos p : (N.one <= N.pos p)%N. Admitted.
       Context {R eq zero one opp add sub mul}
               {ring:@Algebra.ring R eq zero one opp add sub mul}
               {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}.
@@ -50,8 +49,9 @@ Module IntegralDomain.
 
       Lemma CtoZ_correct c : of_Z (CtoZ c) = denote c.
       Proof.
+        Set Printing All.
         induction c; simpl CtoZ; simpl denote;
-          repeat (rewrite_hyp ?*; Ring.push_homomorphism constr:(of_Z)); reflexivity.
+          repeat (rewrite_hyp ?* || Ring.push_homomorphism constr:(of_Z)); reflexivity.
       Qed.
 
       (* TODO: move *)
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index b69e9b191..f39d730f2 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -135,15 +135,46 @@ Section Homomorphism.
   Qed.
 End Homomorphism.
 
+(* TODO: file a Coq bug for rewrite_strat -- it should accept ltac variables *)
 Ltac push_homomorphism phi :=
-  let H := constr:(_:is_homomorphism(phi:=phi)) in
-  repeat rewrite
-         ?(homomorphism_zero(     phi_homom:=H)),
-         ?(homomorphism_one(is_homomorphism:=H)),
-         ?(homomorphism_add(      phi_homom:=H)),
-         ?(homomorphism_opp(      phi_homom:=H)),
-         ?(homomorphism_sub(      phi_homom:=H)),
-         ?(homomorphism_mul(is_homomorphism:=H)).
+  let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in
+  pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_0;
+  pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_1;
+  pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_p;
+  pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_o;
+  pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_s;
+  pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H)
+    as _push_homomrphism_m;
+  (rewrite_strat bottomup (terms _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m));
+  clear _push_homomrphism_0 _push_homomrphism_1 _push_homomrphism_p _push_homomrphism_o _push_homomrphism_s _push_homomrphism_m.
+
+Ltac pull_homomorphism phi :=
+  let H := constr:(_ : @Ring.is_homomorphism _ _ _ _ _ _ _ _ _ _ phi) in
+  pose proof (@homomorphism_zero _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_0;
+  pose proof (@homomorphism_one _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_1;
+  pose proof (@homomorphism_add _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_p;
+  pose proof (@homomorphism_opp _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_o;
+  pose proof (@homomorphism_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_s;
+  pose proof (@homomorphism_mul _ _ _ _ _ _ _ _ _ _ _ H)
+    as _pull_homomrphism_m;
+  symmetry in _pull_homomrphism_0;
+  symmetry in _pull_homomrphism_1;
+  symmetry in _pull_homomrphism_p;
+  symmetry in _pull_homomrphism_o;
+  symmetry in _pull_homomrphism_s;
+  symmetry in _pull_homomrphism_m;
+  (rewrite_strat bottomup (terms _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m));
+  clear _pull_homomrphism_0 _pull_homomrphism_1 _pull_homomrphism_p _pull_homomrphism_o _pull_homomrphism_s _pull_homomrphism_m.
 
 Lemma isomorphism_to_subring_ring
       {T EQ ZERO ONE OPP ADD SUB MUL}