]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/algebra/groups.ma
First part of a slightly more interesting proof on finite (and enumerable)
[helm.git] / helm / matita / library / algebra / groups.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/algebra/groups/".
16
17 include "algebra/monoids.ma".
18 include "nat/le_arith.ma".
19
20 record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
21  { opp_is_left_inverse: is_left_inverse M opp;
22    opp_is_right_inverse: is_right_inverse M opp
23  }.
24  
25 record Group : Type ≝
26  { monoid: Monoid;
27    opp: monoid -> monoid;
28    group_properties: isGroup ? opp
29  }.
30
31 coercion cic:/matita/algebra/groups/monoid.con.
32
33 notation < "G"
34 for @{ 'monoid $G }.
35
36 interpretation "Monoid coercion" 'monoid G =
37  (cic:/matita/algebra/groups/monoid.con G).
38
39 notation < "G"
40 for @{ 'type_of_group $G }.
41
42 interpretation "Type_of_group coercion" 'type_of_group G =
43  (cic:/matita/algebra/groups/Type_of_Group.con G).
44
45 notation < "G"
46 for @{ 'semigroup_of_group $G }.
47
48 interpretation "Semigroup_of_group coercion" 'semigroup_of_group G =
49  (cic:/matita/algebra/groups/SemiGroup_of_Group.con G).
50
51 notation "hvbox(x \sup (-1))" with precedence 89
52 for @{ 'gopp $x }.
53
54 interpretation "Group inverse" 'gopp x =
55  (cic:/matita/algebra/groups/opp.con _ x).
56
57 definition left_cancellable ≝
58  λT:Type. λop: T -> T -> T.
59   ∀x. injective ? ? (op x).
60   
61 definition right_cancellable ≝
62  λT:Type. λop: T -> T -> T.
63   ∀x. injective ? ? (λz.op z x).
64   
65 theorem eq_op_x_y_op_x_z_to_eq:
66  ∀G:Group. left_cancellable G (op G).
67 intros;
68 unfold left_cancellable;
69 unfold injective;
70 intros (x y z);
71 rewrite < (e_is_left_unit ? ? (monoid_properties G));
72 rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
73 rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
74 rewrite > (semigroup_properties G);
75 rewrite > (semigroup_properties G);
76 apply eq_f;
77 assumption.
78 qed.
79
80
81 theorem eq_op_x_y_op_z_y_to_eq:
82  ∀G:Group. right_cancellable G (op G).
83 intros;
84 unfold right_cancellable;
85 unfold injective;
86 simplify;fold simplify (op G); 
87 intros (x y z);
88 rewrite < (e_is_right_unit ? ? (monoid_properties G));
89 rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
90 rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
91 rewrite < (semigroup_properties G);
92 rewrite < (semigroup_properties G);
93 rewrite > H;
94 reflexivity.
95 qed.
96
97
98 record finite_enumerable (T:Type) : Type ≝
99  { order: nat;
100    repr: nat → T;
101    index_of: T → nat;
102    index_of_sur: ∀x.index_of x ≤ order;
103    index_of_repr: ∀n. n≤order → index_of (repr n) = n;
104    repr_index_of: ∀x. repr (index_of x) = x
105  }.
106
107 notation < "hvbox(C \sub i)" with precedence 89
108 for @{ 'repr $C $i }.
109
110 interpretation "Finite_enumerable representation" 'repr C i =
111  (cic:/matita/algebra/groups/repr.con C _ i).
112  
113 notation < "hvbox(|C|)" with precedence 89
114 for @{ 'card $C }.
115
116 interpretation "Finite_enumerable order" 'card C =
117  (cic:/matita/algebra/groups/order.con C _).
118
119 theorem repr_inj:
120  ∀T:Type. ∀H:finite_enumerable T.
121   ∀n,n'. n ≤ order ? H → n' ≤ order ? H →
122    repr ? H n = repr ? H n' → n=n'.
123 intros;
124 rewrite < (index_of_repr ? ? ? H1);
125 rewrite > H3;
126 apply index_of_repr;
127 assumption.
128 qed.
129
130 theorem foo:
131  ∀G:SemiGroup.
132   finite_enumerable (carrier G) →
133    left_cancellable (carrier G) (op G) →
134     right_cancellable (carrier G) (op G) →
135      ∃e:G. isMonoid ? e.
136 intros (G H);
137 letin f ≝ (λn.index_of ? H ((repr ? H O)·(repr ? H n)));
138 cut (∀n.n ≤ order ? H → ∃m.f m = n);
139 [ letin EX ≝ (Hcut O ?);
140   [ apply le_O_n
141   | clearbody EX;
142     clear Hcut;
143     unfold f in EX;
144     elim EX;
145     letin HH ≝ (eq_f ? ? (repr ? H) ? ? H3);
146     clearbody HH;
147     rewrite > (repr_index_of ? H) in HH;
148     apply (ex_intro ? ? (repr ? H a));
149     letin GOGO ≝ (refl_eq ? (repr ? H O));
150     clearbody GOGO;
151     rewrite < HH in GOGO;
152     rewrite < HH in GOGO:(? ? % ?);
153     rewrite > (semigroup_properties G) in GOGO;
154     letin GaGa ≝ (H1 ? ? ? GOGO);
155     clearbody GaGa;
156     clear GOGO;
157     constructor 1;
158     [ unfold is_left_unit; intro;
159       letin GaxGax ≝ (refl_eq ? ((repr ? H a)·x));
160       clearbody GaxGax;
161       rewrite < GaGa in GaxGax:(? ? % ?);
162       rewrite > (semigroup_properties G) in GaxGax;
163       apply (H1 ? ? ? GaxGax)
164     | unfold is_right_unit; intro;
165       letin GaxGax ≝ (refl_eq ? (x·(repr ? H a)));
166       clearbody GaxGax;
167       rewrite < GaGa in GaxGax:(? ? % ?);
168       rewrite < (semigroup_properties G) in GaxGax;
169       apply (H2 ? ? ? GaxGax)
170   ]
171 |
172 ].