From 1e67fe3272ac40e1d5b0908940f740b523db0c21 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Wed, 16 Sep 2015 16:35:03 -0400 Subject: Basic Galois Field Theory Modules --- Makefile | 4 +- src/GaloisField.v | 94 ++++++++++++++++++++ src/GaloisFieldTheory.v | 232 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 328 insertions(+), 2 deletions(-) create mode 100644 src/GaloisField.v create mode 100644 src/GaloisFieldTheory.v 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. + -- cgit v1.2.3