port several theorems from GF to F

4 files changed, 150 insertions, 33 deletions

diff --git a/src/CompleteEwardsCurve/Pre.v b/src/CompleteEwardsCurve/Pre.v
index d66ed8fab..27f7619dc 100644
--- a/src/CompleteEwardsCurve/Pre.v
+++ b/src/CompleteEwardsCurve/Pre.v
@@ -1,17 +1,26 @@
 Require Import BinInt Znumtheory VerdiTactics.
 
 Require Import Crypto.Spec.ModularArithmetic.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Local Open Scope F_scope.
   
 Section Pre.
-  Context {p : BinInt.Z}.
-  Context {a : F p}.
-  Context {d : F p}.
-  Context {modulus_prime : Znumtheory.prime p}.
-  Context {modulus_lt_2 : 2 < p}.
+  Context {q : BinInt.Z}.
+  Context {a : F q}.
+  Context {d : F q}.
+  Context {prime_q : Znumtheory.prime q}.
+  Context {two_lt_q : 2 < q}.
   Context {a_nonzero : a <> 0}.
   Context {a_square : exists sqrt_a, sqrt_a^2 = a}.
   Context {d_nonsquare : forall x, x^2 <> d}.
+
+  Add Field Ffield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
   
   (* the canonical definitions are in Spec *)
   Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
@@ -21,10 +30,10 @@ Section Pre.
     (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
   ).
   
-  Lemma char_gt_2 : ZToField 2 <> (0: F p).
+  Lemma char_gt_2 : ZToField 2 <> (0: F q).
     intro; find_injection.
-    pose proof modulus_lt_2.
-    rewrite (Z.mod_small 2 p), Z.mod_0_l in *; omega.
+    pose proof two_lt_q.
+    rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega.
   Qed.
   
   (*
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 9bbaac489..f4d3b87ff 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -309,42 +309,84 @@ Section RingModuloPre.
     Fdefn.
   Qed.
 End RingModuloPre.
+  
+Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end.
+Ltac Fexp_tac t := Ncst t.
+Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1.
+Ltac Fpostprocess := repeat split;
+  repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] =>
+    change (exist a b (Pre.Z_mod_mod x)) with (@ZToField q x%Z) end;
+  rewrite ?ZToField_0, ?ZToField_1.
 
 Module Type Modulus.
   Parameter modulus : Z.
 End Modulus.
 
+(* Example of how to instantiate the ring tactic *)
 Module RingModulo (Export M : Modulus).
-  (* Add our ring with all the fixin's *)
   Definition ring_theory_modulo := @Fring_theory modulus.
   Definition ring_morph_modulo := @Fring_morph modulus.
   Definition morph_div_theory_modulo := @Fmorph_div_theory modulus.
   Definition power_theory_modulo := @Fpower_theory modulus.
-
-  Ltac Fexp_tac t := Ncst t.
-
-  (* Expose the carrier in constants so field can simplify them *)
-  Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1.
-
-  (* Split up the equation (because field likes /\, then
-   * change back all of our GFones and GFzeros. *)
-  Ltac Fpostprocess :=
-    repeat split;
-		repeat match goal with [ |- context[exist ?a ?b (Pre.Z_mod_mod ?x ?q)] ] =>
-			replace (exist a b (Pre.Z_mod_mod x)) with (@ZToField q x%Z) by reflexivity
-		end;
-    rewrite ?ZToField_0, ?ZToField_1.
-
-  (* Tactic to passively convert from GF to Z in special circumstances *)
-  Ltac Fconstant t :=
-    match t with
-    | @ZToField _ ?x => x
-    | _ => NotConstant
-    end.
   
   Add Ring GFring_Z : ring_theory_modulo
     (morphism ring_morph_modulo,
      constants [Fconstant],
      div morph_div_theory_modulo,
      power_tac power_theory_modulo [Fexp_tac]). 
-End RingModulo.
\ No newline at end of file
+End RingModulo.
+
+Section VariousModulo.
+  Context {m:Z}.
+  
+  Add Ring GFring_Z : (@Fring_theory m)
+    (morphism (@Fring_morph m),
+     constants [Fconstant],
+     div (@Fmorph_div_theory m),
+     power_tac (@Fpower_theory m) [Fexp_tac]). 
+
+  Lemma F_mul_0_l : forall x : F m, 0 * x = 0.
+  Proof.
+    intros; ring.
+  Qed.
+  
+  Lemma F_mul_0_r : forall x : F m, x * 0 = 0.
+  Proof.
+    intros; ring.
+  Qed.
+  
+  Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0.
+    intros; intuition; subst.
+    assert (0 * b = 0) by ring; intuition.
+  Qed.
+  
+  Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0.
+    intros; intuition; subst.
+    assert (a * 0 = 0) by ring; intuition.
+  Qed.
+  
+  Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N ->
+    (x ^ z) * (y ^ z) = (x * y) ^ z.
+  Proof.
+    intros.
+    replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
+    apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | 
+      replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
+    intros z' z'_nonneg IHz'.
+    rewrite Z2N.inj_succ by auto.
+    rewrite <-N.add_1_l.
+    rewrite !(proj2 (@F_pow_spec m _) _).
+    rewrite <- IHz'.
+    ring.
+  Qed.
+  
+  Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y.
+  Proof.
+    split; intro; subst; ring.
+  Qed.
+
+  Lemma F_opp_involutive : forall x : F m, opp (opp x) = x.
+  Proof.
+    intros; ring.
+  Qed.
+End VariousModulo.
\ No newline at end of file
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 4cdd1192e..b652a8e84 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -48,4 +48,69 @@ Module FieldModulo (Import M : PrimeModulus).
      constants [Fconstant],
      div morph_div_theory_modulo,
      power_tac power_theory_modulo [Fexp_tac]). 
-End FieldModulo.
\ No newline at end of file
+End FieldModulo.
+
+Section VariousModPrime.
+  Context {q:Z} {prime_q:prime q}.
+  Local Open Scope F_scope.
+  Add Field Ffield_Z : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+  
+  Lemma Fq_mul_eq : forall x y z : F q, z <> 0 -> x * z = y * z -> x = y.
+  Proof.
+    intros ? ? ? z_nonzero mul_z_eq.
+    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.
+    replace (x * 1) with x in H by field.
+    replace (y * 1) with y in H by field.
+    trivial.
+  Qed.
+  
+  Lemma Fq_mul_zero_why : forall a b : F q, a*b = 0 -> a = 0 \/ b = 0.
+    intros.
+    assert (Z := F_eq_dec a 0); destruct Z.
+  
+    - left; intuition.
+  
+    - assert (a * b / a = 0) by
+        ( rewrite H; field; intuition ).
+  
+      replace (a*b/a) with (b) in H0 by (field; trivial).
+      right; intuition.
+  Qed.
+  
+  Lemma Fq_mul_nonzero_nonzero : forall a b : F q, a <> 0 -> b <> 0 -> a*b <> 0.
+    intros; intuition; subst.
+    apply Fq_mul_zero_why in H1.
+    destruct H1; subst; intuition.
+  Qed.
+  Hint Resolve Fq_mul_nonzero_nonzero.
+  
+  Lemma F_square_mul : forall x y z : F q, (y <> 0) ->
+    x ^ 2 = z * y ^ 2 -> exists sqrt_z, sqrt_z ^ 2 = z.
+  Proof.
+    intros ? ? ? y_nonzero A.
+    exists (x / y).
+    assert ((x / y) ^ 2 = x ^ 2 / y ^ 2) as square_distr_div by (field; trivial).
+    assert (y ^ 2 <> 0) as y2_nonzero by (
+      change (2%N) with (1+(1+0))%N;
+      rewrite !(proj2 (@F_pow_spec q _) _), !(proj1 (@F_pow_spec q _));
+      auto 10 using Fq_mul_nonzero_nonzero, Fq_1_neq_0).
+    rewrite (Fq_mul_eq _ z (y ^ 2)); auto.
+    rewrite <- A.
+    field; trivial.
+  Qed.
+  
+  Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
+  Proof.
+    intros.
+    (* TODO(jadep) *)
+  Admitted.
+End VariousModPrime.
\ No newline at end of file
diff --git a/src/Specific/EdDSA25519.v b/src/Specific/EdDSA25519.v
index 96f997180..6403c8b53 100644
--- a/src/Specific/EdDSA25519.v
+++ b/src/Specific/EdDSA25519.v
@@ -557,7 +557,8 @@ Module EdDSA25519_Params <: EdDSAParams.
      I have so far not managed to unify them. *)
   Lemma point_eq_copy : forall x1 x2 y1 y2, x1 = x2 -> y1 = y2 ->
     forall p1 p2, mkPoint (x1, y1) p1 = mkPoint (x2, y2) p2.
-  Admitted.
+    apply Facts.point_eq.
+  Qed.
 
   Lemma point_encoding_valid : forall p, point_dec (point_enc p) = Some p.
   Proof.