proved an admit in field homomorphisms that turned out to be unprovable; I added another precondition and pushed it through everywhere but one place in ExtendedCoordinates, where I was stuck.

4 files changed, 74 insertions, 23 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index cb9103b52..d47fc6acd 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -438,7 +438,7 @@ Module Ring.
     Local Notation "0" := zero. Local Notation "1" := one.
     Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul.
 
-    Lemma mul_0_r : forall x, 0 * x = 0.
+    Lemma mul_0_l : forall x, 0 * x = 0.
     Proof.
       intros.
       assert (0*x = 0*x) as Hx by reflexivity.
@@ -447,7 +447,7 @@ Module Ring.
       rewrite !ring_sub_definition, <-associative, right_inverse, right_identity in Hxx; exact Hxx.
     Qed.
 
-    Lemma mul_0_l : forall x, x * 0 = 0.
+    Lemma mul_0_r : forall x, x * 0 = 0.
     Proof.
       intros.
       assert (x*0 = x*0) as Hx by reflexivity.
@@ -462,7 +462,7 @@ Module Ring.
     Lemma mul_opp_r x y : x * opp y = opp (x * y).
     Proof.
       assert (Ho:x*(opp y) + x*y = 0)
-        by (rewrite <-left_distributive, left_inverse, mul_0_l; reflexivity).
+        by (rewrite <-left_distributive, left_inverse, mul_0_r; reflexivity).
       rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
       rewrite <-!associative, right_inverse, right_identity; reflexivity.
     Qed.
@@ -470,7 +470,7 @@ Module Ring.
     Lemma mul_opp_l x y : opp x * y = opp (x * y).
     Proof.
       assert (Ho:opp x*y + x*y = 0)
-        by (rewrite <-right_distributive, left_inverse, mul_0_r; reflexivity).
+        by (rewrite <-right_distributive, left_inverse, mul_0_l; reflexivity).
       rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
       rewrite <-!associative, right_inverse, right_identity; reflexivity.
     Qed.
@@ -596,8 +596,8 @@ Module IntegralDomain.
     Proof.
       split.
       { intro H0; split; intro H1; apply H0; rewrite H1.
-        { apply Ring.mul_0_r. }
-        { apply Ring.mul_0_l. } }
+        { apply Ring.mul_0_l. }
+        { apply Ring.mul_0_r. } }
       { intros [? ?] ?; edestruct mul_nonzero_nonzero_cases; eauto with nocore. }
     Qed.
 
@@ -619,10 +619,15 @@ Module Field.
     Local Notation "0" := zero. Local Notation "1" := one.
     Local Infix "+" := add. Local Infix "*" := mul.
 
+    Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one.
+    Proof.
+      intros. rewrite commutative. auto using left_multiplicative_inverse.
+    Qed.
+
     Global Instance is_mul_nonzero_nonzero : @is_mul_nonzero_nonzero T eq 0 mul.
     Proof.
       constructor. intros x y Hx Hy Hxy.
-      assert (0 = (inv y * (inv x * x)) * y) as H00. (rewrite <-!associative, Hxy, !Ring.mul_0_l; reflexivity).
+      assert (0 = (inv y * (inv x * x)) * y) as H00. (rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity).
       rewrite left_multiplicative_inverse in H00 by assumption.
       rewrite right_identity in H00.
       rewrite left_multiplicative_inverse in H00 by assumption.
@@ -634,6 +639,16 @@ Module Field.
       split; auto using field_commutative_ring, field_domain_is_zero_neq_one, is_mul_nonzero_nonzero.
     Qed.
 
+    Lemma inv_unique x ix : ix * x = one -> ix = inv x.
+    Proof.
+      intro Hix.
+      assert (ix*x*inv x = inv x).
+      - rewrite Hix, left_identity; reflexivity.
+      - rewrite <-associative, right_multiplicative_inverse, right_identity in H0; trivial.
+        intro eq_x_0. rewrite eq_x_0, Ring.mul_0_r in Hix.
+        apply zero_neq_one. assumption.
+    Qed.
+
     Require Coq.setoid_ring.Field_theory.
     Lemma field_theory_for_stdlib_tactic : Field_theory.field_theory 0 1 add mul sub opp div inv eq.
     Proof.
@@ -714,7 +729,6 @@ Module Field.
   Proof.
     repeat split; eauto with core typeclass_instances; intros;
       repeat rewrite ?EQ_opp, ?EQ_inv, ?EQ_add, ?EQ_sub, ?EQ_mul, ?EQ_div, ?EQ_zero, ?EQ_one;
-
       auto using (associative (op := add)), (commutative (op := add)), (left_identity (op := add)), (right_identity (op := add)),
                  (associative (op := mul)), (commutative (op := mul)), (left_identity (op := mul)), (right_identity (op := mul)),
                  left_inverse, right_inverse, (left_distributive (add := add)), (right_distributive (add := add)),
@@ -734,12 +748,39 @@ Module Field.
     Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
     Context `{@Ring.is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}.
 
-    Lemma homomorphism_multiplicative_inverse : forall x, phi (INV x) = inv (phi x). Admitted.
+    Lemma homomorphism_multiplicative_inverse_complete
+       : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x))
+       -> phi (INV x) = inv (phi x).
+    Proof.
+      intros.
+      destruct (eq_dec x ZERO); auto.
+      assert (phi (MUL (INV x) x) = one) as A. {
+        rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one.
+      }
+      rewrite Ring.homomorphism_mul in A.
+      apply inv_unique in A. assumption.
+    Qed.
 
-    Lemma homomorphism_div : forall x y, phi (DIV x y) = div (phi x) (phi y).
+    Lemma homomorphism_multiplicative_inverse
+      : forall x, not (EQ x ZERO)
+      -> phi (INV x) = inv (phi x).
+    Proof.
+      intros. apply homomorphism_multiplicative_inverse_complete. contradiction.
+    Qed.
+
+    Lemma homomorphism_div_complete
+      : forall x y, (EQ y ZERO -> phi (INV y) = inv (phi y))
+      -> phi (DIV x y) = div (phi x) (phi y).
     Proof.
       intros. rewrite !field_div_definition.
-      rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse. reflexivity.
+      rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete. reflexivity. trivial.
+    Qed.
+
+    Lemma homomorphism_div
+      : forall x y, not (EQ y ZERO)
+      -> phi (DIV x y) = div (phi x) (phi y).
+    Proof.
+      intros. apply homomorphism_div_complete. contradiction.
     Qed.
   End Homomorphism.
 End Field.
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index a160d8dab..1d8b730cb 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -124,19 +124,20 @@ Module E.
       Qed.
     End PointCompression.
   End CompleteEdwardsCurveTheorems.
-
   Section Homomorphism.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd}
-            {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}.
     Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd}
-            {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
+            {fieldK: @Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
             {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}.
     Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul
                                                    K Keq Kone Kadd Kmul phi}.
     Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}.
-    Local Notation Fpoint := (@point F Feq Fone Fadd Fmul Fa Fd).
-    Local Notation Kpoint := (@point K Keq Kone Kadd Kmul Ka Kd).
+    Local Notation Fpoint := (@E.point F Feq Fone Fadd Fmul Fa Fd).
+    Local Notation Kpoint := (@E.point K Keq Kone Kadd Kmul Ka Kd).
+    Local Notation FonCurve := (@onCurve F Feq Fone Fadd Fmul Fa Fd).
+    Local Notation KonCurve := (@onCurve K Keq Kone Kadd Kmul Ka Kd).
 
     Create HintDb field_homomorphism discriminated.
     Hint Rewrite <-
@@ -149,6 +150,7 @@ Module E.
          Hd
       : field_homomorphism.
 
+    Obligation Tactic := idtac.
     Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ (
       let (x, y) := coordinates P in (phi x, phi y)) _.
     Next Obligation.
@@ -159,7 +161,7 @@ Module E.
 
     Context {point_phi:Fpoint->Kpoint}
             {point_phi_Proper:Proper (eq==>eq) point_phi}
-            {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}.
+            {point_phi_correct: forall (P:point), eq (point_phi P) (ref_phi P)}.
 
     Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi.
     Proof.
@@ -174,7 +176,11 @@ Module E.
              | |- Keq ?x ?x => reflexivity
              | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism
              | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition]
-             end.
+             end;
+        assert (FonCurve (f1,f2)) as FonCurve1 by assumption;
+        assert (FonCurve (f,f0)) as FonCurve2 by assumption;
+        [ eapply (@edwardsAddCompleteMinus F) with (x1 := f1); destruct Fprm; eauto
+        | eapply (@edwardsAddCompletePlus  F) with (x1 := f1); destruct Fprm; eauto].
       Qed.
   End Homomorphism.
 End E.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index d8efb82f3..f3820aeac 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -205,6 +205,8 @@ Module Extended.
     Context {Hd:Keq (phi Fd) Kd} {Kdd Fdd} {HKdd:Keq Kdd (Kadd Kd Kd)} {HFdd:Feq Fdd (Fadd Fd Fd)}.
     Local Notation Fpoint := (@point F Feq Fzero Fone Fadd Fmul Fdiv Fa Fd).
     Local Notation Kpoint := (@point K Keq Kzero Kone Kadd Kmul Kdiv Ka Kd).
+    Local Notation FonCurve := (@onCurve F Feq Fone Fadd Fmul Fa Fd).
+    Local Notation KonCurve := (@onCurve K Keq Kone Kadd Kmul Ka Kd).
 
     Lemma Ha : Keq (phi Fa) Ka.
     Proof. rewrite HFa, HKa, <-homomorphism_one. eapply homomorphism_opp. Qed.
@@ -228,7 +230,7 @@ Module Extended.
       let '(X, Y, Z, T) := coordinates P in (phi X, phi Y, phi Z, phi T)) _.
     Next Obligation.
       destruct P as [[[[] ?] ?] [? [? ?]]]; unfold onCurve in *; simpl.
-      rewrite_strat bottomup hints field_homomorphism.
+      (rewrite_strat bottomup hints field_homomorphism); try assumption.
       eauto 10 using is_homomorphism_phi_proper, phi_nonzero.
     Qed.
 
@@ -250,6 +252,6 @@ Module Extended.
              | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism
              | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition]
              end.
-    Qed.
+      Admitted. (* TODO(jadep or andreser) *)
   End Homomorphism.
 End Extended.
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index c74e9a321..76dd97c72 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -100,14 +100,16 @@ Section RespectsFieldHomomorphism.
        d_ok
        : field_homomorphism.
 
-  Lemma morphism_unidiedAdd' : forall P Q:F*F,
+  Lemma morphism_unifiedAdd' : forall P Q:F*F,
+    (~ EQ (ADD ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) ->
+    (~ EQ (SUB ONE (MUL (MUL (MUL (MUL D (fst P)) (fst Q)) (snd P)) (snd Q))) ZERO) ->
     eqp
       (phip (unifiedAdd'(F:=F)(one:=ONE)(add:=ADD)(sub:=SUB)(mul:=MUL)(div:=DIV)(a:=A)(d:=D) P Q))
             (unifiedAdd'(F:=K)(one:=one)(add:=add)(sub:=sub)(mul:=mul)(div:=div)(a:=a)(d:=d) (phip P) (phip Q)).
   Proof.
-    intros [x1 y1] [x2 y2].
+    intros [x1 y1] [x2 y2] Hnonzero1 Hnonzero2;
     cbv [unifiedAdd' phip eqp];
       apply conj;
-      (rewrite_strat topdown hints field_homomorphism); reflexivity.
+      (rewrite_strat topdown hints field_homomorphism); try assumption; reflexivity.
   Qed.
 End RespectsFieldHomomorphism.