Remove vestigal GaloisField machinery

1 files changed, 0 insertions, 259 deletions

diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v
deleted file mode 100644
index 73eb17549..000000000
--- a/src/Galois/GaloisField.v
+++ /dev/null
@@ -1,259 +0,0 @@
-Require Import BinInt BinNat ZArith Znumtheory.
-Require Import BoolEq Field_theory.
-Require Export Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
-Require Import Crypto.Tactics.VerdiTactics.
-
-(* This file is for the actual field tactics and some specialized
- * morphisms that help field operate.
- *
- * When you want a Galois Field, this is the /only module/ you
- * should import, because it automatically pulls in everything
- * from Galois and the Modulus.
- *)
-Module GaloisField (M: Modulus).
-  Module G := Galois M.
-  Module T := GaloisTheory M.
-  Export M G T.
-
-  (* Define a "ring morphism" between GF and Z, i.e. an equivalence
-   * between 'inject (ZFunction (X))' and 'GFFunction (inject (X))'.
-   *
-   * Doing this allows us to do our coefficient manipulations in Z
-   * rather than GF, because we know it's equivalent to inject the
-   * result afterward.
-   *)
-  Lemma GFring_morph:
-      ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq
-                 0%Z    1%Z   Zplus  Zmult  Zminus  Zopp  Zeq_bool
-                 inject.
-  Proof.
-    constructor; intros; try galois;
-      try (apply gf_eq; simpl; intuition).
-
-    apply Zmod_small; destruct modulus; simpl;
-      apply prime_ge_2 in p; intuition.
-
-    replace (- (x mod modulus)) with (0 - (x mod modulus));
-      try rewrite Zminus_mod_idemp_r; trivial.
-
-    replace x with y; intuition.
-      symmetry; apply Zeq_bool_eq; trivial.
-  Qed.
-
-  (* Redefine our division theory under the ring morphism *)
-  Lemma GFmorph_div_theory: 
-      div_theory eq Zplus Zmult inject Z.quotrem.
-  Proof.
-    constructor; intros; intuition.
-    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
-      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
-
-    eq_remove_proofs; demod;
-      rewrite <- (Z.quot_rem' a b);
-      destruct a; simpl; trivial.
-  Qed.
-
-  (* Some simple utility lemmas *)
-  Lemma injectZeroIsGFZero :
-    GFzero = inject 0.
-  Proof.
-    apply gf_eq; simpl; trivial.
-  Qed.
-
-  Lemma injectOneIsGFOne :
-    GFone = inject 1.
-  Proof.
-    apply gf_eq; simpl; intuition.
-    symmetry; apply Zmod_small; destruct modulus; simpl;
-      apply prime_ge_2 in p; intuition.
-  Qed.
-
-  Lemma divOneIsX :
-    forall (x: GF), (x / 1)%GF = x.
-  Proof.
-    intros; unfold GFdiv.
-
-    replace (GFinv 1)%GF with 1%GF by (
-      replace (GFinv 1)%GF with (GFinv 1 * 1)%GF by ring;
-      rewrite GF_multiplicative_inverse; intuition).
-
-    ring.
-  Qed.
-
-  Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
-  Proof.
-    intuition; solve_by_inversion.
-  Qed.
-
-  (* Change all GFones to (inject 1) and GFzeros to (inject 0) so that
-   * we can use our ring morphism to simplify them
-   *)
-  Ltac GFpreprocess :=
-    repeat rewrite injectZeroIsGFZero;
-    repeat rewrite injectOneIsGFOne.
-
-  (* Split up the equation (because field likes /\, then
-   * change back all of our GFones and GFzeros.
-   *
-   * TODO (adamc): what causes it to generate these subproofs?
-   *)
-  Ltac GFpostprocess :=
-    repeat split;
-
-    repeat match goal with
-    | [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
-      replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
-    end;
-
-    repeat rewrite <- injectZeroIsGFZero;
-    repeat rewrite <- injectOneIsGFOne;
-    repeat rewrite divOneIsX.
-
-  (* Tactic to passively convert from GF to Z in special circumstances *)
-  Ltac GFconstant t :=
-    match t with
-    | inject ?x => x
-    | _ => NotConstant
-    end.
-
-  (* Add our ring with all the fixin's *)
-  Add Ring GFring_Z : GFring_theory
-    (morphism GFring_morph,
-     constants [GFconstant],
-     div GFmorph_div_theory,
-     power_tac GFpower_theory [GFexp_tac]). 
-
-  (* Add our field with all the fixin's *)
-  Add Field GFfield_Z : GFfield_theory
-    (morphism GFring_morph,
-     preprocess [GFpreprocess],
-     postprocess [GFpostprocess],
-     constants [GFconstant],
-     div GFmorph_div_theory,
-     power_tac GFpower_theory [GFexp_tac]). 
-
-  Local Open Scope GF_scope.
-
-  Lemma GF_mul_eq : forall x y z, z <> 0 -> x * z = y * z -> x = y.
-  Proof.
-    intros ? ? ? z_nonzero mul_z_eq.
-    replace x with (x * 1) by field.
-    rewrite <- (GF_multiplicative_inverse z_nonzero).
-    replace (x * (GFinv z * z)) with ((x * z) * GFinv z) by ring.
-    rewrite mul_z_eq.
-    replace (y * z * GFinv z) with (y * (GFinv z * z)) by ring.
-    rewrite GF_multiplicative_inverse; auto; field.
-  Qed.
-
-  Lemma GF_mul_0_l : forall x, 0 * x = 0.
-  Proof.
-    intros; field.
-  Qed.
-
-  Lemma GF_mul_0_r : forall x, x * 0 = 0.
-  Proof.
-    intros; field.
-  Qed.
-
-  Definition GF_eq_dec : forall x y : GF, {x = y} + {x <> y}.
-    intros.
-    assert (H := Z.eq_dec (inject x) (inject y)).
-
-    destruct H.
-    
-    - left; galois; intuition.
-
-    - right; intuition.
-      rewrite H in n.
-      assert (y = y); intuition.
-  Qed.
-
-    Lemma mul_nonzero_l : forall a b, a*b <> 0 -> a <> 0.
-    intros; intuition; subst.
-    assert (0 * b = 0) by field; intuition.
-  Qed.
-
-  Lemma mul_nonzero_r : forall a b, a*b <> 0 -> b <> 0.
-    intros; intuition; subst.
-    assert (a * 0 = 0) by field; intuition.
-  Qed.
-
-  Lemma mul_zero_why : forall a b, a*b = 0 -> a = 0 \/ b = 0.
-    intros.
-    assert (Z := GF_eq_dec a 0); destruct Z.
-
-    - left; intuition.
-
-    - assert (a * b / a = 0) by
-        ( rewrite H; field; intuition ).
-
-      field_simplify in H0.
-      replace (b/1) with b in H0 by (field; intuition).
-      right; intuition.
-      apply n in H0; intuition.
-  Qed.
-
-  Lemma mul_nonzero_nonzero : forall a b, a <> 0 -> b <> 0 -> a*b <> 0.
-    intros; intuition; subst.
-    apply mul_zero_why in H1.
-    destruct H1; subst; intuition.
-  Qed.
-  Hint Resolve mul_nonzero_nonzero.
-
-  Lemma GFexp_distr_mul : forall x y 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; [ field | | 
-      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 (GFexp_pred x) by apply N.neq_succ_0.
-    rewrite (GFexp_pred y) by apply N.neq_succ_0.
-    rewrite (GFexp_pred (x * y)) by apply N.neq_succ_0.
-    rewrite N.pred_succ.
-    rewrite <- IHz'.
-    field.
-  Qed.
-
-  Lemma GF_square_mul : forall x y z, (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. {
-      unfold GFdiv, GFexp, GFexp'.
-      replace (GFinv (y * y)) with (GFinv y * GFinv y); try ring.
-      unfold GFinv.
-      destruct (N.eq_dec (N.pred (totientToN totient)) 0) as [ eq_zero | neq_zero ];
-        [ rewrite eq_zero | rewrite GFexp_distr_mul ]; try field.
-      simpl.
-      do 2 rewrite <- Z2N.inj_pred.
-      replace 0%N with (Z.to_N 0%Z) by auto.
-      apply Z2N.inj_le; modulus_bound.
-    }
-    assert (y ^ 2 <> 0) as y2_nonzero by (apply mul_nonzero_nonzero; auto).
-    rewrite (GF_mul_eq _ z (y ^ 2)); auto.
-    unfold GFdiv.
-    rewrite <- A.
-    field; auto.
-  Qed.
-
-  Lemma sqrt_solutions : forall x y, y ^ 2 = x ^ 2 -> y = x \/ y = GFopp x.
-  Proof.
-    intros.
-    (* TODO(jadep) *)
-  Admitted.
-
-  Lemma GFopp_swap : forall x y, GFopp x = y <-> x = GFopp y.
-  Proof.
-    split; intro; subst; field.
-  Qed.
-
-  Lemma GFopp_involutive : forall x, GFopp (GFopp x) = x.
-  Proof.
-    intros; field.
-  Qed.
-
-End GaloisField.