port several theorems from GF to F

1 files changed, 66 insertions, 1 deletions

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