From 0d063eafadf1237db4b99debf896f61bca4aeef0 Mon Sep 17 00:00:00 2001 From: Robert Sloan Date: Wed, 16 Sep 2015 22:26:59 -0400 Subject: redo module structure + init curve25519 --- Makefile | 10 +- _CoqProject | 3 + src/Curves/Curve25519.v | 32 ++++-- src/Galois/GaloisField.v | 97 +++++++++++++++++ src/Galois/GaloisFieldTheory.v | 233 +++++++++++++++++++++++++++++++++++++++++ src/GaloisField.v | 94 ----------------- src/GaloisFieldTheory.v | 232 ---------------------------------------- 7 files changed, 359 insertions(+), 342 deletions(-) create mode 100644 src/Galois/GaloisField.v create mode 100644 src/Galois/GaloisFieldTheory.v delete mode 100644 src/GaloisField.v delete mode 100644 src/GaloisFieldTheory.v diff --git a/Makefile b/Makefile index 42fb6aa7c..7a7714ebc 100644 --- a/Makefile +++ b/Makefile @@ -10,13 +10,13 @@ include .make/coq.mk FAST_TARGETS += check_fiat clean .DEFAULT_GOAL = all -.PHONY: all clean coquille +.PHONY: all deps objects clean coquille -all: $(SOURCES) - @echo "done!" +all: objects -coquille: - vim -c "execute coquille#Launch($(COQLIBS))" . +deps: $(SOURCES:%=%.d) + +objects: deps $(SOURCES:%=%o) clean: $(RM) $(foreach f,$(SOURCES),$(call coq-generated,$(basename $f))) diff --git a/_CoqProject b/_CoqProject index 89404292d..fac637589 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,3 +1,6 @@ -R src Crypto -R fiat/src Fiat +src/Galois/GaloisField.v +src/Galois/GaloisFieldTheory.v src/Curves/Curve25519.v +src/Assembly/Assembly.v diff --git a/src/Curves/Curve25519.v b/src/Curves/Curve25519.v index 8bc3d6e20..df0b2ce06 100644 --- a/src/Curves/Curve25519.v +++ b/src/Curves/Curve25519.v @@ -1,13 +1,23 @@ -Require Import ZModulo. -(** - * The relevant module is ZModulo: - * the constructor you want is of_pos - * the operations you want are in zmod_ops - * the tactics you want are somewhere between Field and CyclicType: - * probs you want to be converting to/from Z pretty frequently - * - * Coq Reference page: - * https://coq.inria.fr/library/Coq.Numbers.Cyclic.ZModulo.ZModulo.html - *) +Require Import Zpower ZArith Znumtheory. +Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory. + +Definition prime25519 : Prime. + exists ((two_p 255) - 19). + (* *) +Admitted. + +Module Modulus25519 <: Modulus. + Definition modulus := prime25519. +End Modulus25519. + +Declare Module GaloisField25519 : GaloisField Modulus25519. + +Declare Module GaloisTheory25519 : GaloisFieldTheory Modulus25519 GaloisField25519. + +Module Curve25519. + Import Modulus25519 GaloisField25519 GaloisTheory25519. + + (* Prove some theorems! *) +End Curve25519. diff --git a/src/Galois/GaloisField.v b/src/Galois/GaloisField.v new file mode 100644 index 000000000..dfae63312 --- /dev/null +++ b/src/Galois/GaloisField.v @@ -0,0 +1,97 @@ + +Require Import BinInt BinNat ZArith Znumtheory. +Require Import ProofIrrelevance Epsilon. + +Section GaloisPreliminaries. + Definition Prime := {x: Z | prime x}. + + Definition primeToZ(x: Prime) := proj1_sig x. + Coercion primeToZ: Prime >-> Z. + + 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. +End GaloisPreliminaries. + +Module Type Modulus. + Parameter modulus: Prime. +End Modulus. + +Module Type GaloisField (M: Modulus). + Import M. + + Definition GF := {x: Z | exists y, x = y mod modulus}. + Definition GFToZ(x: GF) := proj1_sig x. + Coercion GFToZ: GF >-> Z. + + Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y. + intros x y. destruct x, y. split; apply exist_eq. + Qed. + + (* 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/Galois/GaloisFieldTheory.v b/src/Galois/GaloisFieldTheory.v new file mode 100644 index 000000000..1a478e088 --- /dev/null +++ b/src/Galois/GaloisFieldTheory.v @@ -0,0 +1,233 @@ + +Require Import BinInt BinNat ZArith Znumtheory. +Require Export Coq.Classes.Morphisms Setoid. +Require Export Ring_theory Field_theory Field_tac. +Require Export Crypto.Galois.GaloisField. + +Set Implicit Arguments. +Unset Strict Implicits. + +Module Type GaloisFieldTheory (M: Modulus) (Field: GaloisField M). + Import M. + 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. + diff --git a/src/GaloisField.v b/src/GaloisField.v deleted file mode 100644 index 928eaf702..000000000 --- a/src/GaloisField.v +++ /dev/null @@ -1,94 +0,0 @@ - -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 deleted file mode 100644 index 1a749b027..000000000 --- a/src/GaloisFieldTheory.v +++ /dev/null @@ -1,232 +0,0 @@ - -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