Generalize field_from_redundant_representation

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

1 files changed, 54 insertions, 61 deletions

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).