Library Coqprime.PrimalityTest.FGroup

Require Import List.
Require Import UList.
Require Import Tactic.
Require Import ZArith.

Open Scope Z_scope.

Set Implicit Arguments.


Record FGroup (A: Set) (op: A -> A -> A): Set := mkGroup
  {s : (list A);
   unique_s: ulist s;
   internal: forall a b, In a s -> In b s -> In (op a b) s;
   assoc: forall a b c, In a s -> In b s -> In c s -> op a (op b c) = op (op a b) c;
   e: A;
   e_in_s: In e s;
   e_is_zero_l: forall a, In a s -> op e a = a;
   e_is_zero_r: forall a, In a s -> op a e = a;
   i: A -> A;
   i_internal: forall a, In a s -> In (i a) s;
   i_is_inverse_l: forall a, (In a s) -> op (i a) a = e;
   i_is_inverse_r: forall a, (In a s) -> op a (i a) = e
}.


Definition g_order (A: Set) (op: A -> A -> A) (g: FGroup op) := Z_of_nat (length g.(s)).

Unset Implicit Arguments.

Hint Resolve unique_s internal e_in_s e_is_zero_l e_is_zero_r i_internal
  i_is_inverse_l i_is_inverse_r assoc.

Section FGroup.

Variable A: Set.
Variable op: A -> A -> A.


Theorem g_cancel_l: forall (g : FGroup op), forall a b c, In a g.(s) -> In b g.(s) -> In c g.(s) -> op a b = op a c -> b = c.
intros g a b c H1 H2 H3 H4; apply trans_equal with (op g.(e) b); sauto.
replace (g.(e)) with (op (g.(i) a) a); sauto.
apply trans_equal with (op (i g a) (op a b)); sauto.
apply sym_equal; apply assoc with g; auto.
rewrite H4.
apply trans_equal with (op (op (i g a) a) c); sauto.
apply assoc with g; auto.
replace (op (g.(i) a) a) with g.(e); sauto.
Qed.

Theorem g_cancel_r: forall (g : FGroup op), forall a b c, In a g.(s) -> In b g.(s) -> In c g.(s) -> op b a = op c a -> b = c.
intros g a b c H1 H2 H3 H4; apply trans_equal with (op b g.(e)); sauto.
replace (g.(e)) with (op a (g.(i) a)); sauto.
apply trans_equal with (op (op b a) (i g a)); sauto.
apply assoc with g; auto.
rewrite H4.
apply trans_equal with (op c (op a (i g a))); sauto.
apply sym_equal; apply assoc with g; sauto.
replace (op a (g.(i) a)) with g.(e); sauto.
Qed.

Theorem e_unique: forall (g : FGroup op), forall e1, In e1 g.(s) -> (forall a, In a g.(s) -> op e1 a = a) -> e1 = g.(e).
intros g e1 He1 H2.
apply trans_equal with (op e1 g.(e)); sauto.
Qed.

Theorem inv_op: forall (g: FGroup op) a b, In a g.(s) -> In b g.(s) -> g.(i) (op a b) = op (g.(i) b) (g.(i) a).
intros g a1 b1 H1 H2; apply g_cancel_l with (g := g) (a := op a1 b1); sauto.
repeat rewrite g.(assoc); sauto.
apply trans_equal with g.(e); sauto.
rewrite <- g.(assoc) with (a := a1); sauto.
rewrite g.(i_is_inverse_r); sauto.
rewrite g.(e_is_zero_r); sauto.
Qed.

Theorem i_e: forall (g: FGroup op), g.(i) g.(e) = g.(e).
intro g; apply g_cancel_l with (g:= g) (a := g.(e)); sauto.
apply trans_equal with g.(e); sauto.
Qed.


Theorem g_order_pos: forall g: FGroup op, 0 < g_order g.
intro g; generalize g.(e_in_s); unfold g_order; case g.(s); simpl; auto with zarith.
Qed.

End FGroup.