1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
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.
|
