Remove coqprime-8.4

We're using tactics in terms in some places, and so have no hope of
compiling with Coq 8.4.  We no longer pretend to support it.

We can probably also remove some other compatibility things, if we want.

1 files changed, 0 insertions, 261 deletions

diff --git a/coqprime-8.4/Coqprime/Pocklington.v b/coqprime-8.4/Coqprime/Pocklington.v
deleted file mode 100644
index 79e7dc616..000000000
--- a/coqprime-8.4/Coqprime/Pocklington.v
+++ /dev/null
@@ -1,261 +0,0 @@
-
-(*************************************************************)
-(*      This file is distributed under the terms of the      *)
-(*      GNU Lesser General Public License Version 2.1        *)
-(*************************************************************)
-(*    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.
-
-Open Scope Z_scope.
-
-Theorem Pocklington: 
-forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> 
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
-  forall n, prime n -> (n | N) -> n mod F1 = 1.
-intros N F1 R1 HF1 HR1 Neq Rec n Hn H.
-assert (HN: 1 < N).
-assert (0 < N - 1); auto with zarith.
-rewrite Neq; auto with zarith.
-apply Zlt_le_trans with (1* R1); auto with zarith.
-assert (Hn1: 1 < n); auto with zarith.
-apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
-assert (H1: (F1 | n - 1)).
-2: rewrite <- (Zmod_small 1 F1); auto with zarith.
-2: case H1; intros k H1'.
-2: replace n with (1 + (n - 1)); auto with zarith.
-2: rewrite H1'; apply Z_mod_plus; auto with zarith.
-apply Zdivide_Zpower; auto with zarith.
-intros p i Hp Hi HiF1.
-case (Rec p); auto.
-apply Zdivide_trans with (2 := HiF1).
-apply Zpower_divide; auto with zarith.
-intros a (Ha1, (Ha2, Ha3)).
-assert (HNn: a ^ (N - 1) mod n = 1).
-apply Zdivide_mod_minus; auto with zarith.
-apply Zdivide_trans with (1 := H).
-apply Zmod_divide_minus; auto with zarith.
-assert (~(n | a)).
-intros H1; absurd (0 = 1); auto with zarith.
-rewrite <- HNn; auto.
-apply sym_equal; apply Zdivide_mod; auto with zarith.
-apply Zdivide_trans with (1 := H1); apply Zpower_divide; auto with zarith.
-assert (Hr: rel_prime a n).
-apply rel_prime_sym; apply prime_rel_prime; auto.
-assert (Hz: 0 < Zorder a n).
-apply Zorder_power_pos; auto.
-apply Zdivide_trans with (Zorder a n).
-apply prime_divide_Zpower_Zdiv with (N - 1); auto with zarith.
-apply Zorder_div_power; auto with zarith.
-intros H1; absurd (1 < n); auto; apply Zle_not_lt; apply Zdivide_le; auto with zarith.
-rewrite <- Ha3; apply Zdivide_Zgcd; auto with zarith.
-apply Zmod_divide_minus; auto with zarith.
-case H1; intros t Ht; rewrite Ht.
-assert (Ht1: 0 <= t).
-apply Zmult_le_reg_r with (Zorder a n); auto with zarith.
-rewrite Zmult_0_l; rewrite <- Ht.
-apply Zge_le; apply Z_div_ge0; auto with zarith.
-apply Zlt_gt; apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
-rewrite Zmult_comm; rewrite Zpower_mult; auto with zarith.
-rewrite Zpower_mod; auto with zarith.
-rewrite Zorder_power_is_1; auto with zarith.
-rewrite Zpower_1_l; auto with zarith.
-apply Zmod_small; auto with zarith.
-apply Zdivide_trans with (1:= HiF1); rewrite Neq; apply Zdivide_factor_r.
-apply Zorder_div; auto.
-Qed.
-
-Theorem PocklingtonCorollary1: 
-forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> N < F1 * F1 ->
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
-   prime N.
-intros N F1 R1 H H1 H2 H3 H4; case (prime_dec N); intros H5; auto.
-assert (HN: 1 < N).
-assert (0 < N - 1); auto with zarith.
-rewrite H2; auto with zarith.
-apply Zlt_le_trans with (1* R1); auto with zarith.
-case Zdivide_div_prime_le_square with (2:= H5); auto with zarith.
-intros n (Hn, (Hn1, Hn2)).
-assert (Hn3: 0 <= n).
-apply Zle_trans with 2; try apply prime_ge_2; auto with zarith.
-absurd (n = 1).
-intros H6; contradict Hn; subst; apply not_prime_1.
-rewrite <- (Zmod_small n F1); try split; auto.
-apply Pocklington with (R1 := R1) (4 := H4); auto.
-apply Zlt_square_mult_inv; auto with zarith.
-Qed.
-
-Theorem PocklingtonCorollary2: 
-forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> 
-   (forall p,  prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
-  forall n, 0 <= n -> (n | N) -> n mod F1 = 1.
-intros N F1 R1 H1 H2 H3 H4 n H5; pattern n; apply prime_induction; auto.
-assert (HN: 1 < N).
-assert (0 < N - 1); auto with zarith.
-rewrite H3; auto with zarith.
-apply Zlt_le_trans with (1* R1); auto with zarith.
-intros (u, Hu); contradict HN; subst; rewrite Zmult_0_r; auto with zarith.
-intro H6; rewrite Zmod_small; auto with zarith.
-intros p q Hp Hp1 Hp2; rewrite Zmult_mod; auto with zarith.
-rewrite Pocklington with (n := p) (R1 := R1) (4 := H4); auto.
-rewrite Hp1.
-rewrite Zmult_1_r; rewrite Zmod_small; auto with zarith.
-apply Zdivide_trans with (2 := Hp2); apply Zdivide_factor_l.
-apply Zdivide_trans with (2 := Hp2); apply Zdivide_factor_r; auto.
-Qed.
-
-Definition isSquare x := exists y, x = y * y.
-
-Theorem PocklingtonExtra: 
-forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 ->
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
-   forall m, 1 <= m ->  (forall l, 1 <= l < m -> ~((l * F1 + 1) | N)) ->
-    let s := (R1 / (2 * F1)) in
-    let r := (R1 mod (2 * F1)) in
-      N < (m * F1 + 1) * (2 * F1 * F1 + (r - m) * F1 + 1) ->
-      (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N.
-intros N F1 R1 H1 H2 H3 OF1 ER1 H4 m H5 H6 s r H7 H8.
-case (prime_dec N); auto; intros H9.
-assert (HN: 1 < N).
-assert (0 < N - 1); auto with zarith.
-rewrite H3; auto with zarith.
-apply Zlt_le_trans with (1* R1); auto with zarith.
-case  Zdivide_div_prime_le_square with N; auto.
-intros X (Hx1, (Hx2, Hx3)).
-assert (Hx0: 1 < X).
-apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
-pose (c := (X /  F1)).
-assert(Hc1: 0 <= c); auto with zarith.
-apply Zge_le; unfold c; apply Z_div_ge0; auto with zarith.
-assert (Hc2: X = c * F1 + 1).
-rewrite (Z_div_mod_eq X F1); auto with zarith.
-eq_tac; auto.
-rewrite (Zmult_comm F1); auto.
-apply PocklingtonCorollary2 with (R1 := R1) (4 := H4); auto with zarith.
-case Zle_lt_or_eq with (1 := Hc1); clear Hc1; intros Hc1.
-2: contradict Hx0; rewrite Hc2; try rewrite <- Hc1; auto with zarith.
-case (Zle_or_lt m c); intros Hc3.
-2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5; auto with zarith.
-2: case (H6 c); auto with zarith; rewrite <- Hc2; auto.
-2: contradict Hc3; rewrite <- H5; auto with zarith.
-pose (d := ((N / X) /  F1)).
-assert(Hd0: 0 <= N / X); try apply Z_div_pos; auto with zarith.
-(*
-apply Zge_le; unfold d; repeat apply Z_div_ge0; auto with zarith.
-*)
-assert(Hd1: 0 <= d); auto with zarith.
-apply Zge_le; unfold d; repeat apply Z_div_ge0; auto with zarith.
-assert (Hd2: N / X =  d * F1 + 1).
-rewrite (Z_div_mod_eq (N / X) F1); auto with zarith.
-eq_tac; auto.
-rewrite (Zmult_comm F1); auto.
-apply PocklingtonCorollary2 with (R1 := R1) (4 := H4); auto with zarith.
-exists X; auto with zarith.
-apply Zdivide_Zdiv_eq; auto with zarith.
-case Zle_lt_or_eq with (1  := Hd0); clear Hd0; intros Hd0.
-2: contradict HN; rewrite (Zdivide_Zdiv_eq X N); auto with zarith.
-2: rewrite <- Hd0; auto with zarith.
-case (Zle_lt_or_eq 1 (N / X)); auto with zarith; clear Hd0; intros Hd0.
-2: contradict H9; rewrite (Zdivide_Zdiv_eq X N); auto with zarith.
-2: rewrite <- Hd0; rewrite Zmult_1_r; auto with zarith.
-case Zle_lt_or_eq with (1 := Hd1); clear Hd1; intros Hd1.
-2: contradict Hd0; rewrite Hd2; try rewrite <- Hd1; auto with zarith.
-case (Zle_or_lt m d); intros Hd3.
-2: case Zle_lt_or_eq with (1 := H5); clear H5; intros H5; auto with zarith.
-2: case (H6 d); auto with zarith; rewrite <- Hd2; auto.
-2: exists X; auto with zarith.
-2: apply Zdivide_Zdiv_eq; auto with zarith.
-2: contradict Hd3; rewrite <- H5; auto with zarith.
-assert (L5: N = (c * F1 + 1) * (d * F1 + 1)).
-rewrite <- Hc2; rewrite <- Hd2; apply Zdivide_Zdiv_eq; auto with zarith.
-assert (L6: R1 = c * d * F1 + c + d).
-apply trans_equal with ((N - 1) / F1).
-rewrite H3; rewrite Zmult_comm; apply sym_equal; apply Z_div_mult; auto with zarith.
-rewrite L5.
-match goal with |- (?X / ?Y = ?Z) => replace X with (Z * Y) end; try ring; apply Z_div_mult; auto with zarith.
-assert (L6_1: Zodd (c + d)).
-case (Zeven_odd_dec (c + d)); auto; intros O1.
-contradict ER1; apply Zeven_not_Zodd; rewrite L6; rewrite <- Zplus_assoc; apply Zeven_plus_Zeven; auto.
-apply Zeven_mult_Zeven_r; auto.
-assert (L6_2: Zeven (c * d)).
-case (Zeven_odd_dec c); intros HH1. 
-apply Zeven_mult_Zeven_l; auto.
-case (Zeven_odd_dec d); intros HH2.
-apply Zeven_mult_Zeven_r; auto.
-contradict L6_1; apply Zeven_not_Zodd; apply Zodd_plus_Zodd; auto.
-assert ((c + d) mod (2 * F1) = r).
-rewrite <- Z_mod_plus with (b := Zdiv2 (c * d)); auto with zarith.
-match goal with |- ?X mod _ = _ => replace X with R1 end; auto.
-rewrite L6; pattern (c * d) at 1.
-rewrite Zeven_div2 with (1 := L6_2); ring.
-assert (L9: c + d - r < 2 * F1).
-apply Zplus_lt_reg_r with (r - m).
-apply Zmult_lt_reg_r with (F1); auto with zarith.
-apply Zplus_lt_reg_r with 1.
-match goal with |-  ?X < ?Y =>
-  replace Y with (2 * F1 * F1 + (r - m) * F1 + 1); try ring;
-  replace X with ((((c + d) - m) * F1) + 1); try ring
-end.
-apply Zmult_lt_reg_r with (m * F1 + 1); auto with zarith.
-apply Zlt_trans with (m * F1 + 0); auto with zarith.
-rewrite Zplus_0_r; apply Zmult_lt_O_compat; auto with zarith.
-repeat rewrite (fun x => Zmult_comm x (m * F1 + 1)).
-apply Zle_lt_trans with (2 := H7).
-rewrite L5.
-match goal with |-  ?X <= ?Y =>
-  replace X with ((m * (c + d) - m * m ) * F1 * F1 + (c + d) * F1 + 1); try ring;
-  replace Y with ((c * d) * F1 * F1 + (c + d) * F1 + 1); try ring
-end.
-repeat apply Zplus_le_compat_r.
-repeat apply Zmult_le_compat_r; auto with zarith.
-assert (tmp: forall p q, 0 <= p - q  -> q <= p); auto with zarith; try apply tmp.
-match goal with |-  _ <= ?X =>
-  replace X with ((c - m) * (d - m)); try ring; auto with zarith
-end.
-assert (L10: c + d = r).
-apply Zmod_closeby_eq with (2 * F1); auto with zarith.
-unfold r; apply Z_mod_lt; auto with zarith.
-assert (L11: 2 * s  = c * d).
-apply Zmult_reg_r with F1; auto with zarith.
-apply trans_equal with (R1 - (c + d)).
-rewrite L10; rewrite (Z_div_mod_eq R1 (2 * F1)); auto with zarith.
-unfold s, r; ring.
-rewrite L6; ring.
-case H8; intro H10.
-absurd (0 < c * d); auto with zarith.
-apply Zmult_lt_O_compat; auto with zarith.
-case H10; exists (c - d); auto with zarith.
-rewrite <- L10.
-replace (8 * s) with (4 * (2 * s)); auto with zarith; try rewrite L11; ring.
-Qed.
-
-Theorem PocklingtonExtraCorollary: 
-forall N F1 R1, 1 < F1 -> 0 < R1 -> N - 1 = F1 * R1 -> Zeven F1 -> Zodd R1 ->
-   (forall p, prime p -> (p | F1) -> exists a,  1 < a /\ a^(N - 1) mod N = 1 /\ Zgcd (a ^ ((N - 1)/ p) - 1) N = 1) -> 
-    let s := (R1 / (2 * F1)) in
-    let r := (R1 mod (2 * F1)) in
-      N < 2 * F1 * F1 * F1 ->  (s = 0 \/ ~ isSquare (r * r - 8 * s)) -> prime N.
-intros N F1 R1 H1 H2 H3 OF1 ER1 H4 s r H5 H6.
-apply PocklingtonExtra with (6 := H4) (R1 := R1) (m := 1); auto with zarith.
-apply Zlt_le_trans with (1 := H5).
-match goal with |-  ?X <= ?K * ((?Y + ?Z) + ?T) =>
-    rewrite <- (Zplus_0_l X);
-   replace (K * ((Y + Z) + T)) with ((F1 * (Z + T) +  Y + Z + T) + X);[idtac | ring]
-end.
-apply Zplus_le_compat_r.
-case (Zle_lt_or_eq 0 r); unfold r; auto with zarith.
-case (Z_mod_lt R1 (2 * F1)); auto with zarith.
-intros HH; repeat ((rewrite <- (Zplus_0_r 0); apply Zplus_le_compat)); auto with zarith.
-intros HH; contradict ER1; apply Zeven_not_Zodd.
-rewrite (Z_div_mod_eq R1 (2 * F1)); auto with zarith.
-rewrite <- HH; rewrite Zplus_0_r.
-rewrite <- Zmult_assoc; apply Zeven_2p.
-Qed.