Commit a77514ba authored by Benoit Viguier's avatar Benoit Viguier
Browse files

start working on coq8.7 compatibility

parent 9a2ad8c6
......@@ -110,6 +110,7 @@ Doc
*.vio
*.crashcoqide
*.cache
Makefile.conf
### C ###
# Object files
......@@ -235,4 +236,4 @@ tramp
slides/config.php
slides/send.php
doc
\ No newline at end of file
doc
This diff is collapsed.
......@@ -9,7 +9,9 @@
Set Implicit Arguments.
Require Import ZArith Znumtheory Zpow_facts.
Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
Require Import CyclicAxioms.
Require Import Bignums.CyclicDouble.DoubleCyclic.
Require Import Bignums.BigN.BigN Cyclic31 Int31.
Require Import ZCAux.
Require Import W.
Require Import Mod_op.
......
......@@ -8,8 +8,16 @@
Set Implicit Arguments.
Require Import DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv.
Require Import CyclicAxioms DoubleCyclic BigN Cyclic31.
Require Import Bignums.CyclicDouble.DoubleBase.
Require Import Bignums.CyclicDouble.DoubleSub.
Require Import Bignums.CyclicDouble.DoubleMul.
Require Import Bignums.CyclicDouble.DoubleSqrt.
Require Import Bignums.CyclicDouble.DoubleLift.
Require Import Bignums.CyclicDouble.DoubleDivn1.
Require Import Bignums.CyclicDouble.DoubleDiv.
Require Import CyclicAxioms.
Require Import Bignums.CyclicDouble.DoubleCyclic.
Require Import Bignums.BigN.BigN Cyclic31.
Require Import ZArith ZCAux.
Import CyclicAxioms DoubleType DoubleBase.
......
......@@ -8,7 +8,9 @@
Require Import ZArith Znumtheory Zpow_facts.
Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
Require Import CyclicAxioms.
Require Import Bignums.CyclicDouble.DoubleCyclic.
Require Import Bignums.BigN.BigN Cyclic31 Int31.
Require Import W.
Require Import Mod_op.
Require Import ZEll.
......
......@@ -13,7 +13,9 @@ Require Import ZCAux.
Require Import LucasLehmer.
Require Import Pocklington.
Require Import ZArith Znumtheory Zpow_facts.
Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
Require Import CyclicAxioms.
Require Import Bignums.CyclicDouble.DoubleCyclic.
Require Import Bignums.BigN.BigN Cyclic31 Int31.
Require Import Pmod.
Require Import Mod_op.
Require Import W.
......
......@@ -7,7 +7,7 @@
(*************************************************************)
Set Implicit Arguments.
Require Import CyclicAxioms DoubleCyclic BigN Cyclic31 Int31.
Require Import CyclicAxioms Bignums.CyclicDouble.DoubleCyclic Bignums.BigN.BigN Cyclic31 Int31.
Require Import ZArith ZCAux.
(* ** Type of words ** *)
......
......@@ -48,6 +48,7 @@ Eval vm_compute in
positive_to_num 2147483648.
*)
Let wB := (2^ Z_of_nat size)%Z.
Definition mphi (n : number) :=
fold_right (fun i r => phi i + wB * r )%Z 0%Z n.
......@@ -171,10 +172,10 @@ case (le_lt_or_eq n 30); auto with zarith; intros HH3.
rewrite Zmod_small; nrom; auto with zarith.
split; auto with zarith.
change wB with (Zpower_nat 2 31); apply Zpower_nat_lt_compat; auto with zarith.
rewrite HH3, Z_mod_same; auto with zarith.
rewrite HH3, Z_mod_same; auto with zarith ; try reflexivity.
assert (Hij: (forall i j n, phi i = Zpower_nat 2 n -> phi j < phi i ->
phi (i + j) = phi i + phi j)%Z).
intros i j n Hi Hj.
intros i j n Hi Hj.
rewrite spec_add, Zmod_small; auto; nrom.
case (phi_bounded i); case (phi_bounded j); nrom; intros H1j H2j H1i H2i;
split; auto with zarith.
......@@ -184,7 +185,7 @@ intros i j n Hi Hj.
apply Zlt_le_trans with (Zpower_nat 2 (S n)).
rewrite Zpower_nat_S, <-Hi; auto with zarith.
change wB with (Zpower_nat 2 31).
apply Zpower_nat_le_compat; auto with zarith.
apply Zpower_nat_le_compat; auto with zarith.
assert (H: forall p1 i j n, phi i = Zpower_nat 2 n -> (phi j < phi i ->
mphi (positive_aux_to_num p1 i j) = Zpos p1 * phi i + phi j)%Z).
induction p1 as [p1 Hrec| p1 Hrec| ]; simpl positive_aux_to_num; intros i j n Hi Hj.
......@@ -217,6 +218,7 @@ Qed.
Lemma phi_pos n : (0 <= [n])%Z.
Proof.
induction n as [ | a n Hrec]; nrom; auto with zarith.
unfold wB.
case (phi_bounded a); intros Ha1 Ha2; auto with zarith.
Qed.
......
opam-version: "1.1"
opam-version: "1.2"
name: "coq-coqprime"
version: "dev"
maintainer: ""
homepage: "http://coqprime.gforge.inria.fr/"
bug-reports: "http://coqprime.gforge.inria.fr/"
license: "MIT"
License: "MIT"
build: [
["./configure.sh"]
[make "-j%{jobs}%"]
......@@ -11,7 +13,5 @@ build: [
remove: ["rm" "-R" "%{lib}%/coq/user-contrib/Coqprime"]
depends: [
"coq" {>= "8.5~"}
"coq-bignums"
]
Certifying of prime numbers im Coq
https://gforge.inria.fr/frs/download.php/file/35202/coqprime_8.5.zip
......@@ -53,7 +53,7 @@ COQTOP=$(COQBIN)coqtop
COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
COQDOC=$(COQBIN)coqdoc -d doc -g -utf8 $(DEPFLAGS)
COQVERSION= 8.6.1
COQVERSION= 8.6.1 or-else 8.7.0
COQV=$(shell $(COQC) -v)
ifeq ("$(filter $(COQVERSION),$(COQV))","")
$(error FAILURE: You need Coq $(COQVERSION) but you have this version: $(COQV))
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment