diff options
Diffstat (limited to 'coqprime-8.4/Coqprime/Lagrange.v')
| -rw-r--r-- | coqprime-8.4/Coqprime/Lagrange.v | 179 |
1 files changed, 179 insertions, 0 deletions
diff --git a/coqprime-8.4/Coqprime/Lagrange.v b/coqprime-8.4/Coqprime/Lagrange.v new file mode 100644 index 000000000..b890c5621 --- /dev/null +++ b/coqprime-8.4/Coqprime/Lagrange.v @@ -0,0 +1,179 @@ + +(*************************************************************) +(* 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 *) +(*************************************************************) + +(********************************************************************** + Lagrange.v + + Proof of Lagrange theorem: + the oder of a subgroup divides the order of a group + + Definition: lagrange + **********************************************************************) +Require Import Coq.Lists.List. +Require Import Coqprime.UList. +Require Import Coqprime.ListAux. +Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Coqprime.NatAux. +Require Import Coqprime.FGroup. + +Open Scope Z_scope. + +Section Lagrange. + +Variable A: Set. + +Variable A_dec: forall a b: A, {a = b} + {~ a = b}. + +Variable op: A -> A -> A. + +Variable G: (FGroup op). + +Variable H:(FGroup op). + +Hypothesis G_in_H: (incl G.(s) H.(s)). + +(************************************** + A group and a subgroup have the same neutral element + **************************************) + +Theorem same_e_for_H_and_G: H.(e) = G.(e). +apply trans_equal with (op H.(e) H.(e)); sauto. +apply trans_equal with (op H.(e) (op G.(e) (H.(i) G.(e)))); sauto. +eq_tac; sauto. +apply trans_equal with (op G.(e) (op G.(e) (H.(i) G.(e)))); sauto. +repeat rewrite H.(assoc); sauto. +eq_tac; sauto. +apply trans_equal with G.(e); sauto. +apply trans_equal with (op G.(e) H.(e)); sauto. +eq_tac; sauto. +Qed. + +(************************************** + The proof works like this. + If G = {e, g1, g2, g3, .., gn} and {e, h1, h2, h3, ..., hm} + we construct the list mkGH + {e, g1, g2, g3, ...., gn + hi*e, hi * g1, hi * g2, ..., hi * gn if hi does not appear before + .... + hk*e, hk * g1, hk * g2, ..., hk * gn if hk does not appear before + } + that contains all the element of H. + We show that this list does not contain double (ulist). + **************************************) + +Fixpoint mkList (base l: (list A)) { struct l} : (list A) := + match l with + nil => nil + | cons a l1 => let r1 := mkList base l1 in + if (In_dec A_dec a r1) then r1 else + (map (op a) base) ++ r1 + end. + +Definition mkGH := mkList G.(s) H.(s). + +Theorem mkGH_length: divide (length G.(s)) (length mkGH). +unfold mkGH; elim H.(s); simpl. +exists 0%nat; auto with arith. +intros a l1 (c, H1); case (In_dec A_dec a (mkList G.(s) l1)); intros H2. +exists c; auto. +exists (1 + c)%nat; rewrite ListAux.length_app; rewrite ListAux.length_map; rewrite H1; ring. +Qed. + +Theorem mkGH_incl: incl H.(s) mkGH. +assert (H1: forall l, incl l H.(s) -> incl l (mkList G.(s) l)). +intros l; elim l; simpl; auto with datatypes. +intros a l1 H1 H2. +case (In_dec A_dec a (mkList (s G) l1)); auto with datatypes. +intros H3; assert (H4: incl l1 (mkList (s G) l1)). +apply H1; auto with datatypes. +intros b H4; apply H2; auto with datatypes. +intros b; simpl; intros [H5 | H5]; subst; auto. +intros _ b; simpl; intros [H3 | H3]; subst; auto. +apply in_or_app; left. +cut (In H.(e) G.(s)). +elim (s G); simpl; auto. +intros c l2 Hl2 [H3 | H3]; subst; sauto. +assert (In b H.(s)); sauto. +apply (H2 b); auto with datatypes. +rewrite same_e_for_H_and_G; sauto. +apply in_or_app; right. +apply H1; auto with datatypes. +apply incl_tran with (2:= H2); auto with datatypes. +unfold mkGH; apply H1; auto with datatypes. +Qed. + +Theorem incl_mkGH: incl mkGH H.(s). +assert (H1: forall l, incl l H.(s) -> incl (mkList G.(s) l) H.(s)). +intros l; elim l; simpl; auto with datatypes. +intros a l1 H1 H2. +case (In_dec A_dec a (mkList (s G) l1)); intros H3; auto with datatypes. +apply H1; apply incl_tran with (2 := H2); auto with datatypes. +apply incl_app. +intros b H4. +case ListAux.in_map_inv with (1:= H4); auto. +intros c (Hc1, Hc2); subst; sauto. +apply internal; auto with datatypes. +apply H1; apply incl_tran with (2 := H2); auto with datatypes. +unfold mkGH; apply H1; auto with datatypes. +Qed. + +Theorem ulist_mkGH: ulist mkGH. +assert (H1: forall l, incl l H.(s) -> ulist (mkList G.(s) l)). +intros l; elim l; simpl; auto with datatypes. +intros a l1 H1 H2. +case (In_dec A_dec a (mkList (s G) l1)); intros H3; auto with datatypes. +apply H1; apply incl_tran with (2 := H2); auto with datatypes. +apply ulist_app; auto. +apply ulist_map; sauto. +intros x y H4 H5 H6; apply g_cancel_l with (g:= H) (a := a); sauto. +apply H2; auto with datatypes. +apply H1; apply incl_tran with (2 := H2); auto with datatypes. +intros b H4 H5. +case ListAux.in_map_inv with (1:= H4); auto. +intros c (Hc, Hc1); subst. +assert (H6: forall l a b, In b G.(s) -> incl l H.(s) -> In a (mkList G.(s) l) -> In (op a b) (mkList G.(s) l)). +intros ll u v; elim ll; simpl; auto with datatypes. +intros w ll1 T0 T1 T2. +case (In_dec A_dec w (mkList (s G) ll1)); intros T3 T4; auto with datatypes. +apply T0; auto; apply incl_tran with (2:= T2); auto with datatypes. +case in_app_or with (1 := T4); intros T5; auto with datatypes. +apply in_or_app; left. +case ListAux.in_map_inv with (1:= T5); auto. +intros z (Hz1, Hz2); subst. +replace (op (op w z) v) with (op w (op z v)); sauto. +apply in_map; sauto. +apply assoc with H; auto with datatypes. +apply in_or_app; right; auto with datatypes. +apply T0; try apply incl_tran with (2 := T2); auto with datatypes. +case H3; replace a with (op (op a c) (G.(i) c)); auto with datatypes. +apply H6; sauto. +apply incl_tran with (2 := H2); auto with datatypes. +apply trans_equal with (op a (op c (G.(i) c))); sauto. +apply sym_equal; apply assoc with H; auto with datatypes. +replace (op c (G.(i) c)) with (G.(e)); sauto. +rewrite <- same_e_for_H_and_G. +assert (In a H.(s)); sauto; apply (H2 a); auto with datatypes. +unfold mkGH; apply H1; auto with datatypes. +Qed. + +(************************************** + Lagrange theorem + **************************************) + +Theorem lagrange: (g_order G | (g_order H)). +unfold g_order. +rewrite Permutation.permutation_length with (l := H.(s)) (m:= mkGH). +case mkGH_length; intros x H1; exists (Z_of_nat x). +rewrite H1; rewrite Zmult_comm; apply inj_mult. +apply ulist_incl2_permutation; auto. +apply ulist_mkGH. +apply mkGH_incl. +apply incl_mkGH. +Qed. + +End Lagrange. |