diff options
| -rw-r--r-- | .travis.yml | 8 | ||||
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | README.md | 7 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Cyclic.v (renamed from coqprime-8.5/Coqprime/Cyclic.v) | 14 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/EGroup.v (renamed from coqprime-8.5/Coqprime/EGroup.v) | 36 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Euler.v (renamed from coqprime-8.5/Coqprime/Euler.v) | 8 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/FGroup.v (renamed from coqprime-8.5/Coqprime/FGroup.v) | 8 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/IGroup.v (renamed from coqprime-8.5/Coqprime/IGroup.v) | 12 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Iterator.v (renamed from coqprime-8.5/Coqprime/Iterator.v) | 6 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Lagrange.v (renamed from coqprime-8.5/Coqprime/Lagrange.v) | 12 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/ListAux.v (renamed from coqprime-8.5/Coqprime/ListAux.v) | 10 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/LucasLehmer.v (renamed from coqprime-8.5/Coqprime/LucasLehmer.v) | 36 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Makefile.bak (renamed from coqprime/Coqprime/Makefile.bak) | 0 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/NatAux.v (renamed from coqprime-8.5/Coqprime/NatAux.v) | 2 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Note.pdf (renamed from coqprime/Coqprime/Note.pdf) | bin | 134038 -> 134038 bytes | |||
| -rw-r--r-- | coqprime-8.4/Coqprime/PGroup.v (renamed from coqprime-8.5/Coqprime/PGroup.v) | 18 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Permutation.v (renamed from coqprime-8.5/Coqprime/Permutation.v) | 4 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Pmod.v (renamed from coqprime-8.5/Coqprime/Pmod.v) | 10 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Pocklington.v (renamed from coqprime-8.5/Coqprime/Pocklington.v) | 16 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/PocklingtonCertificat.v (renamed from coqprime-8.5/Coqprime/PocklingtonCertificat.v) | 219 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Root.v (renamed from coqprime-8.5/Coqprime/Root.v) | 14 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Tactic.v (renamed from coqprime-8.5/Coqprime/Tactic.v) | 0 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/UList.v (renamed from coqprime-8.5/Coqprime/UList.v) | 70 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/ZCAux.v (renamed from coqprime-8.5/Coqprime/ZCAux.v) | 8 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/ZCmisc.v (renamed from coqprime-8.5/Coqprime/ZCmisc.v) | 2 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/ZProgression.v (renamed from coqprime-8.5/Coqprime/ZProgression.v) | 6 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/ZSum.v (renamed from coqprime-8.5/Coqprime/ZSum.v) | 12 | ||||
| -rw-r--r-- | coqprime-8.4/Coqprime/Zp.v (renamed from coqprime-8.5/Coqprime/Zp.v) | 20 | ||||
| -rw-r--r-- | coqprime-8.4/Makefile (renamed from coqprime-8.5/Makefile) | 160 | ||||
| -rw-r--r-- | coqprime-8.4/README.md | 9 | ||||
| -rw-r--r-- | coqprime-8.4/_CoqProject (renamed from coqprime-8.5/_CoqProject) | 0 | ||||
| -rw-r--r-- | coqprime-8.5/README.md | 9 | ||||
| -rw-r--r-- | coqprime/Coqprime/Cyclic.v | 14 | ||||
| -rw-r--r-- | coqprime/Coqprime/EGroup.v | 36 | ||||
| -rw-r--r-- | coqprime/Coqprime/Euler.v | 8 | ||||
| -rw-r--r-- | coqprime/Coqprime/FGroup.v | 8 | ||||
| -rw-r--r-- | coqprime/Coqprime/IGroup.v | 12 | ||||
| -rw-r--r-- | coqprime/Coqprime/Iterator.v | 6 | ||||
| -rw-r--r-- | coqprime/Coqprime/Lagrange.v | 12 | ||||
| -rw-r--r-- | coqprime/Coqprime/ListAux.v | 10 | ||||
| -rw-r--r-- | coqprime/Coqprime/LucasLehmer.v | 36 | ||||
| -rw-r--r-- | coqprime/Coqprime/NatAux.v | 2 | ||||
| -rw-r--r-- | coqprime/Coqprime/PGroup.v | 18 | ||||
| -rw-r--r-- | coqprime/Coqprime/Permutation.v | 4 | ||||
| -rw-r--r-- | coqprime/Coqprime/Pmod.v | 10 | ||||
| -rw-r--r-- | coqprime/Coqprime/Pocklington.v | 16 | ||||
| -rw-r--r-- | coqprime/Coqprime/PocklingtonCertificat.v | 219 | ||||
| -rw-r--r-- | coqprime/Coqprime/Root.v | 14 | ||||
| -rw-r--r-- | coqprime/Coqprime/UList.v | 70 | ||||
| -rw-r--r-- | coqprime/Coqprime/ZCAux.v | 8 | ||||
| -rw-r--r-- | coqprime/Coqprime/ZCmisc.v | 2 | ||||
| -rw-r--r-- | coqprime/Coqprime/ZProgression.v | 6 | ||||
| -rw-r--r-- | coqprime/Coqprime/ZSum.v | 12 | ||||
| -rw-r--r-- | coqprime/Coqprime/Zp.v | 20 | ||||
| -rw-r--r-- | coqprime/Makefile | 160 | ||||
| -rw-r--r-- | coqprime/README.md | 2 |
56 files changed, 723 insertions, 722 deletions
diff --git a/.travis.yml b/.travis.yml index b4d747d6a..1092e385a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -5,12 +5,8 @@ dist: trusty env: matrix: - - COQ_VERSION="8.4" COQPRIME="coqprime" - - COQ_VERSION="8.5" COQPRIME="coqprime-8.5" - -matrix: - allow_failures: - - env: COQ_VERSION="8.5" COQPRIME="coqprime-8.5" + - COQ_VERSION="8.4" COQPRIME="coqprime-8.4" + - COQ_VERSION="8.5" COQPRIME="coqprime" before_install: - if [ "$COQ_VERSION" == "8.5" ]; then sudo add-apt-repository ppa:jgross-h/coq-backports -y; fi @@ -32,10 +32,10 @@ coqprime: coqprime-8.4 endif coqprime-8.4: - $(MAKE) -C coqprime + $(MAKE) -C coqprime-8.4 coqprime-8.5: - $(MAKE) -C coqprime-8.5 + $(MAKE) -C coqprime Makefile.coq: Makefile _CoqProject $(Q)$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq @@ -6,7 +6,12 @@ Fiat-Crypto: Synthesizing Correct-by-Construction Assembly for Cryptographic Pri NOTE: The github.com repo is only intermittently synced with github.mit.edu. -To build: +To build (Coq 8.5): export COQPATH="$(pwd)/coqprime${COQPATH:+:}$COQPATH" make + +To build with Coq 8.4 + + export COQPATH="$(pwd)/coqprime-8.4${COQPATH:+:}$COQPATH" + make diff --git a/coqprime-8.5/Coqprime/Cyclic.v b/coqprime-8.4/Coqprime/Cyclic.v index c25f683ca..e2daa4d67 100644 --- a/coqprime-8.5/Coqprime/Cyclic.v +++ b/coqprime-8.4/Coqprime/Cyclic.v @@ -11,13 +11,13 @@ Proof that an abelien ring is cyclic ************************************************************************) -Require Import ZCAux. -Require Import List. -Require Import Root. -Require Import UList. -Require Import IGroup. -Require Import EGroup. -Require Import FGroup. +Require Import Coqprime.ZCAux. +Require Import Coq.Lists.List. +Require Import Coqprime.Root. +Require Import Coqprime.UList. +Require Import Coqprime.IGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/EGroup.v b/coqprime-8.4/Coqprime/EGroup.v index 933176abd..553cb746c 100644 --- a/coqprime-8.5/Coqprime/EGroup.v +++ b/coqprime-8.4/Coqprime/EGroup.v @@ -11,15 +11,15 @@ Given an element a, create the group {e, a, a^2, ..., a^n} **********************************************************************) -Require Import ZArith. -Require Import Tactic. -Require Import List. -Require Import ZCAux. -Require Import ZArith Znumtheory. -Require Import Wf_nat. -Require Import UList. -Require Import FGroup. -Require Import Lagrange. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Tactic. +Require Import Coq.Lists.List. +Require Import Coqprime.ZCAux. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.Lagrange. Open Scope Z_scope. @@ -43,7 +43,7 @@ Hypothesis a_in_G: In a G.(s). **************************************) Set Implicit Arguments. -Definition gpow n := match n with Zpos p => iter_pos _ (op a) G.(e) p | _ => G.(e) end. +Definition gpow n := match n with Zpos p => iter_pos p _ (op a) G.(e) | _ => G.(e) end. Unset Implicit Arguments. Theorem gpow_0: gpow 0 = G.(e). @@ -63,17 +63,17 @@ intros n; case n; simpl; auto. intros p; apply iter_pos_invariant with (Inv := fun x => In x G.(s)); auto. Qed. -Theorem gpow_op: forall b p, In b G.(s) -> iter_pos _ (op a) b p = op (iter_pos _ (op a) G.(e) p) b. +Theorem gpow_op: forall b p, In b G.(s) -> iter_pos p _ (op a) b = op (iter_pos p _ (op a) G.(e)) b. intros b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b Hb. assert (H: In (gpow (Zpos p)) G.(s)). apply gpow_in. -rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos A x y p)); auto. +rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos p A x y)); auto. repeat rewrite G.(assoc); auto. intros p Rec b Hb. assert (H: In (gpow (Zpos p)) G.(s)). apply gpow_in. -rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos A x y p)); auto. +rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos p A x y)); auto. repeat rewrite G.(assoc); auto. intros b H; rewrite e_is_zero_r; auto. Qed. @@ -87,7 +87,7 @@ intros _ _; simpl; apply sym_equal; apply e_is_zero_r. exact (gpow_in (Zpos p1)). 2: intros p2 _ H; contradict H; auto with zarith. intros p2 _ _; simpl. -rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos A x y p2)); auto. +rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos p2 A x y)); auto. exact (gpow_in (Zpos p2)). Qed. @@ -445,7 +445,7 @@ intros x H2 Rec _; unfold Zsucc; rewrite gpow_add; simpl; auto with zarith. repeat rewrite G.(e_is_zero_r); auto with zarith. apply gpow_in; sauto. intros p1 _; case m; simpl; auto. -assert(H1: In (iter_pos A (op a) (e G) p1) (s G)). +assert(H1: In (iter_pos p1 A (op a) (e G)) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p1)); auto. intros p2 _; pattern p2; apply Pind; simpl; auto. rewrite Pmult_1_r; rewrite G.(e_is_zero_r); try rewrite G.(e_is_zero_r); auto. @@ -486,12 +486,12 @@ repeat rewrite iter_pos_plus; simpl. repeat rewrite (fun x y H z => gpow_op A op x G H (op y z)) ; auto. rewrite Rec. repeat rewrite G.(e_is_zero_r); auto. -assert(H1: In (iter_pos A (op a) (e G) p3) (s G)). +assert(H1: In (iter_pos p3 A (op a) (e G)) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p3)); auto. -assert(H2: In (iter_pos A (op b) (e G) p3) (s G)). +assert(H2: In (iter_pos p3 A (op b) (e G)) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p3)); auto. repeat rewrite <- G.(assoc); try eq_tac; auto. -rewrite (fun x y => comm (iter_pos A x y p3) b); auto. +rewrite (fun x y => comm (iter_pos p3 A x y) b); auto. rewrite (G.(assoc) a); try apply comm; auto. Qed. diff --git a/coqprime-8.5/Coqprime/Euler.v b/coqprime-8.4/Coqprime/Euler.v index 06d92ce57..e571d8e3c 100644 --- a/coqprime-8.5/Coqprime/Euler.v +++ b/coqprime-8.4/Coqprime/Euler.v @@ -11,10 +11,10 @@ Definition of the Euler Totient function *************************************************************************) -Require Import ZArith. -Require Export Znumtheory. -Require Import Tactic. -Require Export ZSum. +Require Import Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Export Coqprime.ZSum. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/FGroup.v b/coqprime-8.4/Coqprime/FGroup.v index a55710e7c..0bcc9ebf1 100644 --- a/coqprime-8.5/Coqprime/FGroup.v +++ b/coqprime-8.4/Coqprime/FGroup.v @@ -13,10 +13,10 @@ Definition: FGroup **********************************************************************) -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import ZArith. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coq.ZArith.ZArith. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/IGroup.v b/coqprime-8.4/Coqprime/IGroup.v index 11a73d414..04219be5a 100644 --- a/coqprime-8.5/Coqprime/IGroup.v +++ b/coqprime-8.4/Coqprime/IGroup.v @@ -13,12 +13,12 @@ Definition: ZpGroup **********************************************************************) -Require Import ZArith. -Require Import Tactic. -Require Import Wf_nat. -Require Import UList. -Require Import ListAux. -Require Import FGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/Iterator.v b/coqprime-8.4/Coqprime/Iterator.v index 96d3e5655..e84687cd4 100644 --- a/coqprime-8.5/Coqprime/Iterator.v +++ b/coqprime-8.4/Coqprime/Iterator.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export List. -Require Export Permutation. -Require Import Arith. +Require Export Coq.Lists.List. +Require Export Coqprime.Permutation. +Require Import Coq.Arith.Arith. Section Iterator. Variables A B : Set. diff --git a/coqprime-8.5/Coqprime/Lagrange.v b/coqprime-8.4/Coqprime/Lagrange.v index b35460bad..b890c5621 100644 --- a/coqprime-8.5/Coqprime/Lagrange.v +++ b/coqprime-8.4/Coqprime/Lagrange.v @@ -14,12 +14,12 @@ Definition: lagrange **********************************************************************) -Require Import List. -Require Import UList. -Require Import ListAux. -Require Import ZArith Znumtheory. -Require Import NatAux. -Require Import FGroup. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coqprime.NatAux. +Require Import Coqprime.FGroup. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/ListAux.v b/coqprime-8.4/Coqprime/ListAux.v index c3c9602bd..4ed154685 100644 --- a/coqprime-8.5/Coqprime/ListAux.v +++ b/coqprime-8.4/Coqprime/ListAux.v @@ -11,11 +11,11 @@ Auxillary functions & Theorems **********************************************************************) -Require Export List. -Require Export Arith. -Require Export Tactic. -Require Import Inverse_Image. -Require Import Wf_nat. +Require Export Coq.Lists.List. +Require Export Coq.Arith.Arith. +Require Export Coqprime.Tactic. +Require Import Coq.Wellfounded.Inverse_Image. +Require Import Coq.Arith.Wf_nat. (************************************** Some properties on list operators: app, map,... diff --git a/coqprime-8.5/Coqprime/LucasLehmer.v b/coqprime-8.4/Coqprime/LucasLehmer.v index a0e3b8e46..c459195a8 100644 --- a/coqprime-8.5/Coqprime/LucasLehmer.v +++ b/coqprime-8.4/Coqprime/LucasLehmer.v @@ -13,17 +13,17 @@ Definition: LucasLehmer **********************************************************************) -Require Import ZArith. -Require Import ZCAux. -Require Import Tactic. -Require Import Wf_nat. -Require Import NatAux. -Require Import UList. -Require Import ListAux. -Require Import FGroup. -Require Import EGroup. -Require Import PGroup. -Require Import IGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.ZCAux. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.NatAux. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.PGroup. +Require Import Coqprime.IGroup. Open Scope Z_scope. @@ -47,7 +47,7 @@ Qed. Definition of the power function for pairs p^n **************************************) -Definition ppow p n := match n with Zpos q => iter_pos _ (pmult p) (1, 0) q | _ => (1, 0) end. +Definition ppow p n := match n with Zpos q => iter_pos q _ (pmult p) (1, 0) | _ => (1, 0) end. (************************************** Some properties of ppow @@ -63,14 +63,14 @@ intros p; apply iter_pos_invariant with (Inv := fun x => x = (1, 0)); auto. intros x H; rewrite H; auto. Qed. -Theorem ppow_op: forall a b p, iter_pos _ (pmult a) b p = pmult (iter_pos _ (pmult a) (1, 0) p) b. +Theorem ppow_op: forall a b p, iter_pos p _ (pmult a) b = pmult (iter_pos p _ (pmult a) (1, 0)) b. intros a b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b. rewrite (Rec b). -try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. +try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos p _ x y)); auto. repeat rewrite pmult_assoc; auto. intros p Rec b. -rewrite (Rec b); try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. +rewrite (Rec b); try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos p _ x y)); auto. repeat rewrite pmult_assoc; auto. intros b; rewrite pmult_1_r; auto. Qed. @@ -114,7 +114,7 @@ repeat rewrite (fun x y z => ppow_op x (pmult y z)) ; auto. rewrite Rec. repeat rewrite pmult_1_r; auto. repeat rewrite <- pmult_assoc; try eq_tac; auto. -rewrite (fun x y => pmult_comm (iter_pos _ x y p3) p); auto. +rewrite (fun x y => pmult_comm (iter_pos p3 _ x y) p); auto. rewrite (pmult_assoc m); try apply pmult_comm; auto. Qed. @@ -490,13 +490,13 @@ End Lucas. Definition SS p := let n := Mp p in match p - 2 with - Zpos p1 => iter_pos _ (fun x => Zmodd (Zsquare x - 2) n) (Zmodd 4 n) p1 + Zpos p1 => iter_pos p1 _ (fun x => Zmodd (Zsquare x - 2) n) (Zmodd 4 n) | _ => (Zmodd 4 n) end. Theorem SS_aux_correct: forall p z1 z2 n, 0 <= n -> 0 < z1 -> z2 = fst (s n) mod z1 -> - iter_pos _ (fun x => Zmodd (Zsquare x - 2) z1) z2 p = fst (s (n + Zpos p)) mod z1. + iter_pos p _ (fun x => Zmodd (Zsquare x - 2) z1) z2 = fst (s (n + Zpos p)) mod z1. intros p; pattern p; apply Pind. simpl. intros z1 z2 n Hn H H1; rewrite sn; auto; rewrite H1; rewrite Zmodd_correct; rewrite Zsquare_correct; simpl. diff --git a/coqprime/Coqprime/Makefile.bak b/coqprime-8.4/Coqprime/Makefile.bak index fe49dbf29..fe49dbf29 100644 --- a/coqprime/Coqprime/Makefile.bak +++ b/coqprime-8.4/Coqprime/Makefile.bak diff --git a/coqprime-8.5/Coqprime/NatAux.v b/coqprime-8.4/Coqprime/NatAux.v index eab09150c..6df511eed 100644 --- a/coqprime-8.5/Coqprime/NatAux.v +++ b/coqprime-8.4/Coqprime/NatAux.v @@ -11,7 +11,7 @@ Auxillary functions & Theorems **********************************************************************) -Require Export Arith. +Require Export Coq.Arith.Arith. (************************************** Some properties of minus diff --git a/coqprime/Coqprime/Note.pdf b/coqprime-8.4/Coqprime/Note.pdf Binary files differindex 239a38772..239a38772 100644 --- a/coqprime/Coqprime/Note.pdf +++ b/coqprime-8.4/Coqprime/Note.pdf diff --git a/coqprime-8.5/Coqprime/PGroup.v b/coqprime-8.4/Coqprime/PGroup.v index e9c1b2f47..19eff5850 100644 --- a/coqprime-8.5/Coqprime/PGroup.v +++ b/coqprime-8.4/Coqprime/PGroup.v @@ -14,15 +14,15 @@ Definition: PGroup **********************************************************************) -Require Import ZArith. -Require Import Znumtheory. -Require Import Tactic. -Require Import Wf_nat. -Require Import ListAux. -Require Import UList. -Require Import FGroup. -Require Import EGroup. -Require Import IGroup. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.ListAux. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/Permutation.v b/coqprime-8.4/Coqprime/Permutation.v index a06693f89..7cb6f629d 100644 --- a/coqprime-8.5/Coqprime/Permutation.v +++ b/coqprime-8.4/Coqprime/Permutation.v @@ -11,8 +11,8 @@ Defintion and properties of permutations **********************************************************************) -Require Export List. -Require Export ListAux. +Require Export Coq.Lists.List. +Require Export Coqprime.ListAux. Section permutation. Variable A : Set. diff --git a/coqprime-8.5/Coqprime/Pmod.v b/coqprime-8.4/Coqprime/Pmod.v index f64af48e3..45961896e 100644 --- a/coqprime-8.5/Coqprime/Pmod.v +++ b/coqprime-8.4/Coqprime/Pmod.v @@ -6,8 +6,8 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export ZArith. -Require Export ZCmisc. +Require Export Coq.ZArith.ZArith. +Require Export Coqprime.ZCmisc. Open Local Scope positive_scope. @@ -392,7 +392,7 @@ Lemma gcd_log2_mod0 : Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed. -Require Import Zwf. +Require Import Coq.ZArith.Zwf. Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y). Proof. @@ -510,8 +510,8 @@ Proof. destruct (gcd_log2 b r r);intros;trivial. Qed. -Require Import ZArith. -Require Import Znumtheory. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. Hint Rewrite Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc. diff --git a/coqprime-8.5/Coqprime/Pocklington.v b/coqprime-8.4/Coqprime/Pocklington.v index 9871cd3e6..79e7dc616 100644 --- a/coqprime-8.5/Coqprime/Pocklington.v +++ b/coqprime-8.4/Coqprime/Pocklington.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import ZArith. -Require Export Znumtheory. -Require Import Tactic. -Require Import ZCAux. -Require Import Zp. -Require Import FGroup. -Require Import EGroup. -Require Import Euler. +Require Import Coq.ZArith.ZArith. +Require Export Coq.ZArith.Znumtheory. +Require Import Coqprime.Tactic. +Require Import Coqprime.ZCAux. +Require Import Coqprime.Zp. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.Euler. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/PocklingtonCertificat.v b/coqprime-8.4/Coqprime/PocklingtonCertificat.v index ecf4462ed..fccea30b6 100644 --- a/coqprime-8.5/Coqprime/PocklingtonCertificat.v +++ b/coqprime-8.4/Coqprime/PocklingtonCertificat.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import List. -Require Import ZArith. -Require Import Zorder. -Require Import ZCAux. -Require Import LucasLehmer. -Require Import Pocklington. -Require Import ZCmisc. -Require Import Pmod. +Require Import Coq.Lists.List. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Zorder. +Require Import Coqprime.ZCAux. +Require Import Coqprime.LucasLehmer. +Require Import Coqprime.Pocklington. +Require Import Coqprime.ZCmisc. +Require Import Coqprime.Pmod. Definition dec_prime := list (positive * positive). @@ -61,18 +61,18 @@ Definition mkProd (l:dec_prime) := (* [pow_mod a m n] return [a^m mod n] *) Fixpoint pow_mod (a m n : positive) {struct m} : N := match m with - | xH => (a mod n)%P + | xH => (a mod n) | xO m' => let z := pow_mod a m' n in match z with | N0 => 0%N - | Npos z' => ((square z') mod n)%P + | Npos z' => ((square z') mod n) end | xI m' => let z := pow_mod a m' n in match z with | N0 => 0%N - | Npos z' => (((square z') * a)%P mod n)%P + | Npos z' => ((square z') * a)%P mod n end end. @@ -118,7 +118,7 @@ Fixpoint pow_mod_pred (a:N) (l:dec_prime) (n:positive) {struct l} : N := | (q,p)::l => if (p ?= 1) then pow_mod_pred a l n else - let a' := iter_pos _ (fun x => Npow_mod x q n) a (Ppred p) in + let a' := iter_pos (Ppred p) _ (fun x => Npow_mod x q n) a in pow_mod_pred a' l n end. @@ -332,113 +332,120 @@ Hint Rewrite Pmod_Zmod : zmisc. Lemma Zpower_0 : forall p : positive, 0^p = 0. Proof. intros;simpl;destruct p;unfold Zpower_pos;simpl;trivial. - generalize (iter_pos Z (Z.mul 0) 1 p). + generalize (iter_pos p Z (Z.mul 0) 1). induction p;simpl;trivial. Qed. +Opaque Zpower. +Opaque Zmult. + Lemma pow_Zpower : forall a p, Zpos (pow a p) = a ^ p. -Proof. - induction p; mauto; simpl; mauto; rewrite IHp; mauto. +Proof with mauto. + induction p;simpl... rewrite IHp... rewrite IHp... Qed. Hint Rewrite pow_Zpower : zmisc. Lemma pow_mod_spec : forall n a m, Z_of_N (pow_mod a m n) = a^m mod n. -Proof. - induction m; mauto; simpl; intros; mauto. +Proof with mauto. + induction m;simpl;intros... rewrite Zmult_mod; auto with zmisc. - rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. - rewrite <- IHm; mauto. - destruct (pow_mod a m n); mauto. - rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. - rewrite <- IHm. destruct (pow_mod a m n);simpl; mauto. + rewrite (Zmult_mod (a^m)); auto with zmisc. rewrite <- IHm. + destruct (pow_mod a m n);simpl... + rewrite Zmult_mod; auto with zmisc. + rewrite <- IHm. destruct (pow_mod a m n);simpl... Qed. Hint Rewrite pow_mod_spec Zpower_0 : zmisc. Lemma Npow_mod_spec : forall a p n, Z_of_N (Npow_mod a p n) = a^p mod n. -Proof. - intros a p n;destruct a; mauto; simpl; mauto. +Proof with mauto. + intros a p n;destruct a;simpl ... Qed. Hint Rewrite Npow_mod_spec : zmisc. Lemma iter_Npow_mod_spec : forall n q p a, - Z_of_N (iter_pos N (fun x : N => Npow_mod x q n) a p) = a^q^p mod n. -Proof. - induction p; mauto; intros; simpl Pos.iter; mauto; repeat rewrite IHp. + Z_of_N (iter_pos p N (fun x : N => Npow_mod x q n) a) = a^q^p mod n. +Proof with mauto. + induction p;simpl;intros ... + repeat rewrite IHp. rewrite (Zpower_mod ((a ^ q ^ p) ^ q ^ p));auto with zmisc. - rewrite (Zpower_mod (a ^ q ^ p)); mauto. - mauto. + rewrite (Zpower_mod (a ^ q ^ p))... + repeat rewrite IHp... Qed. -Hint Rewrite iter_Npow_mod_spec : zmisc. +Hint Rewrite iter_Npow_mod_spec : zmisc. + Lemma fold_pow_mod_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n. -Proof. - unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd'; - intros; mauto. - rewrite IHl; mauto. +Proof with mauto. + unfold fold_pow_mod;induction l;simpl;intros ... + rewrite IHl... Qed. Hint Rewrite fold_pow_mod_spec : zmisc. Lemma pow_mod_pred_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n. -Proof. - unfold pow_mod_pred;induction l;simpl mkProd;intros; mauto. - destruct a as (q,p). - simpl mkProd_pred. - destruct (p ?= 1)%P; rewrite IHl; mauto; simpl. +Proof with mauto. + unfold pow_mod_pred;induction l;simpl;intros ... + destruct a as (q,p);simpl. + destruct (p ?= 1)%P; rewrite IHl... Qed. Hint Rewrite pow_mod_pred_spec : zmisc. Lemma mkProd_pred_mkProd : forall l, (mkProd_pred l)*(mkProd' l) = mkProd l. -Proof. - induction l;simpl;intros; mauto. +Proof with mauto. + induction l;simpl;intros ... generalize (pos_eq_1_spec (snd a)); destruct (snd a ?= 1)%P;intros. - rewrite H; mauto. + rewrite H... replace (mkProd_pred l * (fst a * mkProd' l)) with (fst a *(mkProd_pred l * mkProd' l));try ring. - rewrite IHl; mauto. + rewrite IHl... rewrite Zmult_assoc. rewrite times_Zmult. rewrite (Zmult_comm (pow (fst a) (Ppred (snd a)) * mkProd_pred l)). rewrite Zmult_assoc. rewrite pow_Zpower. rewrite <-Ppred_Zminus;trivial. rewrite <- Zpower_Zsucc; try omega. replace (Zsucc (snd a - 1)) with ((snd a - 1)+1). - replace ((snd a - 1)+1) with (Zpos (snd a)); mauto. - rewrite <- IHl;repeat rewrite Zmult_assoc; mauto. + replace ((snd a - 1)+1) with (Zpos (snd a)) ... + rewrite <- IHl;repeat rewrite Zmult_assoc ... destruct (snd a - 1);trivial. assert (1 < snd a); auto with zarith. Qed. -Hint Rewrite mkProd_pred_mkProd : zmisc. +Hint Rewrite mkProd_pred_mkProd : zmisc. Lemma lt_Zmod : forall p n, 0 <= p < n -> p mod n = p. -Proof. +Proof with mauto. intros a b H. assert ( 0 <= a mod b < b). - apply Z_mod_lt; mauto. - destruct (mod_unique b (a/b) (a mod b) 0 a H0 H); mauto. - rewrite <- Z_div_mod_eq; mauto. + apply Z_mod_lt... + destruct (mod_unique b (a/b) (a mod b) 0 a H0 H)... + rewrite <- Z_div_mod_eq... Qed. +Opaque Zminus. Lemma Npred_mod_spec : forall p n, Z_of_N p < Zpos n -> 1 < Zpos n -> Z_of_N (Npred_mod p n) = (p - 1) mod n. -Proof. +Proof with mauto. destruct p;intros;simpl. - rewrite <- Ppred_Zminus; auto. - apply Zmod_unique with (q := -1); mauto. + rewrite <- Ppred_Zminus... + change (-1) with (0 -1). rewrite <- (Z_mod_same n) ... + pattern 1 at 2;rewrite <- (lt_Zmod 1 n) ... + symmetry;apply lt_Zmod. +Transparent Zminus. + omega. assert (H1 := pos_eq_1_spec p);destruct (p?=1)%P. - rewrite H1; mauto. - unfold Z_of_N;rewrite <- Ppred_Zminus; auto. - simpl in H;symmetry; apply (lt_Zmod (p-1) n). + rewrite H1 ... + unfold Z_of_N;rewrite <- Ppred_Zminus... + simpl in H;symmetry; apply (lt_Zmod (p-1) n)... assert (1 < p); auto with zarith. Qed. Hint Rewrite Npred_mod_spec : zmisc. Lemma times_mod_spec : forall x y n, Z_of_N (times_mod x y n) = (x * y) mod n. -Proof. - intros; destruct x; mauto. - destruct y;simpl; mauto. +Proof with mauto. + intros; destruct x ... + destruct y;simpl ... Qed. Hint Rewrite times_mod_spec : zmisc. @@ -446,10 +453,10 @@ Lemma snd_all_pow_mod : forall n l (prod a :N), a mod (Zpos n) = a -> Z_of_N (snd (all_pow_mod prod a l n)) = (a^(mkProd' l)) mod n. -Proof. - induction l; simpl all_pow_mod; simpl mkProd';intros; mauto. - destruct a as (q,p). - rewrite IHl; mauto. +Proof with mauto. + induction l;simpl;intros... + destruct a as (q,p);simpl. + rewrite IHl... Qed. Lemma fold_aux : forall a N (n:positive) l prod, @@ -459,8 +466,8 @@ Lemma fold_aux : forall a N (n:positive) l prod, fold_left (fun (r : Z) (k : positive * positive) => r * (a^(N / fst k) - 1)) l prod mod n. -Proof. - induction l;simpl;intros; mauto. +Proof with mauto. + induction l;simpl;intros ... Qed. Lemma fst_all_pow_mod : @@ -472,12 +479,12 @@ Lemma fst_all_pow_mod : (fold_left (fun r (k:positive*positive) => (r * (a ^ (R* mkProd' l / (fst k)) - 1))) l prod) mod n. -Proof. - induction l;simpl;intros; mauto. +Proof with mauto. + induction l;simpl;intros... destruct a0 as (q,p);simpl. assert (Z_of_N A = A mod n). - rewrite H1; mauto. - rewrite (IHl (R * q)%positive); mauto; mauto. + rewrite H1 ... + rewrite (IHl (R * q)%positive)... pattern (q * mkProd' l) at 2;rewrite (Zmult_comm q). repeat rewrite Zmult_assoc. rewrite Z_div_mult;auto with zmisc zarith. @@ -488,11 +495,12 @@ Proof. repeat rewrite (Zmult_mod prod);auto with zmisc. rewrite Zminus_mod;auto with zmisc. rewrite (Zminus_mod ((a ^ R) ^ mkProd' l));auto with zmisc. - rewrite (Zpower_mod (a^R));auto with zmisc. rewrite H1; mauto. - rewrite H3; mauto. - rewrite H1; mauto. + rewrite (Zpower_mod (a^R));auto with zmisc. rewrite H1... + rewrite H3... + rewrite H1 ... Qed. + Lemma is_odd_Zodd : forall p, is_odd p = true -> Zodd p. Proof. destruct p;intros;simpl;trivial;discriminate. @@ -540,11 +548,11 @@ Ltac spec_dec := repeat match goal with | [H:(?x ?= ?y)%P = _ |- _] => generalize (is_eq_spec x y); - rewrite H;clear H; autorewrite with zmisc; + rewrite H;clear H;simpl; autorewrite with zmisc; intro | [H:(?x ?< ?y)%P = _ |- _] => generalize (is_lt_spec x y); - rewrite H; clear H; autorewrite with zmisc; + rewrite H; clear H;simpl; autorewrite with zmisc; intro end. @@ -568,7 +576,7 @@ Proof. assert (Zpos (xO (xO (xO s))) = 8 * s). repeat rewrite Zpos_xO_add;ring. generalizeclear H1; rewrite H2;mauto;intros. apply (not_square sqrt). - simpl Z.of_N; rewrite H1;auto. + rewrite H1;auto. intros (y,Heq). generalize H1 Heq;mauto. unfold Z_of_N. @@ -579,32 +587,32 @@ Proof. destruct y;discriminate Heq2. Qed. +Opaque Zplus Pplus. Lemma in_mkProd_prime_div_in : forall p:positive, prime p -> forall (l:dec_prime), (forall k, In k l -> prime (fst k)) -> Zdivide p (mkProd l) -> exists n,In (p, n) l. -Proof. - induction l;simpl mkProd; simpl In; mauto. +Proof with mauto. + induction l;simpl ... intros _ H1; absurd (p <= 1). apply Zlt_not_le; apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. apply Zdivide_le; auto with zarith. - intros. - case prime_mult with (2 := H1); auto with zarith; intros H2. + intros; case prime_mult with (2 := H1); auto with zarith; intros H2. exists (snd a);left. destruct a;simpl in *. assert (Zpos p = Zpos p0). - rewrite (prime_div_Zpower_prime p1 p p0); mauto. + rewrite (prime_div_Zpower_prime p1 p p0)... apply (H0 (p0,p1));auto. - inversion H3; auto. - destruct IHl as (n,H3); mauto. - exists n; auto. + inversion H3... + destruct IHl as (n,H3)... + exists n... Qed. Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P). -Proof. +Proof with mauto. intros a;assert (Hacc := Zwf_pos a);induction Hacc;rename x into a;intros. - generalize (div_eucl_spec b a); mauto. + generalize (div_eucl_spec b a)... rewrite <- (Pmod_div_eucl b a). CaseEq (b mod a)%P;[intros Heq|intros r Heq]; intros (H1,H2). simpl in H1;rewrite Zplus_0_r in H1. @@ -621,57 +629,53 @@ Lemma test_pock_correct : forall N a dec sqrt, (forall k, In k dec -> prime (Zpos (fst k))) -> test_pock N a dec sqrt = true -> prime N. -Proof. +Proof with mauto. unfold test_pock;intros. elimif. generalize (div_eucl_spec (Ppred N) (mkProd dec)); - destruct ((Ppred N) / (mkProd dec))%P as (R1,n); mauto;intros (H2,H3). + destruct ((Ppred N) / (mkProd dec))%P as (R1,n);simpl;mauto;intros (H2,H3). destruct R1 as [|R1];try discriminate H0. destruct n;try discriminate H0. elimif. generalize (div_eucl_spec R1 (xO (mkProd dec))); - destruct ((R1 / xO (mkProd dec))%P) as (s,r'); mauto;intros (H7,H8). + destruct ((R1 / xO (mkProd dec))%P) as (s,r');simpl;mauto;intros (H7,H8). destruct r' as [|r];try discriminate H0. generalize (fst_all_pow_mod N a dec (R1*mkProd_pred dec) 1 (pow_mod_pred (pow_mod a R1 N) dec N)). generalize (snd_all_pow_mod N dec 1 (pow_mod_pred (pow_mod a R1 N) dec N)). destruct (all_pow_mod 1 (pow_mod_pred (pow_mod a R1 N) dec N) dec N) as - (prod,aNm1); mauto; simpl Z_of_N. + (prod,aNm1);simpl... destruct prod as [|prod];try discriminate H0. destruct aNm1 as [|aNm1];try discriminate H0;elimif. - simpl in H3; simpl in H2. + simpl in H2;rewrite Zplus_0_r in H2. rewrite <- Ppred_Zminus in H2;try omega. rewrite <- Zmult_assoc;rewrite mkProd_pred_mkProd. intros H12;assert (a^(N-1) mod N = 1). pattern 1 at 2;rewrite <- H9;symmetry. - simpl Z.of_N in H12. - rewrite H2; rewrite H12; mauto. - rewrite <- Zpower_mult; mauto. + rewrite H2;rewrite H12 ... + rewrite <- Zpower_mult... clear H12. intros H14. match type of H14 with _ -> _ -> _ -> ?X => assert (H12:X); try apply H14; clear H14 - end; mauto. - rewrite Zmod_small; mauto. + end... + rewrite Zmod_small... assert (1 < mkProd dec). assert (H14 := Zlt_0_pos (mkProd dec)). - assert (1 <= mkProd dec); mauto. - destruct (Zle_lt_or_eq _ _ H15); mauto. + assert (1 <= mkProd dec)... + destruct (Zle_lt_or_eq _ _ H15)... inversion H16. rewrite <- H18 in H5;discriminate H5. simpl in H8. assert (Z_of_N s = R1 / (2 * mkProd dec) /\ Zpos r = R1 mod (2 * mkProd dec)). apply mod_unique with (2 * mkProd dec);auto with zarith. - revert H8; mauto. - apply Z_mod_lt; mauto. - rewrite <- Z_div_mod_eq; mauto; rewrite H7. - simpl fst; simpl snd; simpl Z_of_N. - ring. + apply Z_mod_lt ... + rewrite <- Z_div_mod_eq... rewrite H7. simpl;ring. destruct H15 as (H15,Heqr). apply PocklingtonExtra with (F1:=mkProd dec) (R1:=R1) (m:=1); auto with zmisc zarith. - rewrite H2; mauto. - apply is_even_Zeven; auto. - apply is_odd_Zodd; auto. + rewrite H2;ring. + apply is_even_Zeven... + apply is_odd_Zodd... intros p; case p; clear p. intros HH; contradict HH. apply not_prime_0. @@ -688,7 +692,6 @@ Proof. pattern 1 at 3; rewrite <- H10; rewrite <- H12. apply Pmod.gcd_Zis_gcd. destruct (in_mkProd_prime_div_in _ Hprime _ H Hdec) as (q,Hin). - revert H2; mauto; intro H2. rewrite <- H2. match goal with |- context [fold_left ?f _ _] => apply (ListAux.fold_left_invol_in _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) @@ -697,9 +700,9 @@ Proof. rewrite <- Heqr. generalizeclear H0; ring_simplify (((mkProd dec + mkProd dec + r + 1) * mkProd dec + r) * mkProd dec + 1) - ((1 * mkProd dec + 1) * (2 * mkProd dec * mkProd dec + (r - 1) * mkProd dec + 1)); mauto. + ((1 * mkProd dec + 1) * (2 * mkProd dec * mkProd dec + (r - 1) * mkProd dec + 1))... rewrite <- H15;rewrite <- Heqr. - apply check_s_r_correct with sqrt; mauto. + apply check_s_r_correct with sqrt ... Qed. Lemma is_in_In : diff --git a/coqprime-8.5/Coqprime/Root.v b/coqprime-8.4/Coqprime/Root.v index 2f65790d6..4e74a4d2f 100644 --- a/coqprime-8.5/Coqprime/Root.v +++ b/coqprime-8.4/Coqprime/Root.v @@ -11,11 +11,11 @@ Proof that a polynomial has at most n roots ************************************************************************) -Require Import ZArith. -Require Import List. -Require Import UList. -Require Import Tactic. -Require Import Permutation. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coqprime.Permutation. Open Scope Z_scope. @@ -33,8 +33,8 @@ Let pol := list A. Definition toA z := match z with Z0 => zero -| Zpos p => iter_pos _ (plus one) zero p -| Zneg p => op (iter_pos _ (plus one) zero p) +| Zpos p => iter_pos p _ (plus one) zero +| Zneg p => op (iter_pos p _ (plus one) zero) end. Fixpoint eval (p: pol) (x: A) {struct p} : A := diff --git a/coqprime-8.5/Coqprime/Tactic.v b/coqprime-8.4/Coqprime/Tactic.v index 93a244149..93a244149 100644 --- a/coqprime-8.5/Coqprime/Tactic.v +++ b/coqprime-8.4/Coqprime/Tactic.v diff --git a/coqprime-8.5/Coqprime/UList.v b/coqprime-8.4/Coqprime/UList.v index 7b9d982ea..32ca6b2a0 100644 --- a/coqprime-8.5/Coqprime/UList.v +++ b/coqprime-8.4/Coqprime/UList.v @@ -7,33 +7,33 @@ (*************************************************************) (*********************************************************************** - UList.v - - Definition of list with distinct elements - - Definition: ulist + UList.v + + Definition of list with distinct elements + + Definition: ulist ************************************************************************) -Require Import List. -Require Import Arith. -Require Import Permutation. -Require Import ListSet. - +Require Import Coq.Lists.List. +Require Import Coq.Arith.Arith. +Require Import Coqprime.Permutation. +Require Import Coq.Lists.ListSet. + Section UniqueList. Variable A : Set. Variable eqA_dec : forall (a b : A), ({ a = b }) + ({ a <> b }). (* A list is unique if there is not twice the same element in the list *) - + Inductive ulist : list A -> Prop := ulist_nil: ulist nil | ulist_cons: forall a l, ~ In a l -> ulist l -> ulist (a :: l) . Hint Constructors ulist . (* Inversion theorem *) - + Theorem ulist_inv: forall a l, ulist (a :: l) -> ulist l. intros a l H; inversion H; auto. Qed. (* The append of two unique list is unique if the list are distinct *) - + Theorem ulist_app: forall l1 l2, ulist l1 -> @@ -48,18 +48,16 @@ apply ulist_inv with ( 1 := H0 ); auto. intros a0 H3 H4; apply (H2 a0); auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv: forall l1 l2 (a : A), ulist (l1 ++ l2) -> In a l1 -> In a l2 -> False. intros l1; elim l1; simpl; auto. -intros a l H l2 a0 H0 [H1|H1] H2. -inversion H0 as [|a1 l0 H3 H4 H5]; auto. -case H3; rewrite H1; auto with datatypes. -apply (H l2 a0); auto. -apply ulist_inv with ( 1 := H0 ); auto. +intros a l H l2 a0 H0 [H1|H1] H2; +inversion H0 as [|a1 l0 H3 H4 H5]; clear H0; auto; + subst; eauto using ulist_inv with datatypes. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv_l: forall (l1 l2 : list A), ulist (l1 ++ l2) -> ulist l1. intros l1; elim l1; simpl; auto. intros a l H l2 H0. @@ -68,13 +66,13 @@ intros H5; case iH2; auto with datatypes. apply H with l2; auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv_r: forall (l1 l2 : list A), ulist (l1 ++ l2) -> ulist l2. intros l1; elim l1; simpl; auto. intros a l H l2 H0; inversion H0; auto. Qed. (* Uniqueness is decidable *) - + Definition ulist_dec: forall l, ({ ulist l }) + ({ ~ ulist l }). intros l; elim l; auto. intros a l1 [H|H]; auto. @@ -83,7 +81,7 @@ right; red; intros H1; inversion H1; auto. right; intros H1; case H; apply ulist_inv with ( 1 := H1 ). Defined. (* Uniqueness is compatible with permutation *) - + Theorem ulist_perm: forall (l1 l2 : list A), permutation l1 l2 -> ulist l1 -> ulist l2. intros l1 l2 H; elim H; clear H l1 l2; simpl; auto. @@ -103,7 +101,7 @@ intros H; case iH1; simpl; auto. inversion_clear H0 as [|ia il iH1 iH2]; auto. inversion iH2; auto. Qed. - + Theorem ulist_def: forall l a, In a l -> ulist l -> ~ (exists l1 , permutation l (a :: (a :: l1)) ). @@ -112,7 +110,7 @@ absurd (ulist (a :: (a :: l1))); auto. intros H2; inversion_clear H2; simpl; auto with datatypes. apply ulist_perm with ( 1 := H1 ); auto. Qed. - + Theorem ulist_incl_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> (exists l3 , permutation l2 (l1 ++ l3) ). @@ -134,7 +132,7 @@ intros l4 H4; exists l4. apply permutation_trans with (a :: l3); auto. apply permutation_sym; auto. Qed. - + Theorem ulist_eq_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> length l1 = length l2 -> permutation l1 l2. @@ -150,7 +148,7 @@ replace l1 with (app l1 l3); auto. apply permutation_sym; auto. rewrite H5; rewrite app_nil_end; auto. Qed. - + Theorem ulist_incl_length: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> le (length l1) (length l2). @@ -166,8 +164,8 @@ intros l1 l2 H1 H2 H3 H4. apply ulist_eq_permutation; auto. apply le_antisym; apply ulist_incl_length; auto. Qed. - - + + Theorem ulist_incl_length_strict: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> ~ incl l2 l1 -> lt (length l1) (length l2). @@ -180,14 +178,14 @@ intros H2; case Hi0; auto. intros a HH; apply permutation_in with ( 1 := H2 ); auto. intros a l Hl0; (rewrite plus_comm; simpl; rewrite plus_comm; auto with arith). Qed. - + Theorem in_inv_dec: forall (a b : A) l, In a (cons b l) -> a = b \/ ~ a = b /\ In a l. intros a b l H; case (eqA_dec a b); auto; intros H1. right; split; auto; inversion H; auto. case H1; auto. Qed. - + Theorem in_ex_app_first: forall (a : A) (l : list A), In a l -> @@ -203,7 +201,7 @@ case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl; subst; auto. intros H4; case H4; auto. Qed. - + Theorem ulist_inv_ulist: forall (l : list A), ~ ulist l -> @@ -239,7 +237,7 @@ replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3)))) with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)); auto with datatypes. (repeat (rewrite <- ass_app; simpl)); auto. Qed. - + Theorem incl_length_repetition: forall (l1 l2 : list A), incl l1 l2 -> @@ -253,11 +251,11 @@ intros l1 l2 H H0; apply ulist_inv_ulist. intros H1; absurd (le (length l1) (length l2)); auto with arith. apply ulist_incl_length; auto. Qed. - + End UniqueList. Implicit Arguments ulist [A]. Hint Constructors ulist . - + Theorem ulist_map: forall (A B : Set) (f : A -> B) l, (forall x y, (In x l) -> (In y l) -> f x = f y -> x = y) -> ulist l -> ulist (map f l). @@ -270,7 +268,7 @@ case in_map_inv with ( 1 := H1 ); auto with datatypes. intros b1 [Hb1 Hb2]. replace a1 with b1; auto with datatypes. Qed. - + Theorem ulist_list_prod: forall (A : Set) (l1 l2 : list A), ulist l1 -> ulist l2 -> ulist (list_prod l1 l2). diff --git a/coqprime-8.5/Coqprime/ZCAux.v b/coqprime-8.4/Coqprime/ZCAux.v index de03a2fe2..aa47fb655 100644 --- a/coqprime-8.5/Coqprime/ZCAux.v +++ b/coqprime-8.4/Coqprime/ZCAux.v @@ -12,10 +12,10 @@ Auxillary functions & Theorems **********************************************************************) -Require Import ArithRing. -Require Export ZArith Zpow_facts. -Require Export Znumtheory. -Require Export Tactic. +Require Import Coq.setoid_ring.ArithRing. +Require Export Coq.ZArith.ZArith Coq.ZArith.Zpow_facts. +Require Export Coq.ZArith.Znumtheory. +Require Export Coqprime.Tactic. Theorem Zdivide_div_prime_le_square: forall x, 1 < x -> ~prime x -> exists p, prime p /\ (p | x) /\ p * p <= x. intros x Hx; generalize Hx; pattern x; apply Z_lt_induction; auto with zarith. diff --git a/coqprime-8.5/Coqprime/ZCmisc.v b/coqprime-8.4/Coqprime/ZCmisc.v index c1bdacc63..e2ec66ba1 100644 --- a/coqprime-8.5/Coqprime/ZCmisc.v +++ b/coqprime-8.4/Coqprime/ZCmisc.v @@ -6,7 +6,7 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export ZArith. +Require Export Coq.ZArith.ZArith. Open Local Scope Z_scope. Coercion Zpos : positive >-> Z. diff --git a/coqprime-8.5/Coqprime/ZProgression.v b/coqprime-8.4/Coqprime/ZProgression.v index 51ce91cdc..4cf30d692 100644 --- a/coqprime-8.5/Coqprime/ZProgression.v +++ b/coqprime-8.4/Coqprime/ZProgression.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export Iterator. -Require Import ZArith. -Require Export UList. +Require Export Coqprime.Iterator. +Require Import Coq.ZArith.ZArith. +Require Export Coqprime.UList. Open Scope Z_scope. Theorem next_n_Z: forall n m, next_n Zsucc n m = n + Z_of_nat m. diff --git a/coqprime-8.5/Coqprime/ZSum.v b/coqprime-8.4/Coqprime/ZSum.v index 3a7f14065..907720f7c 100644 --- a/coqprime-8.5/Coqprime/ZSum.v +++ b/coqprime-8.4/Coqprime/ZSum.v @@ -9,12 +9,12 @@ (*********************************************************************** Summation.v from Z to Z *********************************************************************) -Require Import Arith. -Require Import ArithRing. -Require Import ListAux. -Require Import ZArith. -Require Import Iterator. -Require Import ZProgression. +Require Import Coq.Arith.Arith. +Require Import Coq.setoid_ring.ArithRing. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith. +Require Import Coqprime.Iterator. +Require Import Coqprime.ZProgression. Open Scope Z_scope. diff --git a/coqprime-8.5/Coqprime/Zp.v b/coqprime-8.4/Coqprime/Zp.v index 1e5295191..2f7d28d69 100644 --- a/coqprime-8.5/Coqprime/Zp.v +++ b/coqprime-8.4/Coqprime/Zp.v @@ -14,16 +14,16 @@ Definition: ZpGroup **********************************************************************) -Require Import ZArith Znumtheory Zpow_facts. -Require Import Tactic. -Require Import Wf_nat. -Require Import UList. -Require Import FGroup. -Require Import EGroup. -Require Import IGroup. -Require Import Cyclic. -Require Import Euler. -Require Import ZProgression. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.ZArith.Zpow_facts. +Require Import Coqprime.Tactic. +Require Import Coq.Arith.Wf_nat. +Require Import Coqprime.UList. +Require Import Coqprime.FGroup. +Require Import Coqprime.EGroup. +Require Import Coqprime.IGroup. +Require Import Coqprime.Cyclic. +Require Import Coqprime.Euler. +Require Import Coqprime.ZProgression. Open Scope Z_scope. diff --git a/coqprime-8.5/Makefile b/coqprime-8.4/Makefile index c8e44a658..8fa838a1e 100644 --- a/coqprime-8.5/Makefile +++ b/coqprime-8.4/Makefile @@ -2,7 +2,7 @@ ## v # The Coq Proof Assistant ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.5pl1 ## +## // # Makefile automagically generated by coq_makefile V8.4pl6 ## ############################################################################# # WARNING @@ -19,10 +19,9 @@ .DEFAULT_GOAL := all +# # This Makefile may take arguments passed as environment variables: # COQBIN to specify the directory where Coq binaries resides; -# TIMECMD set a command to log .v compilation time; -# TIMED if non empty, use the default time command as TIMECMD; # ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; # DSTROOT to specify a prefix to install path. @@ -34,25 +33,14 @@ endef includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) $(call includecmdwithout@,$(COQBIN)coqtop -config) -TIMED= -TIMECMD= -STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - -vo_to_obj = $(addsuffix .o,\ - $(filter-out Warning: Error:,\ - $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) - ########################## # # # Libraries definitions. # # # ########################## -COQLIBS?=\ - -R "Coqprime" Coqprime -COQDOCLIBS?=\ - -R "Coqprime" Coqprime +COQLIBS?= -R Coqprime Coqprime +COQDOCLIBS?=-R Coqprime Coqprime ########################## # # @@ -66,11 +54,10 @@ COQDEP?="$(COQBIN)coqdep" -c COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) COQCHKFLAGS?=-silent -o COQDOCFLAGS?=-interpolate -utf8 -COQC?=$(TIMER) "$(COQBIN)coqc" +COQC?="$(COQBIN)coqc" GALLINA?="$(COQBIN)gallina" COQDOC?="$(COQBIN)coqdoc" COQCHK?="$(COQBIN)coqchk" -COQMKTOP?="$(COQBIN)coqmktop" ################## # # @@ -85,7 +72,6 @@ COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq else COQLIBINSTALL="${COQLIB}user-contrib" COQDOCINSTALL="${DOCDIR}user-contrib" -COQTOPINSTALL="${COQLIB}toploop" endif ###################### @@ -94,51 +80,40 @@ endif # # ###################### -VFILES:=Coqprime/Cyclic.v\ - Coqprime/EGroup.v\ - Coqprime/Euler.v\ - Coqprime/FGroup.v\ - Coqprime/IGroup.v\ - Coqprime/Iterator.v\ - Coqprime/Lagrange.v\ - Coqprime/ListAux.v\ - Coqprime/LucasLehmer.v\ - Coqprime/NatAux.v\ - Coqprime/PGroup.v\ - Coqprime/Permutation.v\ - Coqprime/Pmod.v\ - Coqprime/Pocklington.v\ - Coqprime/PocklingtonCertificat.v\ - Coqprime/Root.v\ - Coqprime/Tactic.v\ - Coqprime/UList.v\ - Coqprime/ZCAux.v\ - Coqprime/ZCmisc.v\ - Coqprime/ZProgression.v\ +VFILES:=Coqprime/Zp.v\ Coqprime/ZSum.v\ - Coqprime/Zp.v + Coqprime/ZProgression.v\ + Coqprime/ZCmisc.v\ + Coqprime/ZCAux.v\ + Coqprime/UList.v\ + Coqprime/Tactic.v\ + Coqprime/Root.v\ + Coqprime/PocklingtonCertificat.v\ + Coqprime/Pocklington.v\ + Coqprime/Pmod.v\ + Coqprime/Permutation.v\ + Coqprime/PGroup.v\ + Coqprime/NatAux.v\ + Coqprime/LucasLehmer.v\ + Coqprime/ListAux.v\ + Coqprime/Lagrange.v\ + Coqprime/Iterator.v\ + Coqprime/IGroup.v\ + Coqprime/FGroup.v\ + Coqprime/Euler.v\ + Coqprime/EGroup.v\ + Coqprime/Cyclic.v -ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) --include $(addsuffix .d,$(VFILES)) -else -ifeq ($(MAKECMDGOALS),) -include $(addsuffix .d,$(VFILES)) -endif -endif - .SECONDARY: $(addsuffix .d,$(VFILES)) -VO=vo -VOFILES:=$(VFILES:.v=.$(VO)) +VOFILES:=$(VFILES:.v=.vo) VOFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(VOFILES))) GLOBFILES:=$(VFILES:.v=.glob) +VIFILES:=$(VFILES:.v=.vi) GFILES:=$(VFILES:.v=.g) HTMLFILES:=$(VFILES:.v=.html) GHTMLFILES:=$(VFILES:.v=.g.html) -OBJFILES=$(call vo_to_obj,$(VOFILES)) -ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs) -NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) -NATIVEFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(NATIVEFILES))) ifeq '$(HASNATDYNLINK)' 'true' HASNATDYNLINK_OR_EMPTY := yes else @@ -153,12 +128,8 @@ endif all: $(VOFILES) -quick: $(VOFILES:.vo=.vio) +spec: $(VIFILES) -vio2vo: - $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) -checkproofs: - $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) gallina: $(GFILES) html: $(GLOBFILES) $(VFILES) @@ -189,7 +160,7 @@ beautify: $(VFILES:=.beautified) @echo 'Do not do "make clean" until you are sure that everything went well!' @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo +.PHONY: all opt byte archclean clean install userinstall depend html validate #################### # # @@ -207,7 +178,7 @@ userinstall: +$(MAKE) USERINSTALL=true install install: - cd "Coqprime" && for i in $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1); do \ + cd "Coqprime"; for i in $(VOFILES1); do \ install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \ install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \ done @@ -218,46 +189,12 @@ install-doc: install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/Coqprime/$$i;\ done -uninstall_me.sh: Makefile - echo '#!/bin/sh' > $@ - printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/Coqprime && rm -f $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "Coqprime" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/Coqprime \\\n' >> "$@" - printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@" - printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find Coqprime/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" - chmod +x $@ - -uninstall: uninstall_me.sh - sh $< - -.merlin: - @echo 'FLG -rectypes' > .merlin - @echo "B $(COQLIB) kernel" >> .merlin - @echo "B $(COQLIB) lib" >> .merlin - @echo "B $(COQLIB) library" >> .merlin - @echo "B $(COQLIB) parsing" >> .merlin - @echo "B $(COQLIB) pretyping" >> .merlin - @echo "B $(COQLIB) interp" >> .merlin - @echo "B $(COQLIB) printing" >> .merlin - @echo "B $(COQLIB) intf" >> .merlin - @echo "B $(COQLIB) proofs" >> .merlin - @echo "B $(COQLIB) tactics" >> .merlin - @echo "B $(COQLIB) tools" >> .merlin - @echo "B $(COQLIB) toplevel" >> .merlin - @echo "B $(COQLIB) stm" >> .merlin - @echo "B $(COQLIB) grammar" >> .merlin - @echo "B $(COQLIB) config" >> .merlin - -clean:: - rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES) - find . -name .coq-native -type d -empty -delete - rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) +clean: + rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - - rm -rf html mlihtml uninstall_me.sh + - rm -rf html mlihtml -cleanall:: clean - rm -f $(patsubst %.v,.%.aux,$(VFILES)) - -archclean:: +archclean: rm -f *.cmx *.o printenv: @@ -280,34 +217,31 @@ Makefile: _CoqProject # # ################### -$(VOFILES): %.vo: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -$(GLOBFILES): %.glob: %.v +%.vo %.glob: %.v $(COQC) $(COQDEBUG) $(COQFLAGS) $* -$(VFILES:.v=.vio): %.vio: %.v - $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $* +%.vi: %.v + $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* -$(GFILES): %.g: %.v +%.g: %.v $(GALLINA) $< -$(VFILES:.v=.tex): %.tex: %.v +%.tex: %.v $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ -$(HTMLFILES): %.html: %.v %.glob +%.html: %.v %.glob $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ -$(VFILES:.v=.g.tex): %.g.tex: %.v +%.g.tex: %.v $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ -$(GHTMLFILES): %.g.html: %.v %.glob +%.g.html: %.v %.glob $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ -$(addsuffix .d,$(VFILES)): %.v.d: %.v - $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) +%.v.d: %.v + $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) -$(addsuffix .beautified,$(VFILES)): %.v.beautified: +%.v.beautified: $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* # WARNING diff --git a/coqprime-8.4/README.md b/coqprime-8.4/README.md new file mode 100644 index 000000000..8f1b93b12 --- /dev/null +++ b/coqprime-8.4/README.md @@ -0,0 +1,9 @@ +# Coqprime (LGPL subset) + +This is a mirror of the LGPL-licensed and autogenerated files from [Coqprime](http://coqprime.gforge.inria.fr/) for Coq 8.4. It was generated from [coqprime_par.zip](https://gforge.inria.fr/frs/download.php/file/35201/coqprime_par.zip). Due to the removal of files that are missing license headers in the upstream source, `make` no longer completes successfully. However, a large part of the codebase does build and contains theorems useful to us. Fixing the build system would be nice, but is not a priority for us. + +## Usage + + make PrimalityTest/Zp.vo PrimalityTest/PocklingtonCertificat.vo + cd .. + coqide -R coqprime/Tactic Coqprime -R coqprime/N Coqprime -R coqprime/Z Coqprime -R coqprime/List Coqprime -R coqprime/PrimalityTest Coqprime YOUR_FILE.v # these are the dependencies for PrimalityTest/Zp, other modules can be added in a similar fashion diff --git a/coqprime-8.5/_CoqProject b/coqprime-8.4/_CoqProject index 95b224864..95b224864 100644 --- a/coqprime-8.5/_CoqProject +++ b/coqprime-8.4/_CoqProject diff --git a/coqprime-8.5/README.md b/coqprime-8.5/README.md deleted file mode 100644 index 9c317fb00..000000000 --- a/coqprime-8.5/README.md +++ /dev/null @@ -1,9 +0,0 @@ -# Coqprime (LGPL subset) - -This is a mirror of the LGPL-licensed and autogenerated files from [Coqprime](http://coqprime.gforge.inria.fr/) for Coq 8.5. It was generated from [coqprime_8.5b.zip](https://gforge.inria.fr/frs/download.php/file/35520/coqprime_8.5b.zip). Due to the removal of files that are missing license headers in the upstream source, `make` no longer completes successfully. However, a large part of the codebase does build and contains theorems useful to us. Fixing the build system would be nice, but is not a priority for us. - -## Usage - - make PrimalityTest/Zp.vo PrimalityTest/PocklingtonCertificat.vo - cd .. - coqide -R coqprime/Tactic Coqprime -R coqprime/N Coqprime -R coqprime/Z Coqprime -R coqprime/List Coqprime -R coqprime/PrimalityTest Coqprime YOUR_FILE.v # these are the dependencies for PrimalityTest/Zp, other modules can be added in a similar fashion diff --git a/coqprime/Coqprime/Cyclic.v b/coqprime/Coqprime/Cyclic.v index e2daa4d67..c25f683ca 100644 --- a/coqprime/Coqprime/Cyclic.v +++ b/coqprime/Coqprime/Cyclic.v @@ -11,13 +11,13 @@ Proof that an abelien ring is cyclic ************************************************************************) -Require Import Coqprime.ZCAux. -Require Import Coq.Lists.List. -Require Import Coqprime.Root. -Require Import Coqprime.UList. -Require Import Coqprime.IGroup. -Require Import Coqprime.EGroup. -Require Import Coqprime.FGroup. +Require Import ZCAux. +Require Import List. +Require Import Root. +Require Import UList. +Require Import IGroup. +Require Import EGroup. +Require Import FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/EGroup.v b/coqprime/Coqprime/EGroup.v index 553cb746c..933176abd 100644 --- a/coqprime/Coqprime/EGroup.v +++ b/coqprime/Coqprime/EGroup.v @@ -11,15 +11,15 @@ Given an element a, create the group {e, a, a^2, ..., a^n} **********************************************************************) -Require Import Coq.ZArith.ZArith. -Require Import Coqprime.Tactic. -Require Import Coq.Lists.List. -Require Import Coqprime.ZCAux. -Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Coq.Arith.Wf_nat. -Require Import Coqprime.UList. -Require Import Coqprime.FGroup. -Require Import Coqprime.Lagrange. +Require Import ZArith. +Require Import Tactic. +Require Import List. +Require Import ZCAux. +Require Import ZArith Znumtheory. +Require Import Wf_nat. +Require Import UList. +Require Import FGroup. +Require Import Lagrange. Open Scope Z_scope. @@ -43,7 +43,7 @@ Hypothesis a_in_G: In a G.(s). **************************************) Set Implicit Arguments. -Definition gpow n := match n with Zpos p => iter_pos p _ (op a) G.(e) | _ => G.(e) end. +Definition gpow n := match n with Zpos p => iter_pos _ (op a) G.(e) p | _ => G.(e) end. Unset Implicit Arguments. Theorem gpow_0: gpow 0 = G.(e). @@ -63,17 +63,17 @@ intros n; case n; simpl; auto. intros p; apply iter_pos_invariant with (Inv := fun x => In x G.(s)); auto. Qed. -Theorem gpow_op: forall b p, In b G.(s) -> iter_pos p _ (op a) b = op (iter_pos p _ (op a) G.(e)) b. +Theorem gpow_op: forall b p, In b G.(s) -> iter_pos _ (op a) b p = op (iter_pos _ (op a) G.(e) p) b. intros b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b Hb. assert (H: In (gpow (Zpos p)) G.(s)). apply gpow_in. -rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos p A x y)); auto. +rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos A x y p)); auto. repeat rewrite G.(assoc); auto. intros p Rec b Hb. assert (H: In (gpow (Zpos p)) G.(s)). apply gpow_in. -rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos p A x y)); auto. +rewrite (Rec b); try rewrite (fun x y => Rec (op x y)); try rewrite (fun x y => Rec (iter_pos A x y p)); auto. repeat rewrite G.(assoc); auto. intros b H; rewrite e_is_zero_r; auto. Qed. @@ -87,7 +87,7 @@ intros _ _; simpl; apply sym_equal; apply e_is_zero_r. exact (gpow_in (Zpos p1)). 2: intros p2 _ H; contradict H; auto with zarith. intros p2 _ _; simpl. -rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos p2 A x y)); auto. +rewrite iter_pos_plus; rewrite (fun x y => gpow_op (iter_pos A x y p2)); auto. exact (gpow_in (Zpos p2)). Qed. @@ -445,7 +445,7 @@ intros x H2 Rec _; unfold Zsucc; rewrite gpow_add; simpl; auto with zarith. repeat rewrite G.(e_is_zero_r); auto with zarith. apply gpow_in; sauto. intros p1 _; case m; simpl; auto. -assert(H1: In (iter_pos p1 A (op a) (e G)) (s G)). +assert(H1: In (iter_pos A (op a) (e G) p1) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p1)); auto. intros p2 _; pattern p2; apply Pind; simpl; auto. rewrite Pmult_1_r; rewrite G.(e_is_zero_r); try rewrite G.(e_is_zero_r); auto. @@ -486,12 +486,12 @@ repeat rewrite iter_pos_plus; simpl. repeat rewrite (fun x y H z => gpow_op A op x G H (op y z)) ; auto. rewrite Rec. repeat rewrite G.(e_is_zero_r); auto. -assert(H1: In (iter_pos p3 A (op a) (e G)) (s G)). +assert(H1: In (iter_pos A (op a) (e G) p3) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p3)); auto. -assert(H2: In (iter_pos p3 A (op b) (e G)) (s G)). +assert(H2: In (iter_pos A (op b) (e G) p3) (s G)). refine (gpow_in _ _ _ _ _ (Zpos p3)); auto. repeat rewrite <- G.(assoc); try eq_tac; auto. -rewrite (fun x y => comm (iter_pos p3 A x y) b); auto. +rewrite (fun x y => comm (iter_pos A x y p3) b); auto. rewrite (G.(assoc) a); try apply comm; auto. Qed. diff --git a/coqprime/Coqprime/Euler.v b/coqprime/Coqprime/Euler.v index e571d8e3c..06d92ce57 100644 --- a/coqprime/Coqprime/Euler.v +++ b/coqprime/Coqprime/Euler.v @@ -11,10 +11,10 @@ Definition of the Euler Totient function *************************************************************************) -Require Import Coq.ZArith.ZArith. -Require Export Coq.ZArith.Znumtheory. -Require Import Coqprime.Tactic. -Require Export Coqprime.ZSum. +Require Import ZArith. +Require Export Znumtheory. +Require Import Tactic. +Require Export ZSum. Open Scope Z_scope. diff --git a/coqprime/Coqprime/FGroup.v b/coqprime/Coqprime/FGroup.v index 0bcc9ebf1..a55710e7c 100644 --- a/coqprime/Coqprime/FGroup.v +++ b/coqprime/Coqprime/FGroup.v @@ -13,10 +13,10 @@ Definition: FGroup **********************************************************************) -Require Import Coq.Lists.List. -Require Import Coqprime.UList. -Require Import Coqprime.Tactic. -Require Import Coq.ZArith.ZArith. +Require Import List. +Require Import UList. +Require Import Tactic. +Require Import ZArith. Open Scope Z_scope. diff --git a/coqprime/Coqprime/IGroup.v b/coqprime/Coqprime/IGroup.v index 04219be5a..11a73d414 100644 --- a/coqprime/Coqprime/IGroup.v +++ b/coqprime/Coqprime/IGroup.v @@ -13,12 +13,12 @@ Definition: ZpGroup **********************************************************************) -Require Import Coq.ZArith.ZArith. -Require Import Coqprime.Tactic. -Require Import Coq.Arith.Wf_nat. -Require Import Coqprime.UList. -Require Import Coqprime.ListAux. -Require Import Coqprime.FGroup. +Require Import ZArith. +Require Import Tactic. +Require Import Wf_nat. +Require Import UList. +Require Import ListAux. +Require Import FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Iterator.v b/coqprime/Coqprime/Iterator.v index e84687cd4..96d3e5655 100644 --- a/coqprime/Coqprime/Iterator.v +++ b/coqprime/Coqprime/Iterator.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export Coq.Lists.List. -Require Export Coqprime.Permutation. -Require Import Coq.Arith.Arith. +Require Export List. +Require Export Permutation. +Require Import Arith. Section Iterator. Variables A B : Set. diff --git a/coqprime/Coqprime/Lagrange.v b/coqprime/Coqprime/Lagrange.v index b890c5621..b35460bad 100644 --- a/coqprime/Coqprime/Lagrange.v +++ b/coqprime/Coqprime/Lagrange.v @@ -14,12 +14,12 @@ Definition: lagrange **********************************************************************) -Require Import Coq.Lists.List. -Require Import Coqprime.UList. -Require Import Coqprime.ListAux. -Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. -Require Import Coqprime.NatAux. -Require Import Coqprime.FGroup. +Require Import List. +Require Import UList. +Require Import ListAux. +Require Import ZArith Znumtheory. +Require Import NatAux. +Require Import FGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/ListAux.v b/coqprime/Coqprime/ListAux.v index 4ed154685..c3c9602bd 100644 --- a/coqprime/Coqprime/ListAux.v +++ b/coqprime/Coqprime/ListAux.v @@ -11,11 +11,11 @@ Auxillary functions & Theorems **********************************************************************) -Require Export Coq.Lists.List. -Require Export Coq.Arith.Arith. -Require Export Coqprime.Tactic. -Require Import Coq.Wellfounded.Inverse_Image. -Require Import Coq.Arith.Wf_nat. +Require Export List. +Require Export Arith. +Require Export Tactic. +Require Import Inverse_Image. +Require Import Wf_nat. (************************************** Some properties on list operators: app, map,... diff --git a/coqprime/Coqprime/LucasLehmer.v b/coqprime/Coqprime/LucasLehmer.v index c459195a8..a0e3b8e46 100644 --- a/coqprime/Coqprime/LucasLehmer.v +++ b/coqprime/Coqprime/LucasLehmer.v @@ -13,17 +13,17 @@ Definition: LucasLehmer **********************************************************************) -Require Import Coq.ZArith.ZArith. -Require Import Coqprime.ZCAux. -Require Import Coqprime.Tactic. -Require Import Coq.Arith.Wf_nat. -Require Import Coqprime.NatAux. -Require Import Coqprime.UList. -Require Import Coqprime.ListAux. -Require Import Coqprime.FGroup. -Require Import Coqprime.EGroup. -Require Import Coqprime.PGroup. -Require Import Coqprime.IGroup. +Require Import ZArith. +Require Import ZCAux. +Require Import Tactic. +Require Import Wf_nat. +Require Import NatAux. +Require Import UList. +Require Import ListAux. +Require Import FGroup. +Require Import EGroup. +Require Import PGroup. +Require Import IGroup. Open Scope Z_scope. @@ -47,7 +47,7 @@ Qed. Definition of the power function for pairs p^n **************************************) -Definition ppow p n := match n with Zpos q => iter_pos q _ (pmult p) (1, 0) | _ => (1, 0) end. +Definition ppow p n := match n with Zpos q => iter_pos _ (pmult p) (1, 0) q | _ => (1, 0) end. (************************************** Some properties of ppow @@ -63,14 +63,14 @@ intros p; apply iter_pos_invariant with (Inv := fun x => x = (1, 0)); auto. intros x H; rewrite H; auto. Qed. -Theorem ppow_op: forall a b p, iter_pos p _ (pmult a) b = pmult (iter_pos p _ (pmult a) (1, 0)) b. +Theorem ppow_op: forall a b p, iter_pos _ (pmult a) b p = pmult (iter_pos _ (pmult a) (1, 0) p) b. intros a b p; generalize b; elim p; simpl; auto; clear b p. intros p Rec b. rewrite (Rec b). -try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos p _ x y)); auto. +try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. repeat rewrite pmult_assoc; auto. intros p Rec b. -rewrite (Rec b); try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos p _ x y)); auto. +rewrite (Rec b); try rewrite (fun x y => Rec (pmult x y)); try rewrite (fun x y => Rec (iter_pos _ x y p)); auto. repeat rewrite pmult_assoc; auto. intros b; rewrite pmult_1_r; auto. Qed. @@ -114,7 +114,7 @@ repeat rewrite (fun x y z => ppow_op x (pmult y z)) ; auto. rewrite Rec. repeat rewrite pmult_1_r; auto. repeat rewrite <- pmult_assoc; try eq_tac; auto. -rewrite (fun x y => pmult_comm (iter_pos p3 _ x y) p); auto. +rewrite (fun x y => pmult_comm (iter_pos _ x y p3) p); auto. rewrite (pmult_assoc m); try apply pmult_comm; auto. Qed. @@ -490,13 +490,13 @@ End Lucas. Definition SS p := let n := Mp p in match p - 2 with - Zpos p1 => iter_pos p1 _ (fun x => Zmodd (Zsquare x - 2) n) (Zmodd 4 n) + Zpos p1 => iter_pos _ (fun x => Zmodd (Zsquare x - 2) n) (Zmodd 4 n) p1 | _ => (Zmodd 4 n) end. Theorem SS_aux_correct: forall p z1 z2 n, 0 <= n -> 0 < z1 -> z2 = fst (s n) mod z1 -> - iter_pos p _ (fun x => Zmodd (Zsquare x - 2) z1) z2 = fst (s (n + Zpos p)) mod z1. + iter_pos _ (fun x => Zmodd (Zsquare x - 2) z1) z2 p = fst (s (n + Zpos p)) mod z1. intros p; pattern p; apply Pind. simpl. intros z1 z2 n Hn H H1; rewrite sn; auto; rewrite H1; rewrite Zmodd_correct; rewrite Zsquare_correct; simpl. diff --git a/coqprime/Coqprime/NatAux.v b/coqprime/Coqprime/NatAux.v index 6df511eed..eab09150c 100644 --- a/coqprime/Coqprime/NatAux.v +++ b/coqprime/Coqprime/NatAux.v @@ -11,7 +11,7 @@ Auxillary functions & Theorems **********************************************************************) -Require Export Coq.Arith.Arith. +Require Export Arith. (************************************** Some properties of minus diff --git a/coqprime/Coqprime/PGroup.v b/coqprime/Coqprime/PGroup.v index 19eff5850..e9c1b2f47 100644 --- a/coqprime/Coqprime/PGroup.v +++ b/coqprime/Coqprime/PGroup.v @@ -14,15 +14,15 @@ Definition: PGroup **********************************************************************) -Require Import Coq.ZArith.ZArith. -Require Import Coq.ZArith.Znumtheory. -Require Import Coqprime.Tactic. -Require Import Coq.Arith.Wf_nat. -Require Import Coqprime.ListAux. -Require Import Coqprime.UList. -Require Import Coqprime.FGroup. -Require Import Coqprime.EGroup. -Require Import Coqprime.IGroup. +Require Import ZArith. +Require Import Znumtheory. +Require Import Tactic. +Require Import Wf_nat. +Require Import ListAux. +Require Import UList. +Require Import FGroup. +Require Import EGroup. +Require Import IGroup. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Permutation.v b/coqprime/Coqprime/Permutation.v index 7cb6f629d..a06693f89 100644 --- a/coqprime/Coqprime/Permutation.v +++ b/coqprime/Coqprime/Permutation.v @@ -11,8 +11,8 @@ Defintion and properties of permutations **********************************************************************) -Require Export Coq.Lists.List. -Require Export Coqprime.ListAux. +Require Export List. +Require Export ListAux. Section permutation. Variable A : Set. diff --git a/coqprime/Coqprime/Pmod.v b/coqprime/Coqprime/Pmod.v index 45961896e..f64af48e3 100644 --- a/coqprime/Coqprime/Pmod.v +++ b/coqprime/Coqprime/Pmod.v @@ -6,8 +6,8 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export Coq.ZArith.ZArith. -Require Export Coqprime.ZCmisc. +Require Export ZArith. +Require Export ZCmisc. Open Local Scope positive_scope. @@ -392,7 +392,7 @@ Lemma gcd_log2_mod0 : Proof. intros a b c H;destruct c;simpl;rewrite H;trivial. Qed. -Require Import Coq.ZArith.Zwf. +Require Import Zwf. Lemma Zwf_pos : well_founded (fun x y => Zpos x < Zpos y). Proof. @@ -510,8 +510,8 @@ Proof. destruct (gcd_log2 b r r);intros;trivial. Qed. -Require Import Coq.ZArith.ZArith. -Require Import Coq.ZArith.Znumtheory. +Require Import ZArith. +Require Import Znumtheory. Hint Rewrite Zpos_mult times_Zmult square_Zmult Psucc_Zplus: zmisc. diff --git a/coqprime/Coqprime/Pocklington.v b/coqprime/Coqprime/Pocklington.v index 79e7dc616..9871cd3e6 100644 --- a/coqprime/Coqprime/Pocklington.v +++ b/coqprime/Coqprime/Pocklington.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import Coq.ZArith.ZArith. -Require Export Coq.ZArith.Znumtheory. -Require Import Coqprime.Tactic. -Require Import Coqprime.ZCAux. -Require Import Coqprime.Zp. -Require Import Coqprime.FGroup. -Require Import Coqprime.EGroup. -Require Import Coqprime.Euler. +Require Import ZArith. +Require Export Znumtheory. +Require Import Tactic. +Require Import ZCAux. +Require Import Zp. +Require Import FGroup. +Require Import EGroup. +Require Import Euler. Open Scope Z_scope. diff --git a/coqprime/Coqprime/PocklingtonCertificat.v b/coqprime/Coqprime/PocklingtonCertificat.v index fccea30b6..ecf4462ed 100644 --- a/coqprime/Coqprime/PocklingtonCertificat.v +++ b/coqprime/Coqprime/PocklingtonCertificat.v @@ -6,14 +6,14 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Import Coq.Lists.List. -Require Import Coq.ZArith.ZArith. -Require Import Coq.ZArith.Zorder. -Require Import Coqprime.ZCAux. -Require Import Coqprime.LucasLehmer. -Require Import Coqprime.Pocklington. -Require Import Coqprime.ZCmisc. -Require Import Coqprime.Pmod. +Require Import List. +Require Import ZArith. +Require Import Zorder. +Require Import ZCAux. +Require Import LucasLehmer. +Require Import Pocklington. +Require Import ZCmisc. +Require Import Pmod. Definition dec_prime := list (positive * positive). @@ -61,18 +61,18 @@ Definition mkProd (l:dec_prime) := (* [pow_mod a m n] return [a^m mod n] *) Fixpoint pow_mod (a m n : positive) {struct m} : N := match m with - | xH => (a mod n) + | xH => (a mod n)%P | xO m' => let z := pow_mod a m' n in match z with | N0 => 0%N - | Npos z' => ((square z') mod n) + | Npos z' => ((square z') mod n)%P end | xI m' => let z := pow_mod a m' n in match z with | N0 => 0%N - | Npos z' => ((square z') * a)%P mod n + | Npos z' => (((square z') * a)%P mod n)%P end end. @@ -118,7 +118,7 @@ Fixpoint pow_mod_pred (a:N) (l:dec_prime) (n:positive) {struct l} : N := | (q,p)::l => if (p ?= 1) then pow_mod_pred a l n else - let a' := iter_pos (Ppred p) _ (fun x => Npow_mod x q n) a in + let a' := iter_pos _ (fun x => Npow_mod x q n) a (Ppred p) in pow_mod_pred a' l n end. @@ -332,120 +332,113 @@ Hint Rewrite Pmod_Zmod : zmisc. Lemma Zpower_0 : forall p : positive, 0^p = 0. Proof. intros;simpl;destruct p;unfold Zpower_pos;simpl;trivial. - generalize (iter_pos p Z (Z.mul 0) 1). + generalize (iter_pos Z (Z.mul 0) 1 p). induction p;simpl;trivial. Qed. -Opaque Zpower. -Opaque Zmult. - Lemma pow_Zpower : forall a p, Zpos (pow a p) = a ^ p. -Proof with mauto. - induction p;simpl... rewrite IHp... rewrite IHp... +Proof. + induction p; mauto; simpl; mauto; rewrite IHp; mauto. Qed. Hint Rewrite pow_Zpower : zmisc. Lemma pow_mod_spec : forall n a m, Z_of_N (pow_mod a m n) = a^m mod n. -Proof with mauto. - induction m;simpl;intros... +Proof. + induction m; mauto; simpl; intros; mauto. rewrite Zmult_mod; auto with zmisc. - rewrite (Zmult_mod (a^m)); auto with zmisc. rewrite <- IHm. - destruct (pow_mod a m n);simpl... - rewrite Zmult_mod; auto with zmisc. - rewrite <- IHm. destruct (pow_mod a m n);simpl... + rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. + rewrite <- IHm; mauto. + destruct (pow_mod a m n); mauto. + rewrite (Zmult_mod (a^m)(a^m)); auto with zmisc. + rewrite <- IHm. destruct (pow_mod a m n);simpl; mauto. Qed. Hint Rewrite pow_mod_spec Zpower_0 : zmisc. Lemma Npow_mod_spec : forall a p n, Z_of_N (Npow_mod a p n) = a^p mod n. -Proof with mauto. - intros a p n;destruct a;simpl ... +Proof. + intros a p n;destruct a; mauto; simpl; mauto. Qed. Hint Rewrite Npow_mod_spec : zmisc. Lemma iter_Npow_mod_spec : forall n q p a, - Z_of_N (iter_pos p N (fun x : N => Npow_mod x q n) a) = a^q^p mod n. -Proof with mauto. - induction p;simpl;intros ... - repeat rewrite IHp. + Z_of_N (iter_pos N (fun x : N => Npow_mod x q n) a p) = a^q^p mod n. +Proof. + induction p; mauto; intros; simpl Pos.iter; mauto; repeat rewrite IHp. rewrite (Zpower_mod ((a ^ q ^ p) ^ q ^ p));auto with zmisc. - rewrite (Zpower_mod (a ^ q ^ p))... - repeat rewrite IHp... + rewrite (Zpower_mod (a ^ q ^ p)); mauto. + mauto. Qed. -Hint Rewrite iter_Npow_mod_spec : zmisc. - +Hint Rewrite iter_Npow_mod_spec : zmisc. Lemma fold_pow_mod_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> Z_of_N (fold_pow_mod a l n) = a^(mkProd' l) mod n. -Proof with mauto. - unfold fold_pow_mod;induction l;simpl;intros ... - rewrite IHl... +Proof. + unfold fold_pow_mod;induction l; simpl fold_left; simpl mkProd'; + intros; mauto. + rewrite IHl; mauto. Qed. Hint Rewrite fold_pow_mod_spec : zmisc. Lemma pow_mod_pred_spec : forall (n:positive) l (a:N), Z_of_N a = a mod n -> Z_of_N (pow_mod_pred a l n) = a^(mkProd_pred l) mod n. -Proof with mauto. - unfold pow_mod_pred;induction l;simpl;intros ... - destruct a as (q,p);simpl. - destruct (p ?= 1)%P; rewrite IHl... +Proof. + unfold pow_mod_pred;induction l;simpl mkProd;intros; mauto. + destruct a as (q,p). + simpl mkProd_pred. + destruct (p ?= 1)%P; rewrite IHl; mauto; simpl. Qed. Hint Rewrite pow_mod_pred_spec : zmisc. Lemma mkProd_pred_mkProd : forall l, (mkProd_pred l)*(mkProd' l) = mkProd l. -Proof with mauto. - induction l;simpl;intros ... +Proof. + induction l;simpl;intros; mauto. generalize (pos_eq_1_spec (snd a)); destruct (snd a ?= 1)%P;intros. - rewrite H... + rewrite H; mauto. replace (mkProd_pred l * (fst a * mkProd' l)) with (fst a *(mkProd_pred l * mkProd' l));try ring. - rewrite IHl... + rewrite IHl; mauto. rewrite Zmult_assoc. rewrite times_Zmult. rewrite (Zmult_comm (pow (fst a) (Ppred (snd a)) * mkProd_pred l)). rewrite Zmult_assoc. rewrite pow_Zpower. rewrite <-Ppred_Zminus;trivial. rewrite <- Zpower_Zsucc; try omega. replace (Zsucc (snd a - 1)) with ((snd a - 1)+1). - replace ((snd a - 1)+1) with (Zpos (snd a)) ... - rewrite <- IHl;repeat rewrite Zmult_assoc ... + replace ((snd a - 1)+1) with (Zpos (snd a)); mauto. + rewrite <- IHl;repeat rewrite Zmult_assoc; mauto. destruct (snd a - 1);trivial. assert (1 < snd a); auto with zarith. Qed. -Hint Rewrite mkProd_pred_mkProd : zmisc. +Hint Rewrite mkProd_pred_mkProd : zmisc. Lemma lt_Zmod : forall p n, 0 <= p < n -> p mod n = p. -Proof with mauto. +Proof. intros a b H. assert ( 0 <= a mod b < b). - apply Z_mod_lt... - destruct (mod_unique b (a/b) (a mod b) 0 a H0 H)... - rewrite <- Z_div_mod_eq... + apply Z_mod_lt; mauto. + destruct (mod_unique b (a/b) (a mod b) 0 a H0 H); mauto. + rewrite <- Z_div_mod_eq; mauto. Qed. -Opaque Zminus. Lemma Npred_mod_spec : forall p n, Z_of_N p < Zpos n -> 1 < Zpos n -> Z_of_N (Npred_mod p n) = (p - 1) mod n. -Proof with mauto. +Proof. destruct p;intros;simpl. - rewrite <- Ppred_Zminus... - change (-1) with (0 -1). rewrite <- (Z_mod_same n) ... - pattern 1 at 2;rewrite <- (lt_Zmod 1 n) ... - symmetry;apply lt_Zmod. -Transparent Zminus. - omega. + rewrite <- Ppred_Zminus; auto. + apply Zmod_unique with (q := -1); mauto. assert (H1 := pos_eq_1_spec p);destruct (p?=1)%P. - rewrite H1 ... - unfold Z_of_N;rewrite <- Ppred_Zminus... - simpl in H;symmetry; apply (lt_Zmod (p-1) n)... + rewrite H1; mauto. + unfold Z_of_N;rewrite <- Ppred_Zminus; auto. + simpl in H;symmetry; apply (lt_Zmod (p-1) n). assert (1 < p); auto with zarith. Qed. Hint Rewrite Npred_mod_spec : zmisc. Lemma times_mod_spec : forall x y n, Z_of_N (times_mod x y n) = (x * y) mod n. -Proof with mauto. - intros; destruct x ... - destruct y;simpl ... +Proof. + intros; destruct x; mauto. + destruct y;simpl; mauto. Qed. Hint Rewrite times_mod_spec : zmisc. @@ -453,10 +446,10 @@ Lemma snd_all_pow_mod : forall n l (prod a :N), a mod (Zpos n) = a -> Z_of_N (snd (all_pow_mod prod a l n)) = (a^(mkProd' l)) mod n. -Proof with mauto. - induction l;simpl;intros... - destruct a as (q,p);simpl. - rewrite IHl... +Proof. + induction l; simpl all_pow_mod; simpl mkProd';intros; mauto. + destruct a as (q,p). + rewrite IHl; mauto. Qed. Lemma fold_aux : forall a N (n:positive) l prod, @@ -466,8 +459,8 @@ Lemma fold_aux : forall a N (n:positive) l prod, fold_left (fun (r : Z) (k : positive * positive) => r * (a^(N / fst k) - 1)) l prod mod n. -Proof with mauto. - induction l;simpl;intros ... +Proof. + induction l;simpl;intros; mauto. Qed. Lemma fst_all_pow_mod : @@ -479,12 +472,12 @@ Lemma fst_all_pow_mod : (fold_left (fun r (k:positive*positive) => (r * (a ^ (R* mkProd' l / (fst k)) - 1))) l prod) mod n. -Proof with mauto. - induction l;simpl;intros... +Proof. + induction l;simpl;intros; mauto. destruct a0 as (q,p);simpl. assert (Z_of_N A = A mod n). - rewrite H1 ... - rewrite (IHl (R * q)%positive)... + rewrite H1; mauto. + rewrite (IHl (R * q)%positive); mauto; mauto. pattern (q * mkProd' l) at 2;rewrite (Zmult_comm q). repeat rewrite Zmult_assoc. rewrite Z_div_mult;auto with zmisc zarith. @@ -495,12 +488,11 @@ Proof with mauto. repeat rewrite (Zmult_mod prod);auto with zmisc. rewrite Zminus_mod;auto with zmisc. rewrite (Zminus_mod ((a ^ R) ^ mkProd' l));auto with zmisc. - rewrite (Zpower_mod (a^R));auto with zmisc. rewrite H1... - rewrite H3... - rewrite H1 ... + rewrite (Zpower_mod (a^R));auto with zmisc. rewrite H1; mauto. + rewrite H3; mauto. + rewrite H1; mauto. Qed. - Lemma is_odd_Zodd : forall p, is_odd p = true -> Zodd p. Proof. destruct p;intros;simpl;trivial;discriminate. @@ -548,11 +540,11 @@ Ltac spec_dec := repeat match goal with | [H:(?x ?= ?y)%P = _ |- _] => generalize (is_eq_spec x y); - rewrite H;clear H;simpl; autorewrite with zmisc; + rewrite H;clear H; autorewrite with zmisc; intro | [H:(?x ?< ?y)%P = _ |- _] => generalize (is_lt_spec x y); - rewrite H; clear H;simpl; autorewrite with zmisc; + rewrite H; clear H; autorewrite with zmisc; intro end. @@ -576,7 +568,7 @@ Proof. assert (Zpos (xO (xO (xO s))) = 8 * s). repeat rewrite Zpos_xO_add;ring. generalizeclear H1; rewrite H2;mauto;intros. apply (not_square sqrt). - rewrite H1;auto. + simpl Z.of_N; rewrite H1;auto. intros (y,Heq). generalize H1 Heq;mauto. unfold Z_of_N. @@ -587,32 +579,32 @@ Proof. destruct y;discriminate Heq2. Qed. -Opaque Zplus Pplus. Lemma in_mkProd_prime_div_in : forall p:positive, prime p -> forall (l:dec_prime), (forall k, In k l -> prime (fst k)) -> Zdivide p (mkProd l) -> exists n,In (p, n) l. -Proof with mauto. - induction l;simpl ... +Proof. + induction l;simpl mkProd; simpl In; mauto. intros _ H1; absurd (p <= 1). apply Zlt_not_le; apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith. apply Zdivide_le; auto with zarith. - intros; case prime_mult with (2 := H1); auto with zarith; intros H2. + intros. + case prime_mult with (2 := H1); auto with zarith; intros H2. exists (snd a);left. destruct a;simpl in *. assert (Zpos p = Zpos p0). - rewrite (prime_div_Zpower_prime p1 p p0)... + rewrite (prime_div_Zpower_prime p1 p p0); mauto. apply (H0 (p0,p1));auto. - inversion H3... - destruct IHl as (n,H3)... - exists n... + inversion H3; auto. + destruct IHl as (n,H3); mauto. + exists n; auto. Qed. Lemma gcd_Zis_gcd : forall a b:positive, (Zis_gcd b a (gcd b a)%P). -Proof with mauto. +Proof. intros a;assert (Hacc := Zwf_pos a);induction Hacc;rename x into a;intros. - generalize (div_eucl_spec b a)... + generalize (div_eucl_spec b a); mauto. rewrite <- (Pmod_div_eucl b a). CaseEq (b mod a)%P;[intros Heq|intros r Heq]; intros (H1,H2). simpl in H1;rewrite Zplus_0_r in H1. @@ -629,53 +621,57 @@ Lemma test_pock_correct : forall N a dec sqrt, (forall k, In k dec -> prime (Zpos (fst k))) -> test_pock N a dec sqrt = true -> prime N. -Proof with mauto. +Proof. unfold test_pock;intros. elimif. generalize (div_eucl_spec (Ppred N) (mkProd dec)); - destruct ((Ppred N) / (mkProd dec))%P as (R1,n);simpl;mauto;intros (H2,H3). + destruct ((Ppred N) / (mkProd dec))%P as (R1,n); mauto;intros (H2,H3). destruct R1 as [|R1];try discriminate H0. destruct n;try discriminate H0. elimif. generalize (div_eucl_spec R1 (xO (mkProd dec))); - destruct ((R1 / xO (mkProd dec))%P) as (s,r');simpl;mauto;intros (H7,H8). + destruct ((R1 / xO (mkProd dec))%P) as (s,r'); mauto;intros (H7,H8). destruct r' as [|r];try discriminate H0. generalize (fst_all_pow_mod N a dec (R1*mkProd_pred dec) 1 (pow_mod_pred (pow_mod a R1 N) dec N)). generalize (snd_all_pow_mod N dec 1 (pow_mod_pred (pow_mod a R1 N) dec N)). destruct (all_pow_mod 1 (pow_mod_pred (pow_mod a R1 N) dec N) dec N) as - (prod,aNm1);simpl... + (prod,aNm1); mauto; simpl Z_of_N. destruct prod as [|prod];try discriminate H0. destruct aNm1 as [|aNm1];try discriminate H0;elimif. - simpl in H2;rewrite Zplus_0_r in H2. + simpl in H3; simpl in H2. rewrite <- Ppred_Zminus in H2;try omega. rewrite <- Zmult_assoc;rewrite mkProd_pred_mkProd. intros H12;assert (a^(N-1) mod N = 1). pattern 1 at 2;rewrite <- H9;symmetry. - rewrite H2;rewrite H12 ... - rewrite <- Zpower_mult... + simpl Z.of_N in H12. + rewrite H2; rewrite H12; mauto. + rewrite <- Zpower_mult; mauto. clear H12. intros H14. match type of H14 with _ -> _ -> _ -> ?X => assert (H12:X); try apply H14; clear H14 - end... - rewrite Zmod_small... + end; mauto. + rewrite Zmod_small; mauto. assert (1 < mkProd dec). assert (H14 := Zlt_0_pos (mkProd dec)). - assert (1 <= mkProd dec)... - destruct (Zle_lt_or_eq _ _ H15)... + assert (1 <= mkProd dec); mauto. + destruct (Zle_lt_or_eq _ _ H15); mauto. inversion H16. rewrite <- H18 in H5;discriminate H5. simpl in H8. assert (Z_of_N s = R1 / (2 * mkProd dec) /\ Zpos r = R1 mod (2 * mkProd dec)). apply mod_unique with (2 * mkProd dec);auto with zarith. - apply Z_mod_lt ... - rewrite <- Z_div_mod_eq... rewrite H7. simpl;ring. + revert H8; mauto. + apply Z_mod_lt; mauto. + rewrite <- Z_div_mod_eq; mauto; rewrite H7. + simpl fst; simpl snd; simpl Z_of_N. + ring. destruct H15 as (H15,Heqr). apply PocklingtonExtra with (F1:=mkProd dec) (R1:=R1) (m:=1); auto with zmisc zarith. - rewrite H2;ring. - apply is_even_Zeven... - apply is_odd_Zodd... + rewrite H2; mauto. + apply is_even_Zeven; auto. + apply is_odd_Zodd; auto. intros p; case p; clear p. intros HH; contradict HH. apply not_prime_0. @@ -692,6 +688,7 @@ Proof with mauto. pattern 1 at 3; rewrite <- H10; rewrite <- H12. apply Pmod.gcd_Zis_gcd. destruct (in_mkProd_prime_div_in _ Hprime _ H Hdec) as (q,Hin). + revert H2; mauto; intro H2. rewrite <- H2. match goal with |- context [fold_left ?f _ _] => apply (ListAux.fold_left_invol_in _ _ f (fun k => Zdivide (a ^ ((N - 1) / p) - 1) k)) @@ -700,9 +697,9 @@ Proof with mauto. rewrite <- Heqr. generalizeclear H0; ring_simplify (((mkProd dec + mkProd dec + r + 1) * mkProd dec + r) * mkProd dec + 1) - ((1 * mkProd dec + 1) * (2 * mkProd dec * mkProd dec + (r - 1) * mkProd dec + 1))... + ((1 * mkProd dec + 1) * (2 * mkProd dec * mkProd dec + (r - 1) * mkProd dec + 1)); mauto. rewrite <- H15;rewrite <- Heqr. - apply check_s_r_correct with sqrt ... + apply check_s_r_correct with sqrt; mauto. Qed. Lemma is_in_In : diff --git a/coqprime/Coqprime/Root.v b/coqprime/Coqprime/Root.v index 4e74a4d2f..2f65790d6 100644 --- a/coqprime/Coqprime/Root.v +++ b/coqprime/Coqprime/Root.v @@ -11,11 +11,11 @@ Proof that a polynomial has at most n roots ************************************************************************) -Require Import Coq.ZArith.ZArith. -Require Import Coq.Lists.List. -Require Import Coqprime.UList. -Require Import Coqprime.Tactic. -Require Import Coqprime.Permutation. +Require Import ZArith. +Require Import List. +Require Import UList. +Require Import Tactic. +Require Import Permutation. Open Scope Z_scope. @@ -33,8 +33,8 @@ Let pol := list A. Definition toA z := match z with Z0 => zero -| Zpos p => iter_pos p _ (plus one) zero -| Zneg p => op (iter_pos p _ (plus one) zero) +| Zpos p => iter_pos _ (plus one) zero p +| Zneg p => op (iter_pos _ (plus one) zero p) end. Fixpoint eval (p: pol) (x: A) {struct p} : A := diff --git a/coqprime/Coqprime/UList.v b/coqprime/Coqprime/UList.v index 32ca6b2a0..7b9d982ea 100644 --- a/coqprime/Coqprime/UList.v +++ b/coqprime/Coqprime/UList.v @@ -7,33 +7,33 @@ (*************************************************************) (*********************************************************************** - UList.v - - Definition of list with distinct elements - - Definition: ulist + UList.v + + Definition of list with distinct elements + + Definition: ulist ************************************************************************) -Require Import Coq.Lists.List. -Require Import Coq.Arith.Arith. -Require Import Coqprime.Permutation. -Require Import Coq.Lists.ListSet. - +Require Import List. +Require Import Arith. +Require Import Permutation. +Require Import ListSet. + Section UniqueList. Variable A : Set. Variable eqA_dec : forall (a b : A), ({ a = b }) + ({ a <> b }). (* A list is unique if there is not twice the same element in the list *) - + Inductive ulist : list A -> Prop := ulist_nil: ulist nil | ulist_cons: forall a l, ~ In a l -> ulist l -> ulist (a :: l) . Hint Constructors ulist . (* Inversion theorem *) - + Theorem ulist_inv: forall a l, ulist (a :: l) -> ulist l. intros a l H; inversion H; auto. Qed. (* The append of two unique list is unique if the list are distinct *) - + Theorem ulist_app: forall l1 l2, ulist l1 -> @@ -48,16 +48,18 @@ apply ulist_inv with ( 1 := H0 ); auto. intros a0 H3 H4; apply (H2 a0); auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv: forall l1 l2 (a : A), ulist (l1 ++ l2) -> In a l1 -> In a l2 -> False. intros l1; elim l1; simpl; auto. -intros a l H l2 a0 H0 [H1|H1] H2; -inversion H0 as [|a1 l0 H3 H4 H5]; clear H0; auto; - subst; eauto using ulist_inv with datatypes. +intros a l H l2 a0 H0 [H1|H1] H2. +inversion H0 as [|a1 l0 H3 H4 H5]; auto. +case H3; rewrite H1; auto with datatypes. +apply (H l2 a0); auto. +apply ulist_inv with ( 1 := H0 ); auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv_l: forall (l1 l2 : list A), ulist (l1 ++ l2) -> ulist l1. intros l1; elim l1; simpl; auto. intros a l H l2 H0. @@ -66,13 +68,13 @@ intros H5; case iH2; auto with datatypes. apply H with l2; auto. Qed. (* Iinversion theorem the appended list *) - + Theorem ulist_app_inv_r: forall (l1 l2 : list A), ulist (l1 ++ l2) -> ulist l2. intros l1; elim l1; simpl; auto. intros a l H l2 H0; inversion H0; auto. Qed. (* Uniqueness is decidable *) - + Definition ulist_dec: forall l, ({ ulist l }) + ({ ~ ulist l }). intros l; elim l; auto. intros a l1 [H|H]; auto. @@ -81,7 +83,7 @@ right; red; intros H1; inversion H1; auto. right; intros H1; case H; apply ulist_inv with ( 1 := H1 ). Defined. (* Uniqueness is compatible with permutation *) - + Theorem ulist_perm: forall (l1 l2 : list A), permutation l1 l2 -> ulist l1 -> ulist l2. intros l1 l2 H; elim H; clear H l1 l2; simpl; auto. @@ -101,7 +103,7 @@ intros H; case iH1; simpl; auto. inversion_clear H0 as [|ia il iH1 iH2]; auto. inversion iH2; auto. Qed. - + Theorem ulist_def: forall l a, In a l -> ulist l -> ~ (exists l1 , permutation l (a :: (a :: l1)) ). @@ -110,7 +112,7 @@ absurd (ulist (a :: (a :: l1))); auto. intros H2; inversion_clear H2; simpl; auto with datatypes. apply ulist_perm with ( 1 := H1 ); auto. Qed. - + Theorem ulist_incl_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> (exists l3 , permutation l2 (l1 ++ l3) ). @@ -132,7 +134,7 @@ intros l4 H4; exists l4. apply permutation_trans with (a :: l3); auto. apply permutation_sym; auto. Qed. - + Theorem ulist_eq_permutation: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> length l1 = length l2 -> permutation l1 l2. @@ -148,7 +150,7 @@ replace l1 with (app l1 l3); auto. apply permutation_sym; auto. rewrite H5; rewrite app_nil_end; auto. Qed. - + Theorem ulist_incl_length: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> le (length l1) (length l2). @@ -164,8 +166,8 @@ intros l1 l2 H1 H2 H3 H4. apply ulist_eq_permutation; auto. apply le_antisym; apply ulist_incl_length; auto. Qed. - - + + Theorem ulist_incl_length_strict: forall (l1 l2 : list A), ulist l1 -> incl l1 l2 -> ~ incl l2 l1 -> lt (length l1) (length l2). @@ -178,14 +180,14 @@ intros H2; case Hi0; auto. intros a HH; apply permutation_in with ( 1 := H2 ); auto. intros a l Hl0; (rewrite plus_comm; simpl; rewrite plus_comm; auto with arith). Qed. - + Theorem in_inv_dec: forall (a b : A) l, In a (cons b l) -> a = b \/ ~ a = b /\ In a l. intros a b l H; case (eqA_dec a b); auto; intros H1. right; split; auto; inversion H; auto. case H1; auto. Qed. - + Theorem in_ex_app_first: forall (a : A) (l : list A), In a l -> @@ -201,7 +203,7 @@ case H; auto; intros l1 [l2 [Hl2 Hl3]]; exists (a1 :: l1); exists l2; simpl; subst; auto. intros H4; case H4; auto. Qed. - + Theorem ulist_inv_ulist: forall (l : list A), ~ ulist l -> @@ -237,7 +239,7 @@ replace (l1 ++ (a1 :: (l2 ++ (a1 :: l3)))) with ((l1 ++ (a1 :: l2)) ++ (a1 :: l3)); auto with datatypes. (repeat (rewrite <- ass_app; simpl)); auto. Qed. - + Theorem incl_length_repetition: forall (l1 l2 : list A), incl l1 l2 -> @@ -251,11 +253,11 @@ intros l1 l2 H H0; apply ulist_inv_ulist. intros H1; absurd (le (length l1) (length l2)); auto with arith. apply ulist_incl_length; auto. Qed. - + End UniqueList. Implicit Arguments ulist [A]. Hint Constructors ulist . - + Theorem ulist_map: forall (A B : Set) (f : A -> B) l, (forall x y, (In x l) -> (In y l) -> f x = f y -> x = y) -> ulist l -> ulist (map f l). @@ -268,7 +270,7 @@ case in_map_inv with ( 1 := H1 ); auto with datatypes. intros b1 [Hb1 Hb2]. replace a1 with b1; auto with datatypes. Qed. - + Theorem ulist_list_prod: forall (A : Set) (l1 l2 : list A), ulist l1 -> ulist l2 -> ulist (list_prod l1 l2). diff --git a/coqprime/Coqprime/ZCAux.v b/coqprime/Coqprime/ZCAux.v index aa47fb655..de03a2fe2 100644 --- a/coqprime/Coqprime/ZCAux.v +++ b/coqprime/Coqprime/ZCAux.v @@ -12,10 +12,10 @@ Auxillary functions & Theorems **********************************************************************) -Require Import Coq.setoid_ring.ArithRing. -Require Export Coq.ZArith.ZArith Coq.ZArith.Zpow_facts. -Require Export Coq.ZArith.Znumtheory. -Require Export Coqprime.Tactic. +Require Import ArithRing. +Require Export ZArith Zpow_facts. +Require Export Znumtheory. +Require Export Tactic. Theorem Zdivide_div_prime_le_square: forall x, 1 < x -> ~prime x -> exists p, prime p /\ (p | x) /\ p * p <= x. intros x Hx; generalize Hx; pattern x; apply Z_lt_induction; auto with zarith. diff --git a/coqprime/Coqprime/ZCmisc.v b/coqprime/Coqprime/ZCmisc.v index e2ec66ba1..c1bdacc63 100644 --- a/coqprime/Coqprime/ZCmisc.v +++ b/coqprime/Coqprime/ZCmisc.v @@ -6,7 +6,7 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export Coq.ZArith.ZArith. +Require Export ZArith. Open Local Scope Z_scope. Coercion Zpos : positive >-> Z. diff --git a/coqprime/Coqprime/ZProgression.v b/coqprime/Coqprime/ZProgression.v index 4cf30d692..51ce91cdc 100644 --- a/coqprime/Coqprime/ZProgression.v +++ b/coqprime/Coqprime/ZProgression.v @@ -6,9 +6,9 @@ (* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) (*************************************************************) -Require Export Coqprime.Iterator. -Require Import Coq.ZArith.ZArith. -Require Export Coqprime.UList. +Require Export Iterator. +Require Import ZArith. +Require Export UList. Open Scope Z_scope. Theorem next_n_Z: forall n m, next_n Zsucc n m = n + Z_of_nat m. diff --git a/coqprime/Coqprime/ZSum.v b/coqprime/Coqprime/ZSum.v index 907720f7c..3a7f14065 100644 --- a/coqprime/Coqprime/ZSum.v +++ b/coqprime/Coqprime/ZSum.v @@ -9,12 +9,12 @@ (*********************************************************************** Summation.v from Z to Z *********************************************************************) -Require Import Coq.Arith.Arith. -Require Import Coq.setoid_ring.ArithRing. -Require Import Coqprime.ListAux. -Require Import Coq.ZArith.ZArith. -Require Import Coqprime.Iterator. -Require Import Coqprime.ZProgression. +Require Import Arith. +Require Import ArithRing. +Require Import ListAux. +Require Import ZArith. +Require Import Iterator. +Require Import ZProgression. Open Scope Z_scope. diff --git a/coqprime/Coqprime/Zp.v b/coqprime/Coqprime/Zp.v index 2f7d28d69..1e5295191 100644 --- a/coqprime/Coqprime/Zp.v +++ b/coqprime/Coqprime/Zp.v @@ -14,16 +14,16 @@ Definition: ZpGroup **********************************************************************) -Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.ZArith.Zpow_facts. -Require Import Coqprime.Tactic. -Require Import Coq.Arith.Wf_nat. -Require Import Coqprime.UList. -Require Import Coqprime.FGroup. -Require Import Coqprime.EGroup. -Require Import Coqprime.IGroup. -Require Import Coqprime.Cyclic. -Require Import Coqprime.Euler. -Require Import Coqprime.ZProgression. +Require Import ZArith Znumtheory Zpow_facts. +Require Import Tactic. +Require Import Wf_nat. +Require Import UList. +Require Import FGroup. +Require Import EGroup. +Require Import IGroup. +Require Import Cyclic. +Require Import Euler. +Require Import ZProgression. Open Scope Z_scope. diff --git a/coqprime/Makefile b/coqprime/Makefile index 8fa838a1e..c8e44a658 100644 --- a/coqprime/Makefile +++ b/coqprime/Makefile @@ -2,7 +2,7 @@ ## v # The Coq Proof Assistant ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.4pl6 ## +## // # Makefile automagically generated by coq_makefile V8.5pl1 ## ############################################################################# # WARNING @@ -19,9 +19,10 @@ .DEFAULT_GOAL := all -# # This Makefile may take arguments passed as environment variables: # COQBIN to specify the directory where Coq binaries resides; +# TIMECMD set a command to log .v compilation time; +# TIMED if non empty, use the default time command as TIMECMD; # ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; # DSTROOT to specify a prefix to install path. @@ -33,14 +34,25 @@ endef includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) $(call includecmdwithout@,$(COQBIN)coqtop -config) +TIMED= +TIMECMD= +STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) + +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1)))) + ########################## # # # Libraries definitions. # # # ########################## -COQLIBS?= -R Coqprime Coqprime -COQDOCLIBS?=-R Coqprime Coqprime +COQLIBS?=\ + -R "Coqprime" Coqprime +COQDOCLIBS?=\ + -R "Coqprime" Coqprime ########################## # # @@ -54,10 +66,11 @@ COQDEP?="$(COQBIN)coqdep" -c COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) COQCHKFLAGS?=-silent -o COQDOCFLAGS?=-interpolate -utf8 -COQC?="$(COQBIN)coqc" +COQC?=$(TIMER) "$(COQBIN)coqc" GALLINA?="$(COQBIN)gallina" COQDOC?="$(COQBIN)coqdoc" COQCHK?="$(COQBIN)coqchk" +COQMKTOP?="$(COQBIN)coqmktop" ################## # # @@ -72,6 +85,7 @@ COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq else COQLIBINSTALL="${COQLIB}user-contrib" COQDOCINSTALL="${DOCDIR}user-contrib" +COQTOPINSTALL="${COQLIB}toploop" endif ###################### @@ -80,40 +94,51 @@ endif # # ###################### -VFILES:=Coqprime/Zp.v\ - Coqprime/ZSum.v\ - Coqprime/ZProgression.v\ - Coqprime/ZCmisc.v\ - Coqprime/ZCAux.v\ - Coqprime/UList.v\ - Coqprime/Tactic.v\ - Coqprime/Root.v\ - Coqprime/PocklingtonCertificat.v\ - Coqprime/Pocklington.v\ - Coqprime/Pmod.v\ - Coqprime/Permutation.v\ - Coqprime/PGroup.v\ - Coqprime/NatAux.v\ - Coqprime/LucasLehmer.v\ - Coqprime/ListAux.v\ - Coqprime/Lagrange.v\ - Coqprime/Iterator.v\ - Coqprime/IGroup.v\ - Coqprime/FGroup.v\ - Coqprime/Euler.v\ +VFILES:=Coqprime/Cyclic.v\ Coqprime/EGroup.v\ - Coqprime/Cyclic.v + Coqprime/Euler.v\ + Coqprime/FGroup.v\ + Coqprime/IGroup.v\ + Coqprime/Iterator.v\ + Coqprime/Lagrange.v\ + Coqprime/ListAux.v\ + Coqprime/LucasLehmer.v\ + Coqprime/NatAux.v\ + Coqprime/PGroup.v\ + Coqprime/Permutation.v\ + Coqprime/Pmod.v\ + Coqprime/Pocklington.v\ + Coqprime/PocklingtonCertificat.v\ + Coqprime/Root.v\ + Coqprime/Tactic.v\ + Coqprime/UList.v\ + Coqprime/ZCAux.v\ + Coqprime/ZCmisc.v\ + Coqprime/ZProgression.v\ + Coqprime/ZSum.v\ + Coqprime/Zp.v +ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) +-include $(addsuffix .d,$(VFILES)) +else +ifeq ($(MAKECMDGOALS),) -include $(addsuffix .d,$(VFILES)) +endif +endif + .SECONDARY: $(addsuffix .d,$(VFILES)) -VOFILES:=$(VFILES:.v=.vo) +VO=vo +VOFILES:=$(VFILES:.v=.$(VO)) VOFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(VOFILES))) GLOBFILES:=$(VFILES:.v=.glob) -VIFILES:=$(VFILES:.v=.vi) GFILES:=$(VFILES:.v=.g) HTMLFILES:=$(VFILES:.v=.html) GHTMLFILES:=$(VFILES:.v=.g.html) +OBJFILES=$(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs) +NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) +NATIVEFILES1=$(patsubst Coqprime/%,%,$(filter Coqprime/%,$(NATIVEFILES))) ifeq '$(HASNATDYNLINK)' 'true' HASNATDYNLINK_OR_EMPTY := yes else @@ -128,8 +153,12 @@ endif all: $(VOFILES) -spec: $(VIFILES) +quick: $(VOFILES:.vo=.vio) +vio2vo: + $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +checkproofs: + $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) gallina: $(GFILES) html: $(GLOBFILES) $(VFILES) @@ -160,7 +189,7 @@ beautify: $(VFILES:=.beautified) @echo 'Do not do "make clean" until you are sure that everything went well!' @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: all opt byte archclean clean install userinstall depend html validate +.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo #################### # # @@ -178,7 +207,7 @@ userinstall: +$(MAKE) USERINSTALL=true install install: - cd "Coqprime"; for i in $(VOFILES1); do \ + cd "Coqprime" && for i in $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1); do \ install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i`"; \ install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/Coqprime/$$i; \ done @@ -189,12 +218,46 @@ install-doc: install -m 0644 $$i "$(DSTROOT)"$(COQDOCINSTALL)/Coqprime/$$i;\ done -clean: - rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) +uninstall_me.sh: Makefile + echo '#!/bin/sh' > $@ + printf 'cd "$${DSTROOT}"$(COQLIBINSTALL)/Coqprime && rm -f $(NATIVEFILES1) $(GLOBFILES1) $(VFILES1) $(VOFILES1) && find . -type d -and -empty -delete\ncd "$${DSTROOT}"$(COQLIBINSTALL) && find "Coqprime" -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" + printf 'cd "$${DSTROOT}"$(COQDOCINSTALL)/Coqprime \\\n' >> "$@" + printf '&& rm -f $(shell find "html" -maxdepth 1 -and -type f -print)\n' >> "$@" + printf 'cd "$${DSTROOT}"$(COQDOCINSTALL) && find Coqprime/html -maxdepth 0 -and -empty -exec rmdir -p \{\} \;\n' >> "$@" + chmod +x $@ + +uninstall: uninstall_me.sh + sh $< + +.merlin: + @echo 'FLG -rectypes' > .merlin + @echo "B $(COQLIB) kernel" >> .merlin + @echo "B $(COQLIB) lib" >> .merlin + @echo "B $(COQLIB) library" >> .merlin + @echo "B $(COQLIB) parsing" >> .merlin + @echo "B $(COQLIB) pretyping" >> .merlin + @echo "B $(COQLIB) interp" >> .merlin + @echo "B $(COQLIB) printing" >> .merlin + @echo "B $(COQLIB) intf" >> .merlin + @echo "B $(COQLIB) proofs" >> .merlin + @echo "B $(COQLIB) tactics" >> .merlin + @echo "B $(COQLIB) tools" >> .merlin + @echo "B $(COQLIB) toplevel" >> .merlin + @echo "B $(COQLIB) stm" >> .merlin + @echo "B $(COQLIB) grammar" >> .merlin + @echo "B $(COQLIB) config" >> .merlin + +clean:: + rm -f $(OBJFILES) $(OBJFILES:.o=.native) $(NATIVEFILES) + find . -name .coq-native -type d -empty -delete + rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - - rm -rf html mlihtml + - rm -rf html mlihtml uninstall_me.sh -archclean: +cleanall:: clean + rm -f $(patsubst %.v,.%.aux,$(VFILES)) + +archclean:: rm -f *.cmx *.o printenv: @@ -217,31 +280,34 @@ Makefile: _CoqProject # # ################### -%.vo %.glob: %.v +$(VOFILES): %.vo: %.v + $(COQC) $(COQDEBUG) $(COQFLAGS) $* + +$(GLOBFILES): %.glob: %.v $(COQC) $(COQDEBUG) $(COQFLAGS) $* -%.vi: %.v - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* +$(VFILES:.v=.vio): %.vio: %.v + $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $* -%.g: %.v +$(GFILES): %.g: %.v $(GALLINA) $< -%.tex: %.v +$(VFILES:.v=.tex): %.tex: %.v $(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ -%.html: %.v %.glob +$(HTMLFILES): %.html: %.v %.glob $(COQDOC) $(COQDOCFLAGS) -html $< -o $@ -%.g.tex: %.v +$(VFILES:.v=.g.tex): %.g.tex: %.v $(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ -%.g.html: %.v %.glob +$(GHTMLFILES): %.g.html: %.v %.glob $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ -%.v.d: %.v - $(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) +$(addsuffix .d,$(VFILES)): %.v.d: %.v + $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) -%.v.beautified: +$(addsuffix .beautified,$(VFILES)): %.v.beautified: $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $* # WARNING diff --git a/coqprime/README.md b/coqprime/README.md index 8f1b93b12..9c317fb00 100644 --- a/coqprime/README.md +++ b/coqprime/README.md @@ -1,6 +1,6 @@ # Coqprime (LGPL subset) -This is a mirror of the LGPL-licensed and autogenerated files from [Coqprime](http://coqprime.gforge.inria.fr/) for Coq 8.4. It was generated from [coqprime_par.zip](https://gforge.inria.fr/frs/download.php/file/35201/coqprime_par.zip). Due to the removal of files that are missing license headers in the upstream source, `make` no longer completes successfully. However, a large part of the codebase does build and contains theorems useful to us. Fixing the build system would be nice, but is not a priority for us. +This is a mirror of the LGPL-licensed and autogenerated files from [Coqprime](http://coqprime.gforge.inria.fr/) for Coq 8.5. It was generated from [coqprime_8.5b.zip](https://gforge.inria.fr/frs/download.php/file/35520/coqprime_8.5b.zip). Due to the removal of files that are missing license headers in the upstream source, `make` no longer completes successfully. However, a large part of the codebase does build and contains theorems useful to us. Fixing the build system would be nice, but is not a priority for us. ## Usage |