aboutsummaryrefslogtreecommitdiff
path: root/coqprime
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-06-22 11:47:16 -0700
committerGravatar Jason Gross <jagro@google.com>2016-06-22 11:47:16 -0700
commitaccc9fa1f5689d1bf57d3024c4ad293fd10f3617 (patch)
tree2a5b8e4ffa0ce872ed1fec10c91fcfdf0dfe2239 /coqprime
parent67fc064ef8606a0efa110c5346261564fc861f11 (diff)
Make Coq 8.5 the default target for Fiat-Crypto
Instructions for 8.4 build in the README
Diffstat (limited to 'coqprime')
-rw-r--r--coqprime/Coqprime/Cyclic.v14
-rw-r--r--coqprime/Coqprime/EGroup.v36
-rw-r--r--coqprime/Coqprime/Euler.v8
-rw-r--r--coqprime/Coqprime/FGroup.v8
-rw-r--r--coqprime/Coqprime/IGroup.v12
-rw-r--r--coqprime/Coqprime/Iterator.v6
-rw-r--r--coqprime/Coqprime/Lagrange.v12
-rw-r--r--coqprime/Coqprime/ListAux.v10
-rw-r--r--coqprime/Coqprime/LucasLehmer.v36
-rw-r--r--coqprime/Coqprime/Makefile.bak203
-rw-r--r--coqprime/Coqprime/NatAux.v2
-rw-r--r--coqprime/Coqprime/Note.pdfbin134038 -> 0 bytes
-rw-r--r--coqprime/Coqprime/PGroup.v18
-rw-r--r--coqprime/Coqprime/Permutation.v4
-rw-r--r--coqprime/Coqprime/Pmod.v10
-rw-r--r--coqprime/Coqprime/Pocklington.v16
-rw-r--r--coqprime/Coqprime/PocklingtonCertificat.v219
-rw-r--r--coqprime/Coqprime/Root.v14
-rw-r--r--coqprime/Coqprime/UList.v70
-rw-r--r--coqprime/Coqprime/ZCAux.v8
-rw-r--r--coqprime/Coqprime/ZCmisc.v2
-rw-r--r--coqprime/Coqprime/ZProgression.v6
-rw-r--r--coqprime/Coqprime/ZSum.v12
-rw-r--r--coqprime/Coqprime/Zp.v20
-rw-r--r--coqprime/Makefile160
-rw-r--r--coqprime/README.md2
26 files changed, 385 insertions, 523 deletions
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
--- a/coqprime/Coqprime/Note.pdf
+++ /dev/null
Binary files 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 ##
## <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