diff options
Diffstat (limited to 'coqprime-8.4/Coqprime/FGroup.v')
| -rw-r--r-- | coqprime-8.4/Coqprime/FGroup.v | 123 |
1 files changed, 123 insertions, 0 deletions
diff --git a/coqprime-8.4/Coqprime/FGroup.v b/coqprime-8.4/Coqprime/FGroup.v new file mode 100644 index 000000000..0bcc9ebf1 --- /dev/null +++ b/coqprime-8.4/Coqprime/FGroup.v @@ -0,0 +1,123 @@ + +(*************************************************************) +(* 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 *) +(*************************************************************) + +(********************************************************************** + FGroup.v + + Defintion and properties of finite groups + + Definition: FGroup + **********************************************************************) +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.Tactic. +Require Import Coq.ZArith.ZArith. + +Open Scope Z_scope. + +Set Implicit Arguments. + +(************************************** + A finite group is defined for an operation op + it has a support (s) + op operates inside the group (internal) + op is associative (assoc) + it has an element (e) that is neutral (e_is_zero_l e_is_zero_r) + it has an inverse operator (i) + the inverse operates inside the group (i_internal) + it gives an inverse (i_is_inverse_l is_is_inverse_r) + **************************************) + +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 +}. + +(************************************** + The order of a group is the lengh of the support + **************************************) + +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. + +(************************************** + Some properties of a finite group + **************************************) + +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. + +(************************************** + A group has at least one element + **************************************) + +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. |