Generalize field_from_redundant_representation

Note that the old version did not need phi', but the new version does

3 files changed, 80 insertions, 88 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index fb34e488e..e10552f9c 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -929,8 +929,10 @@ Module Field.
             {phi'_inv : forall a, phi' (inv a) = INV (phi' a)}
             (phi'_div : forall a b, phi' (div a b) = DIV (phi' a) (phi' b)).
 
-    Local Instance field_from_redundant_representation
-      : @field H eq zero one opp add sub mul inv div.
+    Lemma field_and_homomorphism_from_redundant_representation
+      : @field H eq zero one opp add sub mul inv div
+        /\ @Ring.is_homomorphism F EQ ONE ADD MUL H eq one add mul phi
+        /\ @Ring.is_homomorphism H eq one add mul F EQ ONE ADD MUL phi'.
     Proof.
       repeat match goal with
              | [ H : field |- _ ] => destruct H; try clear H
@@ -956,8 +958,8 @@ Module Field.
              | [ |- eq _ _ ] => apply phi'_eq
              | [ H : (~eq _ _)%type |- _ ] => pose proof (fun pf => H (proj1 (@phi'_eq _ _) pf)); clear H
              | [ H : EQ _ _ |- _ ] => rewrite H
-             | _ => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div by reflexivity
-             | [ H : _ |- _ ] => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div in H by reflexivity
+             | _ => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div, ?phi'_phi_id by reflexivity
+             | [ H : _ |- _ ] => progress erewrite ?phi'_zero, ?phi'_one, ?phi'_opp, ?phi'_add, ?phi'_sub, ?phi'_mul, ?phi'_inv, ?phi'_div, ?phi'_phi_id in H by reflexivity
              | _ => solve [ eauto ]
              end.
     Qed.
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index e89615dde..920aeaef8 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -386,79 +386,72 @@ Definition mbs_field := modular_base_system_field modulus_gt_2.
 
 Import Morphisms.
 
-Lemma field25519 : @field fe25519 eq zero_ one_ opp add sub mul inv div.
-Proof.
-  pose proof (Equivalence_Reflexive : Reflexive eq).
-  eapply (Field.equivalent_operations_field (fieldR := mbs_field)).
-  Grab Existential Variables.
-  + reflexivity.
-  + reflexivity.
-  + reflexivity.
-  + intros; rewrite mul_correct.
-    rewrite carry_mul_opt_correct by auto using k_subst, c_subst.
-    cbv [eq].
-    rewrite carry_mul_rep by reflexivity.
-    rewrite mul_rep; reflexivity.
-  + intros; rewrite sub_correct, sub_opt_correct; reflexivity.
-  + intros; rewrite add_correct, add_opt_correct; reflexivity.
-  + intros; rewrite inv_correct, inv_opt_correct; reflexivity.
-  + intros; rewrite opp_correct, opp_opt_correct; reflexivity.
+Local Existing Instance prime_modulus.
+
+Lemma field25519_and_homomorphisms
+  : @field fe25519 eq zero_ one_ opp add sub mul inv div
+    /\ @Ring.is_homomorphism
+         (F modulus) Logic.eq F.one F.add F.mul
+         fe25519 eq one_ add mul encode
+    /\ @Ring.is_homomorphism
+         fe25519 eq one_ add mul
+         (F modulus) Logic.eq F.one F.add F.mul
+         decode.
+Proof.
+  eapply @Field.field_and_homomorphism_from_redundant_representation.
+  { exact (F.field_modulo _). }
+  { apply encode_rep. }
+  { reflexivity. }
+  { reflexivity. }
+  { reflexivity. }
+  { intros; rewrite opp_correct, opp_opt_correct; apply opp_rep; reflexivity. }
+  { intros; rewrite add_correct, add_opt_correct; apply add_rep; reflexivity. }
+  { intros; rewrite sub_correct, sub_opt_correct; apply sub_rep; reflexivity. }
+  { intros; rewrite mul_correct, carry_mul_opt_correct by reflexivity; apply carry_mul_rep; reflexivity. }
+  { intros; rewrite inv_correct, inv_opt_correct by reflexivity; apply inv_rep; reflexivity. }
+  { intros; apply encode_rep. }
 Qed.
 
-
-Lemma carry_field25519 : @field fe25519 eq zero_ one_ carry_opp carry_add carry_sub mul inv div.
-Proof.
-  pose proof (Equivalence_Reflexive : Reflexive eq).
-  eapply (Field.equivalent_operations_field (fieldR := mbs_field)).
-  Grab Existential Variables.
-  + reflexivity.
-  + reflexivity.
-  + reflexivity.
-  + intros; rewrite mul_correct.
-    rewrite carry_mul_opt_correct by auto using k_subst, c_subst.
-    cbv [eq].
-    rewrite carry_mul_rep by reflexivity.
-    rewrite mul_rep; reflexivity.
-  + intros; rewrite carry_sub_correct, carry_sub_opt_correct;
-    apply carry_sub_rep.
-  + intros; rewrite carry_add_correct, carry_add_opt_correct;
-    apply carry_add_rep.
-  + intros; rewrite inv_correct, inv_opt_correct; reflexivity.
-  + intros; rewrite carry_opp_correct, carry_opp_opt_correct;
-    apply carry_opp_rep.
+Definition field25519 : @field fe25519 eq zero_ one_ opp add sub mul inv div := proj1 field25519_and_homomorphisms.
+
+Lemma carry_field25519_and_homomorphisms
+  : @field fe25519 eq zero_ one_ carry_opp carry_add carry_sub mul inv div
+    /\ @Ring.is_homomorphism
+         (F modulus) Logic.eq F.one F.add F.mul
+         fe25519 eq one_ carry_add mul encode
+    /\ @Ring.is_homomorphism
+         fe25519 eq one_ carry_add mul
+         (F modulus) Logic.eq F.one F.add F.mul
+         decode.
+Proof.
+  eapply @Field.field_and_homomorphism_from_redundant_representation.
+  { exact (F.field_modulo _). }
+  { apply encode_rep. }
+  { reflexivity. }
+  { reflexivity. }
+  { reflexivity. }
+  { intros; rewrite carry_opp_correct, carry_opp_opt_correct, carry_opp_rep; apply opp_rep; reflexivity. }
+  { intros; rewrite carry_add_correct, carry_add_opt_correct, carry_add_rep; apply add_rep; reflexivity. }
+  { intros; rewrite carry_sub_correct, carry_sub_opt_correct, carry_sub_rep; apply sub_rep; reflexivity. }
+  { intros; rewrite mul_correct, carry_mul_opt_correct by reflexivity; apply carry_mul_rep; reflexivity. }
+  { intros; rewrite inv_correct, inv_opt_correct by reflexivity; apply inv_rep; reflexivity. }
+  { intros; apply encode_rep. }
 Qed.
 
+Definition carry_field25519 : @field fe25519 eq zero_ one_ carry_opp carry_add carry_sub mul inv div := proj1 carry_field25519_and_homomorphisms.
+
 Lemma homomorphism_F25519 :
   @Ring.is_homomorphism
     (F modulus) Logic.eq F.one F.add F.mul
     fe25519 eq one add mul encode.
-Proof.
-  econstructor.
-  + econstructor; [ | apply encode_Proper].
-    intros; cbv [eq].
-    rewrite add_correct, add_opt_correct, add_rep; apply encode_rep.
-  + intros; cbv [eq].
-    rewrite mul_correct, carry_mul_opt_correct, carry_mul_rep
-      by auto using k_subst, c_subst, encode_rep.
-    apply encode_rep.
-  + reflexivity.
-Qed.
+Proof. apply field25519_and_homomorphisms. Qed.
+
 
 Lemma homomorphism_carry_F25519 :
   @Ring.is_homomorphism
     (F modulus) Logic.eq F.one F.add F.mul
     fe25519 eq one carry_add mul encode.
-Proof.
-  econstructor.
-  + econstructor; [ | apply encode_Proper].
-    intros; cbv [eq].
-    rewrite carry_add_correct, carry_add_opt_correct, carry_add_rep, add_rep; apply encode_rep.
-  + intros; cbv [eq].
-    rewrite mul_correct, carry_mul_opt_correct, carry_mul_rep
-      by auto using k_subst, c_subst, encode_rep.
-    apply encode_rep.
-  + reflexivity.
-Qed.
+Proof. apply carry_field25519_and_homomorphisms. Qed.
 
 Definition ge_modulus_sig (f : fe25519) :
   { b : Z | b = ge_modulus_opt (to_list 10 f) }.
@@ -679,4 +672,4 @@ Definition unpack (f : wire_digits) : fe25519 :=
 
 Definition unpack_correct (f : wire_digits)
   : unpack f = unpack_opt params25519 wire_widths_nonneg bits_eq f
-  := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f).
\ No newline at end of file
+  := Eval cbv beta iota delta [proj2_sig pack_sig] in proj2_sig (unpack_sig f).
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index 5f8972c8f..50ddcdb44 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -217,6 +217,8 @@ Proof.
   exact (proj2_sig sqrtW_sig f').
 Qed.
 
+
+
 Definition add (f g : fe25519) : fe25519.
 Proof. define_binop f g addW addW_correct_and_bounded. Defined.
 Definition sub (f g : fe25519) : fe25519.
@@ -258,38 +260,33 @@ Proof. op_correct_t sqrt sqrtW_correct_and_bounded. Qed.
 
 Import Morphisms.
 
-Lemma field25519 : @field fe25519 eq zero one opp add sub mul inv div.
+Local Existing Instance prime_modulus.
+
+Lemma field25519_and_homomorphisms
+  : @field fe25519 eq zero one opp add sub mul inv div
+    /\ @Ring.is_homomorphism (F _) (@Logic.eq _) 1%F F.add F.mul fe25519 eq one add mul encode
+    /\ @Ring.is_homomorphism fe25519 eq one add mul (F _) (@Logic.eq _) 1%F F.add F.mul decode.
 Proof.
-  assert (Reflexive eq) by (repeat intro; reflexivity).
-  eapply (Field.field_from_redundant_representation
-            (fieldF:=Specific.GF25519.carry_field25519)
-            (phi':=proj1_fe25519)).
+  eapply @Field.field_and_homomorphism_from_redundant_representation.
+  { exact (F.field_modulo _). }
+  { cbv [decode encode]; intros; rewrite !proj1_fe25519_exist_fe25519; apply encode_rep. }
   { reflexivity. }
   { reflexivity. }
   { reflexivity. }
-  { intros; rewrite opp_correct; reflexivity. }
-  { intros; rewrite add_correct; reflexivity. }
-  { intros; rewrite sub_correct; reflexivity. }
-  { intros; rewrite mul_correct; reflexivity. }
-  { intros; rewrite inv_correct; reflexivity. }
-  { cbv [div]; intros; rewrite proj1_fe25519_exist_fe25519; reflexivity. }
+  { cbv [decode encode]; intros; rewrite opp_correct, carry_opp_correct, carry_opp_opt_correct, carry_opp_rep; apply opp_rep; reflexivity. }
+  { cbv [decode encode]; intros; rewrite add_correct, carry_add_correct, carry_add_opt_correct, carry_add_rep; apply add_rep; reflexivity. }
+  { cbv [decode encode]; intros; rewrite sub_correct, carry_sub_correct, carry_sub_opt_correct, carry_sub_rep; apply sub_rep; reflexivity. }
+  { cbv [decode encode]; intros; rewrite mul_correct, GF25519.mul_correct, carry_mul_opt_correct by reflexivity; apply carry_mul_rep; reflexivity. }
+  { cbv [decode encode]; intros; rewrite inv_correct, GF25519.inv_correct, inv_opt_correct by reflexivity; apply inv_rep; reflexivity. }
+  { cbv [decode encode div]; intros; rewrite !proj1_fe25519_exist_fe25519; apply encode_rep. }
 Qed.
 
+Definition field25519 : @field fe25519 eq zero one opp add sub mul inv div := proj1 field25519_and_homomorphisms.
+
 Local Opaque proj1_fe25519 exist_fe25519 proj1_fe25519W exist_fe25519W.
 Lemma homomorphism_F25519 :
   @Ring.is_homomorphism
     (F modulus) Logic.eq F.one F.add F.mul
     fe25519 eq one add mul encode.
-Proof.
-  pose proof homomorphism_carry_F25519 as H.
-  destruct H as [ [H0 H1] H2 H3].
-  econstructor; [ econstructor | | ];
-    cbv [eq encode]; repeat intro;
-      rewrite ?add_correct, ?mul_correct, ?proj1_fe25519_exist_fe25519, ?proj1_fe25519_exist_fe25519W, ?proj1_fe25519W_exist_fe25519 in *.
-  { rewrite H0; reflexivity. }
-  { apply H1; assumption. }
-  { rewrite H2; reflexivity. }
-  { reflexivity. }
-Qed.
-
+Proof. apply field25519_and_homomorphisms. Qed.
 (** TODO: pack, unpack, ge_modulus *)