Basic Galois Field Theory Modules

3 files changed, 328 insertions, 2 deletions

diff --git a/Makefile b/Makefile
index 2799187f6..42fb6aa7c 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
 # © 2015 the Massachusetts Institute of Technology
-# @author bbaren
+# @author bbaren + rsloan
 
 SOURCES := $(shell grep -v '^-' _CoqProject | tr '\n' ' ')
 COQLIBS := $(shell grep '^-' _CoqProject | tr '\n' ' ')
@@ -16,7 +16,7 @@ all: $(SOURCES)
 	@echo "done!"
 
 coquille:
-	vim -c "execute coquille#Launch($(COQLIBS))" -N
+	vim -c "execute coquille#Launch($(COQLIBS))" .
 
 clean:
 	$(RM) $(foreach f,$(SOURCES),$(call coq-generated,$(basename $f)))
diff --git a/src/GaloisField.v b/src/GaloisField.v
new file mode 100644
index 000000000..928eaf702
--- /dev/null
+++ b/src/GaloisField.v
@@ -0,0 +1,94 @@
+
+Require Import BinInt BinNat ZArith Znumtheory.
+Require Import ProofIrrelevance Epsilon.
+
+Definition Prime := {x: Z | prime x}.
+
+Module Type GaloisField.
+
+  Parameter modulus: Prime.
+
+  (* Data type definitions *)
+  Definition primeToZ(x: Prime) := proj1_sig x.
+  Coercion primeToZ: Prime >-> Z.
+
+  Definition GF := {x: Z | exists y, x = y mod modulus}.
+  Definition GFToZ(x: GF) := proj1_sig x.
+
+  Theorem exist_eq: forall (x y: Z) P e1 e2, x = y <-> exist P x e1 = exist P y e2.
+    intros. split.
+      intro H. apply subset_eq_compat; trivial.
+      intro H.
+      assert (proj1_sig (exist P x e1) = proj1_sig (exist P y e2)).
+        rewrite H. trivial.
+      simpl in H0. rewrite H0. trivial.
+  Qed.
+
+  Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y.
+    intros x y. destruct x, y. split; apply exist_eq.
+  Qed.
+
+  Coercion GFToZ: GF >-> Z.
+
+  (* Elementary operations *)
+  Definition GFzero: GF.
+    exists 0. exists 0. trivial.
+  Defined.
+
+  Definition GFone: GF.
+    exists 1. exists 1. symmetry; apply Zmod_small. intuition.
+    destruct modulus; simpl.
+    apply prime_ge_2 in p. intuition.
+  Defined.
+
+  Definition GFplus(x y: GF): GF.
+    exists ((x + y) mod modulus). exists (x + y). trivial.
+  Defined.
+
+  Definition GFminus(x y: GF): GF.
+    exists ((x - y) mod modulus). exists (x - y). trivial.
+  Defined.
+
+  Definition GFmult(x y: GF): GF.
+    exists ((x * y) mod modulus). exists (x * y). trivial.
+  Defined.
+
+  Definition GFopp(x: GF): GF := GFminus GFzero x.
+
+  (* Totient Preliminaries *)
+  Fixpoint GFexp' (x: GF) (power: positive) :=
+    match power with
+    | xH => x
+    | (xO power') => GFexp' (GFmult x x) power'
+    | (xI power') => GFmult x (GFexp' (GFmult x x) power')
+    end.
+
+  Definition GFexp (x: GF) (power: N): GF :=
+    match power with
+    | N0 => GFone
+    | Npos power' => GFexp' x power'
+    end.
+
+  (* Inverses + division derived from the existence of a totient *)
+  Definition isTotient(e: N) := N.gt e 0 /\ forall g, GFexp g e = GFone.
+
+  Definition Totient := {e: N | isTotient e}.
+
+  Theorem fermat_little_theorem: isTotient (N.pred (Z.to_N modulus)).
+  Admitted.
+
+  Definition totient : Totient.
+    apply constructive_indefinite_description.
+    exists (N.pred (Z.to_N modulus)).
+    exact fermat_little_theorem.
+  Defined.
+
+  Definition totientToN(x: Totient) := proj1_sig x.
+  Coercion totientToN: Totient >-> N.
+
+  Definition GFinv(x: GF): GF := GFexp x (N.pred totient).
+
+  Definition GFdiv(x y: GF): GF := GFmult x (GFinv y).
+
+End GaloisField.
+
diff --git a/src/GaloisFieldTheory.v b/src/GaloisFieldTheory.v
new file mode 100644
index 000000000..1a749b027
--- /dev/null
+++ b/src/GaloisFieldTheory.v
@@ -0,0 +1,232 @@
+
+Require Import BinInt BinNat ZArith Znumtheory.
+Require Export Morphisms Setoid Ring_theory Field_theory Field_tac.
+Require Export GaloisField.
+
+Set Implicit Arguments.
+Unset Strict Implicits.
+
+Module Type GaloisFieldTheory.
+  Declare Module Field: GaloisField.
+  Import Field.
+
+  (* Notations *)
+  Notation "x {+} y" := (GFplus x y)   (at level 60, right associativity).
+  Notation "x {-} y" := (GFminus x y)  (at level 60, right associativity).
+  Notation "x {*} y" := (GFmult x y)   (at level 50, left associativity).
+  Notation "x {/} y" := (GFdiv x y)    (at level 50, left associativity).
+  Notation "x {^} y" := (GFexp x y)    (at level 40, left associativity).
+  Notation "{1}"     := GFone.
+  Notation "{0}"     := GFzero.
+
+  (* Basic Properties *)
+
+  Theorem GFplus_0_l: forall x : GF, {0}{+}x = x.
+    intro x. apply gf_eq. unfold GFzero, GFplus, GFToZ; simpl.
+    destruct x. destruct e. simpl. rewrite e.
+    rewrite Zmod_mod. trivial.
+  Qed.
+
+  Theorem GFplus_commutative: forall x y : GF, x{+}y = y{+}x.
+    intros x y. apply gf_eq. unfold GFzero, GFplus, GFToZ; simpl.
+    destruct x. destruct e.
+    destruct y. destruct e0.
+    simpl. rewrite Zplus_comm. rewrite e, e0. trivial.
+  Qed.
+
+  Theorem GFplus_associative: forall x y z : GF, x{+}y{+}z = (x{+}y){+}z.
+    intros x y z. apply gf_eq. unfold GFzero, GFplus, GFToZ; simpl.
+    destruct x. destruct e.
+    destruct y. destruct e0.
+    destruct z. destruct e1.
+    simpl. rewrite Zplus_mod_idemp_l, Zplus_mod_idemp_r, Zplus_assoc. trivial.
+  Qed.
+
+  Theorem GFmult_1_l: forall x : GF, {1}{*}x = x.
+    intro x. apply gf_eq. unfold GFzero, GFmult, GFToZ; simpl.
+    destruct x. destruct e. simpl. rewrite e.
+
+    (* TODO: how do we make this automatic?
+    *        I'd like to case, but we need to keep the mod.*)
+    assert (forall z,
+      match z with
+      | 0 => 0
+      | Z.pos y' => Z.pos y'
+      | Z.neg y' => Z.neg y'
+      end = z).
+      intros; induction z; simpl; intuition.
+
+    rewrite H, Zmod_mod. trivial.
+  Qed.
+
+  Theorem GFmult_commutative: forall x y : GF, x{*}y = y{*}x.
+    intros x y. apply gf_eq. unfold GFzero, GFmult, GFToZ; simpl.
+    destruct x. destruct e.
+    destruct y. destruct e0.
+    simpl. rewrite Zmult_comm. rewrite e, e0. trivial.
+  Qed.
+
+  Theorem GFmult_associative: forall x y z : GF, x{*}(y{*}z) = x{*}y{*}z.
+    intros x y z. apply gf_eq. unfold GFzero, GFmult, GFToZ; simpl.
+    destruct x. destruct e.
+    destruct y. destruct e0.
+    destruct z. destruct e1.
+    simpl. rewrite Zmult_mod_idemp_l, Zmult_mod_idemp_r, Zmult_assoc. trivial.
+  Qed.
+
+  Theorem GFdistributive: forall x y z : GF, (x{+}y){*}z = x{*}z{+}y{*}z.
+    intros x y z. apply gf_eq. unfold GFzero, GFmult, GFplus, GFToZ; simpl.
+    destruct x. destruct e.
+    destruct y. destruct e0.
+    destruct z. destruct e1.
+    simpl.
+    rewrite Zmult_mod_idemp_l.
+    rewrite <- Zplus_mod.
+    rewrite Z.mul_add_distr_r.
+    trivial.
+  Qed.
+
+  Theorem GFminus_opp: forall x y : GF, x{-}y = x{+}GFopp y.
+    intros x y. apply gf_eq. unfold GFzero, GFmult, GFToZ; simpl.
+    destruct x. destruct e.
+    destruct y. destruct e0.
+    simpl.
+    rewrite Zplus_mod_idemp_r.
+    trivial.
+  Qed.
+
+  Theorem GFopp_inverse: forall x : GF, x{+}GFopp x = {0}.
+    intro x. apply gf_eq. unfold GFzero, GFplus, GFToZ; simpl.
+    destruct x. destruct e. simpl. rewrite e.
+    rewrite <- Zplus_mod.
+    rewrite Z.add_opp_r.
+    rewrite Zminus_mod_idemp_r.
+    rewrite Z.sub_diag.
+    trivial.
+  Qed.
+
+  (* Ring Theory*)
+
+  Instance GFplus_compat : Proper (eq==>eq==>eq) GFplus.
+    intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; intuition; simpl in *.
+    assert (p1 + r1 = q1 + s1).
+      apply exist_eq in H; apply exist_eq in H0. rewrite H, H0. trivial.
+    unfold GFplus; simpl; rewrite H1; trivial.
+  Qed.
+
+  Instance GFminus_compat : Proper (eq==>eq==>eq) GFminus.
+    intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; intuition; simpl in *.
+    assert (p1 - r1 = q1 - s1).
+      apply exist_eq in H; apply exist_eq in H0. rewrite H, H0. trivial.
+    unfold GFminus; simpl; rewrite H1; trivial.
+  Qed.
+
+  Instance GFmult_compat : Proper (eq==>eq==>eq) GFmult.
+    intros (p1, p2) (q1, q2) H (r1, r2) (s1, s2) H0; intuition; simpl in *.
+    assert (p1 * r1 = q1 * s1).
+      apply exist_eq in H; apply exist_eq in H0. rewrite H, H0. trivial.
+    unfold GFmult; simpl; rewrite H1; trivial.
+  Qed.
+
+  Instance GFopp_compat : Proper (eq==>eq) GFopp.
+    intros x y H; intuition; simpl in *.
+    unfold GFopp, GFzero, GFminus; simpl. apply exist_eq.
+    destruct x. destruct e. rewrite e in *.
+    destruct y. destruct e0. rewrite e0 in *.
+    simpl in *. apply exist_eq in H.
+
+    assert (HX := (Z.eq_dec (x0 mod modulus) 0)); destruct HX.
+    rewrite e1; rewrite H in e1; rewrite e1; simpl; intuition.
+    repeat rewrite Z_mod_nz_opp_full;
+      try repeat rewrite Zmod_mod;
+      simpl; intuition.
+  Qed.
+
+  Definition GFring_theory : ring_theory GFzero GFone GFplus GFmult GFminus GFopp eq.
+    constructor.
+    exact GFplus_0_l.
+    exact GFplus_commutative.
+    exact GFplus_associative.
+    exact GFmult_1_l.
+    exact GFmult_commutative.
+    exact GFmult_associative.
+    exact GFdistributive.
+    exact GFminus_opp.
+    exact GFopp_inverse.
+  Defined.
+
+  Add Ring GFring : GFring_theory.
+
+  (* Power theory *)
+
+
+  Lemma GFpower_theory : power_theory GFone GFmult eq id GFexp.
+    constructor. intros.
+    induction n; simpl; intuition.
+
+    (* Prove the doubling case, which we'll use alot *)
+    assert (forall q r0, GFexp' r0 q{*}GFexp' r0 q = GFexp' (r0{*}r0) q).
+      induction q.
+      intros. assert (Q := (IHq (r0{*}r0))).
+        unfold GFexp'; simpl; fold GFexp'.
+        rewrite <- Q. ring.
+      intros. assert (Q := (IHq (r0{*}r0))).
+        unfold GFexp'; simpl; fold GFexp'.
+        rewrite <- Q. ring.
+      intros; simpl; ring.
+
+    (* Take it case-by-case *)
+    unfold GFexp; induction p.
+
+    (* Odd case *)
+    unfold GFexp'; simpl; fold GFexp'; fold pow_pos.
+    rewrite <- (H p r).
+    rewrite <- IHp. trivial.
+
+    (* Even case *)
+    unfold GFexp'; simpl; fold GFexp'; fold pow_pos.
+    rewrite <- (H p r).
+    rewrite <- IHp. trivial.
+
+    (* Base case *)
+    simpl; intuition.
+  Qed.
+
+  (* Field Theory*)
+
+  Instance GFinv_compat : Proper (eq==>eq) GFinv.
+    unfold GFinv; simpl; intuition.
+  Qed.
+
+  Instance GFdiv_compat : Proper (eq==>eq==>eq) GFdiv.
+    unfold GFdiv; simpl; intuition.
+  Qed.
+
+  Definition GFfield_theory : field_theory GFzero GFone GFplus GFmult GFminus GFopp GFdiv GFinv eq.
+    constructor; simpl; intuition.
+    exact GFring_theory.
+    unfold GFone, GFzero in H; apply exist_eq in H; simpl in H; intuition.
+
+    (* Prove multiplicative inverses *)
+    unfold GFinv.
+    destruct totient; simpl. destruct i.
+    replace (p{^}(N.pred x){*}p) with (p{^}x); simpl; intuition.
+    apply N.gt_lt in H0; apply N.lt_neq in H0.
+    replace x with (N.succ (N.pred x)).
+      induction (N.pred x).
+      simpl. ring.
+      rewrite N.pred_succ.
+
+    (* Just the N.succ case *)
+    generalize p. induction p0; simpl in *; intuition.
+      rewrite (IHp0 (p1{*}p1)). ring.
+      ring.
+
+    (* cleanup *)
+    rewrite N.succ_pred; intuition.
+  Defined.
+
+  Add Field GFfield : GFfield_theory.
+
+End GaloisFieldTheory.
+