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, 411 deletions

diff --git a/coqprime-8.4/Coqprime/Zp.v b/coqprime-8.4/Coqprime/Zp.v
deleted file mode 100644
index 2f7d28d69..000000000
--- a/coqprime-8.4/Coqprime/Zp.v
+++ /dev/null
@@ -1,411 +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      *)
-(*************************************************************)
-
-(**********************************************************************
-    Zp.v                        
-                                                                     
-    Build the group of the inversible element on {1, 2, .., n-1}
-    for the multiplication modulo n
-                                                                 
-    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.
-
-Open Scope Z_scope.
-
-Section Zp.
-
-Variable n: Z.
-
-Hypothesis n_pos: 1 < n.
-
-
-(************************************** 
-  mkZp m creates {m, m - 1, ..., 0}
- **************************************)
-
-Fixpoint mkZp_aux (m: nat): list Z:=
-  Z_of_nat m :: match m with O => nil | (S m1) => mkZp_aux m1 end. 
-
-(************************************** 
-  Some properties of mkZp_aux
- **************************************)
-
-Theorem mkZp_aux_length: forall m, length (mkZp_aux m) = (m + 1)%nat.
-intros m; elim m; simpl; auto.
-Qed.
-
-Theorem mkZp_aux_in: forall m p, 0 <= p <= Z_of_nat m -> In p (mkZp_aux m).
-intros m; elim m.
-simpl; auto with zarith.
-intros n1 Rec p (H1, H2); case Zle_lt_or_eq with (1 := H2); clear H2; intro H2.
-rewrite inj_S in H2.
-simpl; right; apply Rec; split; auto with zarith.
-rewrite H2; simpl; auto.
-Qed.
-
-Theorem in_mkZp_aux: forall m p, In p (mkZp_aux  m) ->  0 <= p <= Z_of_nat m.
-intros m; elim m; clear m.
-simpl; intros p H1; case H1; clear H1; intros H1; subst; auto with zarith.
-intros m1; generalize (inj_S m1); simpl.
-intros H Rec p [H1 | H1].
-rewrite <- H1; rewrite H; auto with zarith.
-rewrite H; case (Rec p); auto with zarith.
-Qed.
-
-Theorem mkZp_aux_ulist: forall m, ulist (mkZp_aux m).
-intros m; elim m; simpl; auto.
-intros m1 H; apply ulist_cons; auto.
-change (~ In (Z_of_nat (S m1)) (mkZp_aux m1)).
-rewrite inj_S; intros H1.
-case in_mkZp_aux with (1 := H1); auto with zarith.
-Qed.
-
-(************************************** 
-  mkZp creates {n - 1, ..., 1, 0}
- **************************************)
-
-Definition mkZp := mkZp_aux (Zabs_nat (n - 1)).
-
-(************************************** 
-  Some properties of mkZp
- **************************************)
-
-Theorem mkZp_length: length mkZp = Zabs_nat n.
-unfold mkZp; rewrite mkZp_aux_length.
-apply inj_eq_rev.
-rewrite inj_plus.
-simpl; repeat rewrite inj_Zabs_nat; auto with zarith.
-repeat rewrite Zabs_eq; auto with zarith.
-Qed.
-
-Theorem mkZp_in: forall p, 0 <= p < n -> In p mkZp.
-intros p (H1, H2); unfold mkZp; apply mkZp_aux_in.
-rewrite inj_Zabs_nat; auto with zarith.
-repeat rewrite Zabs_eq; auto with zarith.
-Qed.
-
-Theorem in_mkZp: forall p, In p mkZp ->  0 <= p < n.
-intros p H; case (in_mkZp_aux (Zabs_nat  (n - 1)) p); auto with zarith.
-rewrite inj_Zabs_nat; auto with zarith.
-repeat rewrite Zabs_eq; auto with zarith.
-Qed.
-
-Theorem mkZp_ulist: ulist mkZp.
-unfold mkZp; apply mkZp_aux_ulist; auto.
-Qed.
-
-(************************************** 
-  Multiplication of two pairs
- **************************************)
-
-Definition pmult (p q: Z) := (p * q) mod n.
-
-(************************************** 
-  Properties of multiplication
- **************************************)
-
-Theorem pmult_assoc: forall p q r, (pmult p (pmult q r)) = (pmult (pmult p q) r).
-assert (Hu: 0 < n); try apply Zlt_trans with 1; auto with zarith.
-generalize Zmod_mod; intros H.
-intros p q r; unfold pmult.
-rewrite (Zmult_mod p); auto.
-repeat rewrite Zmod_mod; auto.
-rewrite (Zmult_mod q); auto.
-rewrite <- Zmult_mod; auto.
-rewrite Zmult_assoc.
-rewrite (Zmult_mod (p * (q mod n))); auto.
-rewrite (Zmult_mod ((p * q) mod n)); auto.
-eq_tac; auto.
-eq_tac; auto.
-rewrite (Zmult_mod p); sauto.
-rewrite Zmod_mod; auto.
-rewrite <- Zmult_mod; sauto.
-Qed.
-
-Theorem pmult_1_l: forall p, In p mkZp -> pmult 1 p = p.
-intros p H; unfold pmult; rewrite Zmult_1_l.
-apply Zmod_small.
-case (in_mkZp p); auto with zarith.
-Qed.
-
-Theorem pmult_1_r: forall p, In p mkZp -> pmult p 1 = p.
-intros p H; unfold pmult; rewrite Zmult_1_r.
-apply Zmod_small.
-case (in_mkZp p); auto with zarith.
-Qed.
-
-Theorem pmult_comm: forall p q, pmult p q = pmult q p.
-intros p q; unfold pmult; rewrite Zmult_comm; auto.
-Qed.
-
-Definition Lrel := isupport_aux _ pmult  mkZp 1 Z_eq_dec (progression Zsucc 0 (Zabs_nat n)).
-
-Theorem rel_prime_is_inv: 
-  forall a, is_inv Z pmult mkZp 1 Z_eq_dec a = if (rel_prime_dec a n) then true else false.
-assert (Hu: 0 < n); try apply Zlt_trans with 1; auto with zarith.
-intros a; case (rel_prime_dec a n); intros H.
-assert (H1: Bezout a n 1); try apply rel_prime_bezout; auto.
-inversion H1 as [c d Hcd]; clear H1.
-assert (pmult (c mod n) a = 1).
-unfold pmult; rewrite Zmult_mod; try rewrite Zmod_mod; auto.
-rewrite <- Zmult_mod; auto.
-replace (c * a) with (1 + (-d) * n).
-rewrite Z_mod_plus; auto with zarith.
-rewrite Zmod_small; auto with zarith.
-rewrite <- Hcd; ring.
-apply is_inv_true with (a := (c mod n)); auto.
-apply mkZp_in; auto with zarith.
-exact pmult_1_l.
-exact pmult_1_r.
-rewrite pmult_comm; auto.
-apply mkZp_in; auto with zarith.
-apply Z_mod_lt; auto with zarith.
-apply is_inv_false.
-intros c H1; left; intros H2; contradict H.
-apply bezout_rel_prime.
-apply Bezout_intro with c  (- (Zdiv (c * a) n)).
-pattern (c * a) at 1; rewrite (Z_div_mod_eq (c * a) n); auto with zarith.
-unfold pmult in H2; rewrite (Zmult_comm c); try rewrite H2.
-ring.
-Qed.
-
-(************************************** 
-   We are now ready to build our group 
- **************************************)
-
-Definition ZPGroup : (FGroup pmult).
-apply IGroup with (support := mkZp) (e:= 1).
-exact Z_eq_dec.
-apply mkZp_ulist.
-apply mkZp_in; auto with zarith.
-intros a b H1 H2; apply mkZp_in.
-unfold pmult; apply Z_mod_lt; auto with zarith.
-intros; apply pmult_assoc.
-exact pmult_1_l.
-exact pmult_1_r.
-Defined.
-
-Theorem in_ZPGroup: forall p, rel_prime p n -> 0 <= p < n -> In p ZPGroup.(s).
-intros p H (H1, H2); unfold ZPGroup; simpl.
-apply isupport_is_in.
-generalize (rel_prime_is_inv p); case (rel_prime_dec p); auto.
-apply mkZp_in; auto with zarith.
-Qed.
-
-
-Theorem phi_is_length: phi n = Z_of_nat (length Lrel).
-assert (Hu: 0 < n); try apply Zlt_trans with 1; auto with zarith.
-rewrite phi_def_with_0; auto.
-unfold Zsum, Lrel; rewrite Zle_imp_le_bool; auto with zarith.
-replace (1 + (n - 1) - 0) with n; auto with zarith.
-elim (progression Zsucc 0 (Zabs_nat n)); simpl; auto.
-intros a l1 Rec.
-rewrite Rec.
-rewrite rel_prime_is_inv.
-case (rel_prime_dec a n); auto with zarith.
-simpl length; rewrite inj_S; auto with zarith.
-Qed.
-
-Theorem phi_is_order: phi n = g_order ZPGroup.
-unfold g_order; rewrite phi_is_length.
-eq_tac; apply permutation_length.
-apply ulist_incl2_permutation.
-unfold Lrel; apply isupport_aux_ulist.
-apply ulist_Zprogression; auto.
-apply ZPGroup.(unique_s).
-intros a H; unfold ZPGroup; simpl.
-apply isupport_is_in.
-unfold Lrel in H; apply  isupport_aux_is_inv_true with (1 := H).
-apply mkZp_in; auto.
-assert (In a (progression Zsucc 0 (Zabs_nat  n))). 
-apply  (isupport_aux_incl _ pmult mkZp 1 Z_eq_dec); auto.
-split.
-apply Zprogression_le_init with (1 := H0).
-replace n with (0 + Z_of_nat (Zabs_nat n)).
-apply Zprogression_le_end with (1 := H0).
-rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-intros a H; unfold Lrel; simpl.
-apply isupport_aux_is_in.
-simpl in H; apply  isupport_is_inv_true with (1 := H).
-apply in_Zprogression.
-rewrite Zplus_0_l; rewrite inj_Zabs_nat; auto with zarith.
-rewrite Zabs_eq; auto with zarith.
-assert (In a mkZp). 
-apply  (isupport_aux_incl _ pmult mkZp 1 Z_eq_dec); auto.
-apply in_mkZp; auto.
-Qed.
-
-Theorem Zp_cyclic: prime n -> cyclic Z_eq_dec ZPGroup.
-intros H1.
-unfold ZPGroup, pmult;
-generalize (cyclic_field _ (fun x y => (x + y) mod n) (fun x y => (x *  y) mod n) (fun x => (-x) mod n) 0);
-unfold IA; intros tmp; apply tmp; clear tmp; auto.
-intros; discriminate.
-apply mkZp_in; auto with zarith.
-intros; apply mkZp_in; auto with zarith.
-apply Z_mod_lt; auto with zarith.
-intros; rewrite Zplus_0_l; auto.
-apply Zmod_small; auto.
-apply in_mkZp; auto.
-intros; rewrite Zplus_comm; auto.
-intros a b c Ha Hb Hc.
-pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith.
-pattern c at 2; rewrite <- (Zmod_small c n); auto with zarith.
-repeat rewrite <- Zplus_mod; auto with zarith.
-eq_tac; auto with zarith.
-apply in_mkZp; auto.
-apply in_mkZp; auto.
-intros; eq_tac; auto with zarith.
-intros a b c Ha Hb Hc.
-pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith.
-repeat rewrite <- Zmult_mod; auto with zarith.
-repeat rewrite <- Zplus_mod; auto with zarith.
-eq_tac; auto with zarith.
-apply in_mkZp; auto.
-intros; apply mkZp_in; apply Z_mod_lt; auto with zarith.
-intros a Ha.
-pattern a at 1; rewrite <- (Zmod_small a n); auto with zarith.
-repeat rewrite <- Zplus_mod; auto with zarith.
-rewrite <- (Zmod_small 0 n); auto with zarith.
-eq_tac; auto with zarith.
-apply in_mkZp; auto.
-intros a b Ha Hb H; case (prime_mult n H1 a b).
-apply Zmod_divide; auto with zarith.
-intros H2; left.
-case (Zle_lt_or_eq 0 a); auto.
-case (in_mkZp a); auto.
-intros H3; absurd (n <= a).
-apply Zlt_not_le.
-case (in_mkZp a); auto.
-apply Zdivide_le; auto with zarith.
-intros H2; right.
-case (Zle_lt_or_eq 0 b); auto.
-case (in_mkZp b); auto.
-intros H3; absurd (n <= b).
-apply Zlt_not_le.
-case (in_mkZp b); auto.
-apply Zdivide_le; auto with zarith.
-Qed.
-
-End Zp.
-
-(* Definition of the order (0 for q < 1) *)
-
-Definition Zorder: Z -> Z -> Z.
-intros p q; case (Z_le_dec q 1); intros H.
-exact 0.
-refine (e_order Z_eq_dec (p mod q) (ZPGroup q _)); auto with zarith.
-Defined.
-
-Theorem Zorder_pos: forall p n, 0 <= Zorder p n.
-intros p n; unfold Zorder.
-case (Z_le_dec n 1); auto with zarith.
-intros n1.
-apply Zlt_le_weak; apply e_order_pos.
-Qed.
-
-Theorem in_mod_ZPGroup
-     : forall (n : Z) (n_pos : 1 < n) (p : Z),
-       rel_prime p n -> In (p mod n) (s (ZPGroup n n_pos)).
-intros n H p H1.
-apply in_ZPGroup; auto.
-apply rel_prime_mod; auto with zarith.
-apply Z_mod_lt; auto with zarith.
-Qed.
-
-
-Theorem Zpower_mod_is_gpow: 
-  forall p q n (Hn: 1 < n), rel_prime p n -> 0 <= q -> p ^ q mod n = gpow (p mod n) (ZPGroup n Hn) q. 
-intros p q n H Hp H1; generalize H1; pattern q; apply natlike_ind; simpl; auto.
-intros _; apply Zmod_small; auto with zarith.
-intros n1 Hn1 Rec _; simpl.
-generalize (in_mod_ZPGroup _ H _ Hp); intros Hu.
-unfold Zsucc; rewrite Zpower_exp; try rewrite Zpower_1_r; auto with zarith.
-rewrite gpow_add; auto with zarith.
-rewrite gpow_1; auto; rewrite <- Rec; auto.
-rewrite Zmult_mod; auto.
-Qed.
-
-
-Theorem Zorder_div_power: forall p q n, 1 < n -> rel_prime p n -> p ^ q  mod n = 1 -> (Zorder p n | q). 
-intros p q n H H1 H2.
-assert (Hq: 0 <= q).
-generalize H2; case q; simpl; auto with zarith.
-intros p1 H3; contradict H3; rewrite Zmod_small; auto with zarith.
-unfold Zorder; case (Z_le_dec n 1).
-intros H3; contradict H; auto with zarith.
-intros H3; apply e_order_divide_gpow; auto.
-apply in_mod_ZPGroup; auto.
-rewrite <- Zpower_mod_is_gpow; auto with zarith.
-Qed.
-
-Theorem Zorder_div:  forall p n,  prime n -> ~(n | p) -> (Zorder p n | n - 1). 
-intros p n H; unfold Zorder.
-case (Z_le_dec n 1); intros H1 H2.
-contradict H1; generalize (prime_ge_2 n H); auto with zarith.
-rewrite <- prime_phi_n_minus_1; auto.
-match goal with |- context[ZPGroup _ ?H2] => rewrite phi_is_order with (n_pos := H2) end.
-apply e_order_divide_g_order; auto.
-apply in_mod_ZPGroup; auto.
-apply rel_prime_sym; apply prime_rel_prime; auto.
-Qed.
-
-
-Theorem Zorder_power_is_1:  forall p n, 1 < n -> rel_prime p n -> p ^ (Zorder p n)  mod n = 1.
-intros p n H H1;  unfold Zorder.
-case (Z_le_dec n 1); intros H2.
-contradict H; auto with zarith.
-let x := match goal with |- context[ZPGroup _ ?X] => X end  in  rewrite Zpower_mod_is_gpow with (Hn := x); auto with zarith.
-rewrite gpow_e_order_is_e.
-reflexivity.
-apply in_mod_ZPGroup; auto.
-apply Zlt_le_weak; apply e_order_pos.
-Qed.
-
-Theorem Zorder_power_pos: forall p n, 1 < n -> rel_prime p n -> 0 < Zorder p n.
-intros p n H H1;  unfold Zorder.
-case (Z_le_dec n 1); intros H2.
-contradict H; auto with zarith.
-apply e_order_pos.
-Qed.
-
-Theorem phi_power_is_1:  forall p n, 1 < n -> rel_prime p n -> p ^ (phi n)  mod n = 1.
-intros p n H H1.
-assert (V1:= Zorder_power_pos p n H H1).
-assert (H2: (Zorder p n | phi n)).
-unfold Zorder.
-case (Z_le_dec n 1); intros H2.
-contradict H; auto with zarith.
-match goal with |- context[ZPGroup n ?H] =>
-rewrite phi_is_order  with (n_pos := H)
-end.
-apply e_order_divide_g_order.
-apply in_mod_ZPGroup; auto.
-case H2; clear H2; intros q H2; rewrite H2.
-rewrite Zmult_comm.
-assert (V2 := (phi_pos _ H)).
-assert (V3: 0 <= q).
-rewrite H2 in V2.
-apply Zlt_le_weak; apply Zmult_lt_0_reg_r with (2 := V2); auto with zarith.
-rewrite Zpower_mult; auto with zarith.
-rewrite Zpower_mod; auto with zarith.
-rewrite Zorder_power_is_1; auto.
-rewrite Zpower_1_l; auto with zarith.
-apply Zmod_small; auto with zarith.
-Qed.