(*************************************************************)
(*      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      *)
(*************************************************************)

(***********************************************************************
      Cyclic.v                                                                                       
                                                                                                         
      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.

Open Scope Z_scope.

Section Cyclic.

Variable A: Set.
Variable plus mult: A -> A -> A.
Variable op: A -> A.
Variable zero one: A.
Variable support: list A.
Variable e: A.

Hypothesis A_dec: forall a b: A, {a = b} + {a <> b}.
Hypothesis e_not_zero: zero <> e.
Hypothesis support_ulist: ulist support.
Hypothesis e_in_support: In e support.
Hypothesis zero_in_support: In zero support.
Hypothesis mult_internal: forall a b, In a support -> In b support -> In (mult a b) support.
Hypothesis mult_assoc: forall a b c, In a support -> In b support -> In c support -> mult a (mult b c) = mult (mult a b) c.
Hypothesis e_is_zero_l:  forall a, In a support ->  mult e a = a.
Hypothesis e_is_zero_r:  forall a, In a support ->  mult a e = a.
Hypothesis plus_internal: forall a b, In a support -> In b support -> In (plus a b) support.
Hypothesis plus_zero: forall a, In a support -> plus zero a = a.
Hypothesis plus_comm: forall a b, In a support -> In b support -> plus a b = plus b a.
Hypothesis plus_assoc: forall a b c, In a support -> In b support -> In c support -> plus a (plus b c) = plus (plus a b) c.
Hypothesis mult_zero: forall a, In a support -> mult zero a = zero.
Hypothesis mult_comm: forall a b, In a support -> In b support ->mult a b = mult b a.
Hypothesis mult_plus_distr: forall a b c, In a support -> In b support -> In c support -> mult a (plus b c) = plus (mult a b) (mult a c).
Hypothesis op_internal: forall a, In a support -> In (op a) support.
Hypothesis plus_op_zero: forall a, In a support -> plus a (op a) = zero.
Hypothesis mult_integral: forall a b, In a support -> In b support -> mult a b = zero -> a = zero \/ b = zero.

Definition IA := (IGroup A mult support e A_dec support_ulist e_in_support mult_internal 
                             mult_assoc
                             e_is_zero_l e_is_zero_r).

Hint Resolve (fun x => isupport_incl _ mult support e A_dec x).

Theorem gpow_evaln: forall n, 0 < n -> 
  exists p, (length p <=  Zabs_nat n)%nat /\  (forall i, In i p -> In i support) /\
  forall x, In x IA.(s) -> eval A plus mult zero (zero::p) x = gpow x IA n.
intros n Hn; generalize Hn; pattern n; apply natlike_ind; auto with zarith.
intros H1; contradict H1; auto with zarith.
intros x Hx Rec _.
case Zle_lt_or_eq with (1 := Hx); clear Hx; intros Hx; subst; simpl.
case Rec; auto; simpl; intros p (Hp1, (Hp2, Hp3)); clear Rec.
exists (zero::p); split; simpl.
rewrite Zabs_nat_Zsucc; auto with arith zarith.
split.
intros i [Hi | Hi]; try rewrite <- Hi; auto.
intros x1 Hx1; simpl.
rewrite Hp3; repeat rewrite plus_zero; unfold Zsucc; try rewrite gpow_add; auto with zarith.
rewrite gpow_1; try apply mult_comm; auto.
apply  (fun x => isupport_incl _ mult support e A_dec x); auto.
change (In (gpow x1 IA x) IA.(s)).
apply gpow_in; auto.
apply mult_internal; auto.
apply  (fun x => isupport_incl _ mult support e A_dec x); auto.
change (In (gpow x1 IA x) IA.(s)).
apply gpow_in; auto.
exists (e:: nil); split; simpl.
compute; auto with arith.
split.
intros i [Hi | Hi]; try rewrite <- Hi; auto; case Hi.
intros x Hx; simpl.
rewrite plus_zero; rewrite (fun x => mult_comm x zero); try rewrite mult_zero; auto.
rewrite plus_comm; try rewrite plus_zero; auto.
Qed.

Definition check_list_gpow: forall l n, (incl l IA.(s)) -> {forall a, In a l -> gpow a IA n = e} + {exists a, In a l /\  gpow a IA n <> e}.
intros l n; elim l; simpl; auto.
intros H; left; intros a H1; case H1.
intros a l1 Rec H.
case (A_dec (gpow a IA n) e); intros H2.
case Rec; try intros H3. 
apply incl_tran with (2 := H); auto with datatypes.
left; intros a1 H4; case H4; auto.
intros H5; rewrite <- H5; auto.
right; case H3; clear H3; intros a1 (H3, H4).
exists a1; auto.
right; exists a; auto.
Defined.


Theorem prime_power_div: forall p q i, prime p -> 0 <= q -> 0 <= i -> (q | p ^ i)  -> exists j, 0 <= j <= i /\ q = p ^ j.
intros p q i Hp Hq Hi H.
assert (Hp1: 0 < p).
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
pattern q; apply prime_div_induction with (p ^ i); auto with zarith.
exists 0; rewrite Zpower_0_r; auto with zarith.
intros p1 i1 Hp2 Hi1 H1.
case Zle_lt_or_eq with (1 := Hi1); clear Hi1; intros Hi1; subst.
assert (Heq: p1 = p).
apply prime_div_Zpower_prime with i; auto.
apply Zdivide_trans with (2 := H1).
apply Zpower_divide; auto with zarith.
exists i1; split; auto; try split; auto with zarith.
case (Zle_or_lt i1 i); auto; intros H2.
absurd (p1 ^ i1 <= p  ^ i).
apply Zlt_not_le; rewrite Heq; apply Zpower_lt_monotone; auto with zarith.
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
apply Zdivide_le; auto with zarith.
rewrite Heq; auto.
exists 0; repeat rewrite Zpower_exp_0; auto with zarith.
intros p1 q1 Hpq (j1,((Hj1, Hj2), Hj3)) (j2, ((Hj4, Hj5), Hj6)).
case Zle_lt_or_eq with (1 := Hj1); clear Hj1; intros Hj1; subst.
case Zle_lt_or_eq with (1 := Hj4); clear Hj4; intros Hj4; subst.
inversion Hpq as [ H0 H1 H2].
absurd (p | 1).
intros H3; absurd (1 < p).
apply Zle_not_lt; apply Zdivide_le; auto with zarith.
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
apply H2; apply Zpower_divide; auto with zarith.
exists j1; rewrite Zpower_0_r; auto with zarith.
exists j2; rewrite Zpower_0_r; auto with zarith.
Qed.

Theorem inj_lt_inv: forall n m : nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
intros n m H; case (le_or_lt m n); auto; intros H1; contradict H.
apply Zle_not_lt; apply inj_le; auto.
Qed.

Theorem not_all_solutions: forall i, 0 < i < g_order IA -> exists a, In a IA.(s) /\ gpow a IA i <> e.
intros i (Hi, Hi2).
case (check_list_gpow IA.(s) i); try intros H; auto with datatypes.
case (gpow_evaln i); auto; intros p (Hp1, (Hp2, Hp3)).
absurd ((op e) = zero).
intros H1; case e_not_zero.
rewrite <- (plus_op_zero e); try rewrite H1; auto. 
rewrite plus_comm; auto.
apply (root_max_is_zero _ (fun x => In x support) plus mult op zero) with (l := IA.(s)) (p := op e :: p); auto with datatypes.
simpl; intros x [Hx | Hx]; try rewrite <- Hx; auto.
intros x Hx.
generalize (Hp3 _ Hx); simpl; rewrite plus_zero; auto.
intros tmp; rewrite tmp; clear tmp.
rewrite H; auto; rewrite plus_comm; auto with datatypes.
apply mult_internal; auto.
apply eval_P; auto.
simpl; apply lt_le_S; apply le_lt_trans with (1 := Hp1).
apply inj_lt_inv.
rewrite inj_Zabs_nat; auto with zarith.
rewrite Zabs_eq; auto with zarith.
Qed.
 
Theorem divide_g_order_e_order: forall n, 0 <= n -> (n | g_order IA) -> exists a, In a IA.(s) /\ e_order A_dec  a IA = n.
intros n Hn H.
assert (Hg: 0 < g_order IA).
apply g_order_pos.
assert (He: forall a, 0 <= e_order A_dec a IA).
intros a; apply Zlt_le_weak; apply e_order_pos.
pattern n; apply prime_div_induction with (n := g_order IA); auto.
exists e; split; auto.
apply IA.(e_in_s).
apply Zle_antisym.
apply Zdivide_le; auto with zarith.
apply e_order_divide_gpow; auto with zarith.
apply IA.(e_in_s).
rewrite gpow_1; auto.
apply IA.(e_in_s).
match goal with |- (_ <= ?X) => assert (0 < X) end; try apply e_order_pos; auto with zarith.
intros p i Hp Hi K.
assert (Hp1: 0 < p).
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
assert (Hi1: 0 < p ^ i).
apply Zpower_gt_0; auto.
case Zle_lt_or_eq with (1 := Hi); clear Hi; intros Hi; subst.
case (not_all_solutions (g_order IA / p)).
apply Zdivide_Zdiv_lt_pos; auto with zarith.
apply Zlt_le_trans with 2; try apply prime_ge_2; auto with zarith.
apply Zdivide_trans with (2 := K).
apply Zpower_divide; auto.
intros a (Ha1, Ha2).
exists (gpow a IA (g_order IA  / p ^ i)); split.
apply gpow_in; auto.
match goal with |- ?X = ?Y => assert (H1: (X | Y) ) end; auto.
apply e_order_divide_gpow; auto with zarith.
apply gpow_in; auto.
rewrite <- gpow_gpow; auto with zarith.
rewrite Zmult_comm; rewrite <- Zdivide_Zdiv_eq; auto with zarith.
apply fermat_gen; auto.
apply Z_div_pos; auto with zarith.
case prime_power_div with (4 := H1); auto with zarith.
intros j ((Hj1, Hj2), Hj3).
case Zle_lt_or_eq with (1 := Hj2); intros Hj4; subst; auto.
case Ha2.
replace (g_order IA) with (((g_order IA / p ^i) * p ^ j) * p ^ (i - j - 1) * p).
rewrite Z_div_mult; auto with zarith.
repeat rewrite gpow_gpow; auto with zarith.
rewrite <- Hj3.
rewrite gpow_e_order_is_e; auto with zarith.
rewrite gpow_e; auto.
apply Zlt_le_weak; apply Zpower_gt_0; auto with zarith.
apply gpow_in; auto.
apply Z_div_pos; auto with zarith.
apply Zmult_le_0_compat; try apply Z_div_pos; auto with zarith.
pattern p at 4; rewrite <- Zpower_1_r.
repeat rewrite <- Zmult_assoc; repeat rewrite <- Zpower_exp; auto with zarith.
replace (j + (i - j - 1 + 1)) with i; auto with zarith.
apply sym_equal; rewrite Zmult_comm; apply Zdivide_Zdiv_eq; auto with zarith.
rewrite Zpower_0_r; exists e; split.
apply IA.(e_in_s).
match goal with |- ?X = 1 => assert (tmp: 0 < X); try apply e_order_pos;
case Zle_lt_or_eq with 1 X; auto with zarith; clear tmp; intros H1 end.
absurd (gpow IA.(FGroup.e) IA 1 = IA.(FGroup.e)).
apply gpow_e_order_lt_is_not_e with A_dec; auto with zarith.
apply gpow_e; auto with zarith.
intros p q H1 (a, (Ha1, Ha2)) (b, (Hb1, Hb2)).
exists (mult a b); split.
apply IA.(internal); auto.
rewrite <- Ha2; rewrite <- Hb2; apply order_mult; auto.
rewrite Ha2; rewrite Hb2; auto.
Qed.

Set Implicit Arguments.
Definition cyclic (A: Set) A_dec (op: A -> A -> A) (G: FGroup op):= exists a, In a G.(s) /\ e_order A_dec a G = g_order G.
Unset Implicit Arguments.

Theorem cyclic_field: cyclic A_dec IA.
red; apply divide_g_order_e_order; auto.
apply Zlt_le_weak; apply g_order_pos.
exists 1; ring.
Qed.

End Cyclic.