prove existance of F inv, implement pow -- CompleteEdwardsCurve.unifiedAdd Closed Under Global Context

4 files changed, 264 insertions, 27 deletions

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index e23288e49..7501bfa23 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -6,6 +6,14 @@ Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *
 Require Import Coq.Classes.Morphisms Setoid.
 Require Export Ring_theory Field_theory Field_tac.
 
+Theorem F_eq: forall {m} (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
+Proof.
+  destruct x, y; intuition; simpl in *; try congruence.
+  subst_max.
+  f_equal.
+  eapply UIP_dec, Z.eq_dec.
+Qed.
+
 Lemma F_opp_spec : forall {m} (a:F m), add a (opp a) = ZToField 0.
   intros m a.
   pose (@opp_with_spec m) as H.
@@ -13,12 +21,13 @@ Lemma F_opp_spec : forall {m} (a:F m), add a (opp a) = ZToField 0.
   destruct H; eauto.
 Qed.
 
-Theorem F_eq: forall {m} (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
+Lemma F_pow_spec : forall {m} (a:F m),
+    pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x).
 Proof.
-  destruct x, y; intuition; simpl in *; try congruence.
-  subst_max.
-  f_equal.
-  eapply UIP_dec, Z.eq_dec.
+  intros m a.
+  pose (@pow_with_spec m) as H.
+  change (@pow m) with (proj1_sig H). 
+  destruct H; eauto.
 Qed.
 
 (* Fails iff the input term does some arithmetic with mod'd values. *)
@@ -165,7 +174,16 @@ Section FandZ.
 
   Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m ->
                                      b mod m =  (- a)  mod m.
-  Admitted.
+  Proof.
+    rewrite <-Z.sub_0_l; intros.
+    replace (0-a)%Z with (b-(a + b))%Z by omega.
+    rewrite Zminus_mod.
+    rewrite <- H.
+    rewrite Zmod_0_l.
+    replace (b mod m - 0)%Z with (b mod m) by omega.
+    rewrite Zmod_mod.
+    reflexivity.
+  Qed.
 
   Lemma FieldToZ_opp' : forall x, FieldToZ (@opp m x) mod m = -x mod m.
   Proof.
@@ -260,15 +278,36 @@ Section RingModuloPre.
     constructor; Fdefn.
   Qed.
 
-  Lemma pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.
+  Lemma F_mul_1_r:
+    forall x : F m, x * 1 = x.
+  Proof.
+    Fdefn; rewrite Z.mul_1_r; auto.
+  Qed.
+    
+  Lemma F_mul_assoc:
+    forall x y z : F m, x * (y * z) = x * y * z.
+  Proof.
+    Fdefn.
+  Qed.  
+
+  Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.
   Proof.
-    destruct (F_pow_spec x) as [HO HS].
-  Admitted.
+    destruct (F_pow_spec x) as [HO HS]; intros.
+    destruct n; auto; unfold id.
+    rewrite Pre.N_pos_1plus at 1.
+    rewrite HS.
+    simpl.
+    induction p using Pos.peano_ind.
+    - simpl. rewrite HO; apply F_mul_1_r.
+    - rewrite (@pow_pos_succ (F m) (@mul m) eq _ _ F_mul_assoc x).
+      rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS.
+      f_equal.
+  Qed.
 
   (***** Power theory *****)
   Lemma Fpower_theory : power_theory 1%F (@mul m) eq id (@pow m).
   Proof.
-    constructor; apply pow_pow_N.
+    constructor; apply F_pow_pow_N.
   Qed.
 
   (***** Division Theory *****)
@@ -284,8 +323,16 @@ Section RingModuloPre.
     Fdefn; rewrite <-Z.quot_rem'; trivial.
   Qed.
 
+  Lemma Z_opp_opp : forall x : Z, (-(-x)) = x.
+    destruct x; auto.
+  Qed.
+
   Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m.
-  Admitted.
+    intros.
+    apply Pre.mod_opp_equiv.
+    rewrite Z_opp_opp.
+    demod; auto.
+  Qed.
 
   (* Define a "ring morphism" between GF and Z, i.e. an equivalence
    * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
@@ -426,11 +473,6 @@ Section VariousModulo.
     intros; ring.
   Qed.
 
-  Lemma F_mul_1_r : forall x : F m, (x * 1)%F = x.
-  Proof.
-    intros; ring.
-  Qed.
-
   Lemma F_mul_1_l : forall x : F m, (1 * x)%F = x.
   Proof.
     intros; ring.
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v
index c313bfcea..c6d1ca911 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/ModularArithmetic/Pre.v
@@ -1,6 +1,7 @@
-Require Import Znumtheory BinInt BinNums.
+Require Import BinInt BinNat BinNums Zdiv Znumtheory.
 Require Import Eqdep_dec.
 Require Import EqdepFacts.
+Require Import Crypto.Tactics.VerdiTactics.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
   symmetry.
@@ -13,7 +14,11 @@ Lemma exist_reduced_eq: forall (m : Z) (a b : Z), a = b -> forall pfa pfb,
     exist (fun z : Z => z = z mod m) a pfa =
     exist (fun z : Z => z = z mod m) b pfb.
 Proof.
-Admitted.
+  intuition; simpl in *; try congruence.
+  subst_max.
+  f_equal.
+  eapply UIP_dec, Z.eq_dec.
+Qed.
 
 Definition opp_impl:
   forall {m : BinNums.Z},
@@ -36,4 +41,169 @@ Definition opp_impl:
   Grab Existential Variables.
   destruct x; simpl.
   rewrite Zdiv.Zmod_mod; reflexivity.
-Defined.
\ No newline at end of file
+Defined.
+
+Definition mulmod m := fun a b => a * b mod m.
+Definition pow_impl_pos m := Pos.iter_op (mulmod m).
+Definition pow_impl_N m a x := match x with N0 => 1 mod m | Npos p => @pow_impl_pos m p a end.
+  
+Lemma mulmod_assoc:
+  forall m x y z : Z, mulmod m x (mulmod m y z) = mulmod m (mulmod m x y) z.
+Proof.
+  unfold mulmod; intros.
+  rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal.
+  apply Z.mul_assoc.
+Qed.
+
+Lemma pow_impl_N_correct:
+      forall m a : Z,
+        a = a mod m ->
+        forall x : N, pow_impl_N m a (1 + x) = (a * (pow_impl_N m a x mod m)) mod m.
+Proof.
+  intros m a pfa x.
+  rewrite N.add_1_l.
+  cbv beta delta [pow_impl_N N.succ].
+  destruct x; [simpl; rewrite ?Zdiv.Zmult_mod_idemp_r, Z.mul_1_r; auto|].
+  unfold pow_impl_pos.
+  rewrite Pos.iter_op_succ by (apply mulmod_assoc).
+  unfold mulmod.
+  rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal.
+Qed.
+
+Lemma N_pos_1plus : forall p, (N.pos p = 1 + (N.pred (N.pos p)))%N.
+  intros.
+  rewrite <-N.pos_pred_spec.
+  rewrite N.add_1_l.
+  rewrite N.pos_pred_spec.
+  rewrite N.succ_pred; eauto.
+  discriminate.
+Qed.
+
+Definition pow_impl_sig {m} : {z : Z | z = z mod m} -> N -> {z : Z | z = z mod m}.
+  intros a x.
+  exists (pow_impl_N m (proj1_sig a) x).
+  destruct x; [simpl; rewrite Zmod_mod; reflexivity|].
+  rewrite N_pos_1plus.
+  rewrite pow_impl_N_correct.
+  - rewrite Zmod_mod; reflexivity.
+  - destruct a; auto.
+Defined.
+
+Definition pow_impl:
+   forall {m : BinNums.Z},
+   {pow0
+   : {z : BinNums.Z | z = z mod m} -> BinNums.N -> {z : BinNums.Z | z = z mod m}
+   |
+   forall a : {z : BinNums.Z | z = z mod m},
+   pow0 a 0%N =
+   exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m) /\
+   (forall x : BinNums.N,
+    pow0 a (1 + x)%N =
+    exist (fun z : BinNums.Z => z = z mod m)
+      ((proj1_sig a * proj1_sig (pow0 a x)) mod m)
+      (Z_mod_mod (proj1_sig a * proj1_sig (pow0 a x)) m))}.
+  intros m. exists pow_impl_sig.
+  split; [eauto using exist_reduced_eq|]; intros.
+  apply exist_reduced_eq.
+  rewrite pow_impl_N_correct.
+  rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal.
+  destruct a; auto.
+Qed.
+
+Lemma mul_mod_modulus_r : forall x m, (x*m) mod m = 0.
+  intros.
+  rewrite Zmult_mod, Z_mod_same_full.
+  rewrite Z.mul_0_r, Zmod_0_l.
+  reflexivity.
+Qed.
+
+Lemma mod_opp_equiv : forall x y m,  x  mod m = (-y) mod m ->
+                              (-x) mod m =   y  mod m.
+Proof.
+  intros.
+  rewrite <-Z.sub_0_l.
+  rewrite Zminus_mod. rewrite H.
+  rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal.
+  destruct y; auto.
+Qed.
+
+Definition mod_inv_eucl (a m:Z) : Z.
+  destruct (euclid a m). (* [euclid] is opaque. TODO: reimplement? *)
+  exact ((match a with Z0 => Z0 | _ =>
+                                 (match d with Z.pos _ =>  u | _ => -u end)
+          end) mod m).
+Defined.
+  
+Lemma reduced_nonzero_pos:
+  forall a m : Z, m > 0 -> a <> 0 -> a = a mod m -> 0 < a.
+Proof.
+  intros a m m_pos a_nonzero pfa.
+  destruct (Z.eq_dec 0 m); subst_max; try omega.
+  pose proof (Z_mod_lt a m) as H.
+  destruct (Z.eq_dec 0 a); subst_max; try omega.
+Qed.
+
+Lemma mod_inv_eucl_correct : forall a m, a <> 0 -> a = a mod m -> prime m ->
+                                    ((mod_inv_eucl a m) * a) mod m = 1 mod m.
+Proof.
+  intros a m a_nonzero pfa prime_m.
+  pose proof (prime_ge_2 _ prime_m).
+  assert (0 < m) as m_pos by omega.
+  assert (0 <= m) as m_nonneg by omega.
+  assert (0 < a) as a_pos by (eapply reduced_nonzero_pos; eauto; omega).
+  unfold mod_inv_eucl.
+  destruct a as [|a'|a'] eqn:ha; try pose proof (Zlt_neg_0 a') as nnn; try omega; clear nnn.
+  rewrite<- ha in *.
+  lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end.
+  lazymatch goal with [H: Zis_gcd _ _ _ |- _ ] => destruct H end.
+  rewrite Z.add_move_r in e.
+  destruct (Z_mod_lt a m ); try omega; rewrite <- pfa in *.
+  destruct (prime_divisors _ prime_m _ H1) as [Ha|[Hb|[Hc|Hd]]]; subst d.
+  + assert ((u * a) mod m = (-1 - v * m) mod m) as Hx by (f_equal; trivial).
+    rewrite Zminus_mod, mul_mod_modulus_r, Z.sub_0_r, Zmod_mod in Hx.
+    rewrite Zmult_mod_idemp_l.
+    rewrite <-Zopp_mult_distr_l.
+    eauto using mod_opp_equiv.
+  + rewrite Zmult_mod_idemp_l.
+    rewrite e, Zminus_mod, mul_mod_modulus_r, Z.sub_0_r, Zmod_mod; reflexivity.
+  + pose proof (Zdivide_le _ _ m_nonneg a_pos H0); omega.
+  + apply Zdivide_opp_l_rev in H0.
+    pose proof (Zdivide_le _ _ m_nonneg a_pos H0); omega.
+Qed.
+
+Lemma mod_inv_eucl_sig : forall {m}, {z : Z | z = z mod m} -> {z : Z | z = z mod m}.
+  intros m a.
+  exists (mod_inv_eucl (proj1_sig a) m).
+  destruct a; unfold mod_inv_eucl.
+  lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end.
+  rewrite Zmod_mod; reflexivity.
+Defined.
+
+Definition inv_impl :
+   forall {m : BinNums.Z},
+   {inv0 : {z : BinNums.Z | z = z mod m} -> {z : BinNums.Z | z = z mod m} |
+   inv0 (exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m)) =
+   exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m) /\
+   (Znumtheory.prime m ->
+    forall a : {z : BinNums.Z | z = z mod m},
+    a <> exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m) ->
+    exist (fun z : BinNums.Z => z = z mod m)
+      ((proj1_sig a * proj1_sig (inv0 a)) mod m)
+      (Z_mod_mod (proj1_sig a * proj1_sig (inv0 a)) m) =
+    exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))}.
+Proof.
+  intros m. exists mod_inv_eucl_sig. split; intros.
+  - simpl.
+    apply exist_reduced_eq; simpl.
+    unfold mod_inv_eucl; simpl.
+    lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end.
+    auto.
+  - 
+    destruct a.
+    cbv [proj1_sig mod_inv_eucl_sig].
+    rewrite Z.mul_comm.
+    eapply exist_reduced_eq.
+    rewrite mod_inv_eucl_correct; eauto.
+    intro; destruct H0.
+    eapply exist_reduced_eq. congruence.
+Qed.
\ No newline at end of file
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 6a862fb3b..9d086f4fa 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -8,6 +8,15 @@ Require Import Eqdep_dec.
 
 Existing Class prime.
 
+Lemma F_inv_spec : forall {m}, inv 0%F = (0%F : F m)
+      /\ (prime m -> forall a0 : F m, a0 <> 0%F -> (a0 * inv a0)%F = 1%F).
+Proof.
+  intros m.
+  pose (@inv_with_spec m) as H.
+  change (@inv m) with (proj1_sig H).
+  destruct H; eauto.
+Qed.
+
 Section FieldModuloPre.
   Context {q:Z} {prime_q:prime q}.
   Local Open Scope F_scope.
@@ -18,10 +27,17 @@ Section FieldModuloPre.
     rewrite F_eq, !FieldToZ_ZToField, !Zmod_small by omega; congruence.
   Qed.
 
-  Lemma F_mul_inv_l : forall x : F q, inv x * x = 1.
+  Lemma F_mul_inv_r : forall x : F q, x <> 0 -> x * inv x = 1.
+  Proof.
+    intros.
+    edestruct @F_inv_spec; eauto.
+  Qed.
+
+  Lemma F_mul_inv_l : forall x : F q, x <> 0 -> inv x * x = 1.
   Proof.
     intros.
-    rewrite <-(proj1 (F_inv_spec _ x)).
+    edestruct @F_inv_spec as [Ha Hb]; eauto.
+    erewrite <-Hb; eauto.
     Fdefn.
   Qed.
 
@@ -67,7 +83,7 @@ Section VariousModPrime.
     assert (x * z * inv z = y * z * inv z) as H by (rewrite mul_z_eq; reflexivity).
     replace (x * z * inv z) with (x * (z * inv z)) in H by (field; trivial).
     replace (y * z * inv z) with (y * (z * inv z)) in H by (field; trivial).
-    rewrite (proj1 (@F_inv_spec q _ _)) in H.
+    rewrite F_mul_inv_r in H by assumption.
     replace (x * 1) with x in H by field.
     replace (y * 1) with y in H by field.
     trivial.
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index 2f887548f..5f8b9ed38 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -31,16 +31,25 @@ Section FieldOperations.
   Definition add (a b:Fm) : Fm := ZToField (a + b).
   Definition mul (a b:Fm) : Fm := ZToField (a * b).
 
-  Definition opp_with_spec : { opp | forall x, add x (opp x) = 0 } := Pre.opp_impl.
+  Definition opp_with_spec : { opp : Fm -> Fm
+                             | forall x, add x (opp x) = 0
+                             } := Pre.opp_impl.
   Definition opp : F m -> F m := Eval hnf in proj1_sig opp_with_spec.
   Definition sub (a b:Fm) : Fm := add a (opp b).
 
-  Parameter inv : Fm -> Fm. 
-  Axiom F_inv_spec : Znumtheory.prime m -> forall (a:Fm), mul a (inv a) = 1 /\ inv 0 = 0.
+  Definition inv_with_spec : { inv : Fm -> Fm
+                             | inv 0 = 0
+                             /\ ( Znumtheory.prime m ->
+                                 forall (a:Fm), a <> 0 -> mul a (inv a) = 1 )
+                             } := Pre.inv_impl.
+  Definition inv : F m -> F m := Eval hnf in proj1_sig inv_with_spec.
   Definition div (a b:Fm) : Fm := mul a (inv b).
 
-  Parameter pow : Fm -> BinNums.N ->  Fm. 
-  Axiom F_pow_spec : forall a, pow a 0%N = 1 /\ forall x, pow a (1 + x)%N = mul a (pow a x).
+  Definition pow_with_spec : { pow : Fm -> BinNums.N -> Fm
+                             | forall a, pow a 0%N = 1
+                             /\ forall x, pow a (1 + x)%N = mul a (pow a x)
+                             } := Pre.pow_impl.
+  Definition pow : F m -> BinNums.N -> F m := Eval hnf in proj1_sig pow_with_spec.
 End FieldOperations.
 
 Delimit Scope F_scope with F.