From accc9fa1f5689d1bf57d3024c4ad293fd10f3617 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Jun 2016 11:47:16 -0700 Subject: Make Coq 8.5 the default target for Fiat-Crypto Instructions for 8.4 build in the README --- coqprime/Coqprime/Cyclic.v | 14 +- coqprime/Coqprime/EGroup.v | 36 ++--- coqprime/Coqprime/Euler.v | 8 +- coqprime/Coqprime/FGroup.v | 8 +- coqprime/Coqprime/IGroup.v | 12 +- coqprime/Coqprime/Iterator.v | 6 +- coqprime/Coqprime/Lagrange.v | 12 +- coqprime/Coqprime/ListAux.v | 10 +- coqprime/Coqprime/LucasLehmer.v | 36 ++--- coqprime/Coqprime/Makefile.bak | 203 --------------------------- coqprime/Coqprime/NatAux.v | 2 +- coqprime/Coqprime/Note.pdf | Bin 134038 -> 0 bytes coqprime/Coqprime/PGroup.v | 18 +-- coqprime/Coqprime/Permutation.v | 4 +- coqprime/Coqprime/Pmod.v | 10 +- coqprime/Coqprime/Pocklington.v | 16 +-- coqprime/Coqprime/PocklingtonCertificat.v | 219 +++++++++++++++--------------- coqprime/Coqprime/Root.v | 14 +- coqprime/Coqprime/UList.v | 70 +++++----- coqprime/Coqprime/ZCAux.v | 8 +- coqprime/Coqprime/ZCmisc.v | 2 +- coqprime/Coqprime/ZProgression.v | 6 +- coqprime/Coqprime/ZSum.v | 12 +- coqprime/Coqprime/Zp.v | 20 +-- coqprime/Makefile | 160 +++++++++++++++------- coqprime/README.md | 2 +- 26 files changed, 385 insertions(+), 523 deletions(-) delete mode 100644 coqprime/Coqprime/Makefile.bak delete mode 100644 coqprime/Coqprime/Note.pdf (limited to 'coqprime') 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/Makefile.bak b/coqprime/Coqprime/Makefile.bak deleted file mode 100644 index fe49dbf29..000000000 --- a/coqprime/Coqprime/Makefile.bak +++ /dev/null @@ -1,203 +0,0 @@ -############################################################################## -## The Calculus of Inductive Constructions ## -## ## -## Projet Coq ## -## ## -## INRIA ENS-CNRS ## -## Rocquencourt Lyon ## -## ## -## Coq V7 ## -## ## -## ## -############################################################################## - -# WARNING -# -# This Makefile has been automagically generated by coq_makefile -# Edit at your own risks ! -# -# END OF WARNING - -# -# This Makefile was generated by the command line : -# coq_makefile -f Make -o Makefile -# - -########################## -# # -# Variables definitions. # -# # -########################## - -CAMLP4LIB=`camlp4 -where` -COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \ - -I $(COQTOP)/library -I $(COQTOP)/parsing \ - -I $(COQTOP)/pretyping -I $(COQTOP)/interp \ - -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \ - -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/correctness \ - -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \ - -I $(COQTOP)/contrib/fourier -I $(COQTOP)/contrib/graphs \ - -I $(COQTOP)/contrib/interface -I $(COQTOP)/contrib/jprover \ - -I $(COQTOP)/contrib/omega -I $(COQTOP)/contrib/romega \ - -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/xml \ - -I $(CAMLP4LIB) -ZFLAGS=$(OCAMLLIBS) $(COQSRC) -OPT= -COQFLAGS=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML) -COQC=$(COQBIN)coqc -GALLINA=gallina -COQDOC=coqdoc -CAMLC=ocamlc -c -CAMLOPTC=ocamlopt -c -CAMLLINK=ocamlc -CAMLOPTLINK=ocamlopt -COQDEP=$(COQBIN)coqdep -c -GRAMMARS=grammar.cma -CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo -PP=-pp "camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl" - -######################### -# # -# Libraries definition. # -# # -######################### - -OCAMLLIBS=-I .\ - -I ../Tactic\ - -I ../N\ - -I ../Z\ - -I ../List -COQLIBS=-I .\ - -I ../Tactic\ - -I ../N\ - -I ../Z\ - -I ../List - -################################### -# # -# Definition of the "all" target. # -# # -################################### - -VFILES=Cyclic.v\ - EGroup.v\ - Euler.v\ - FGroup.v\ - IGroup.v\ - Lagrange.v\ - LucasLehmer.v\ - Pepin.v\ - PGroup.v\ - PocklingtonCertificat.v\ - PocklingtonRefl.v\ - Pocklington.v\ - Proth.v\ - Root.v\ - Zp.v -VOFILES=$(VFILES:.v=.vo) -VIFILES=$(VFILES:.v=.vi) -GFILES=$(VFILES:.v=.g) -HTMLFILES=$(VFILES:.v=.html) -GHTMLFILES=$(VFILES:.v=.g.html) - -all: Cyclic.vo\ - EGroup.vo\ - Euler.vo\ - FGroup.vo\ - IGroup.vo\ - Lagrange.vo\ - LucasLehmer.vo\ - Pepin.vo\ - PGroup.vo\ - PocklingtonCertificat.vo\ - PocklingtonRefl.vo\ - Pocklington.vo\ - Proth.vo\ - Root.vo\ - Zp.vo - -spec: $(VIFILES) - -gallina: $(GFILES) - -html: $(HTMLFILES) - -gallinahtml: $(GHTMLFILES) - -all.ps: $(VFILES) - $(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - -all-gal.ps: $(VFILES) - $(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)` - - - -#################### -# # -# Special targets. # -# # -#################### - -.PHONY: all opt byte archclean clean install depend html - -.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html - -.v.vo: - $(COQC) $(COQDEBUG) $(COQFLAGS) $* - -.v.vi: - $(COQC) -i $(COQDEBUG) $(COQFLAGS) $* - -.v.g: - $(GALLINA) $< - -.v.tex: - $(COQDOC) -latex $< -o $@ - -.v.html: - $(COQDOC) -html $< -o $@ - -.v.g.tex: - $(COQDOC) -latex -g $< -o $@ - -.v.g.html: - $(COQDOC) -html -g $< -o $@ - -byte: - $(MAKE) all "OPT=" - -opt: - $(MAKE) all "OPT=-opt" - -include .depend - -.depend depend: - rm -f .depend - $(COQDEP) -i $(COQLIBS) $(VFILES) *.ml *.mli >.depend - $(COQDEP) $(COQLIBS) -suffix .html $(VFILES) >>.depend - -install: - mkdir -p `$(COQC) -where`/user-contrib - cp -f $(VOFILES) `$(COQC) -where`/user-contrib - -Makefile: Make - mv -f Makefile Makefile.bak - $(COQBIN)coq_makefile -f Make -o Makefile - - -clean: - rm -f *.cmo *.cmi *.cmx *.o $(VOFILES) $(VIFILES) $(GFILES) *~ - rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES) - -archclean: - rm -f *.cmx *.o - -html: - -# WARNING -# -# This Makefile has been automagically generated by coq_makefile -# Edit at your own risks ! -# -# END OF WARNING - 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/Note.pdf b/coqprime/Coqprime/Note.pdf deleted file mode 100644 index 239a38772..000000000 Binary files a/coqprime/Coqprime/Note.pdf and /dev/null differ 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 ## ## $@ + 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 -- cgit v1.2.3