First part of a slightly more interesting proof on finite (and enumerable)

groups.

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 0f759434f85fd07b48935e418cd99a35664878e7..15361b6c9a1a93ea6b498b5e57e324aedc03b04a 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -27,9 +27,27 @@ record Group : Type ≝
    opp: monoid -> monoid;
    group_properties: isGroup ? opp
  }.
- 
+
 coercion cic:/matita/algebra/groups/monoid.con.
 
+notation < "G"
+for @{ 'monoid $G }.
+
+interpretation "Monoid coercion" 'monoid G =
+ (cic:/matita/algebra/groups/monoid.con G).
+
+notation < "G"
+for @{ 'type_of_group $G }.
+
+interpretation "Type_of_group coercion" 'type_of_group G =
+ (cic:/matita/algebra/groups/Type_of_Group.con G).
+
+notation < "G"
+for @{ 'semigroup_of_group $G }.
+
+interpretation "Semigroup_of_group coercion" 'semigroup_of_group G =
+ (cic:/matita/algebra/groups/SemiGroup_of_Group.con G).
+
 notation "hvbox(x \sup (-1))" with precedence 89
 for @{ 'gopp $x }.
 
@@ -76,25 +94,79 @@ rewrite > H;
 reflexivity.
 qed.
 
-(*
-record enumerable (T:Type) : Type ≝
+
+record finite_enumerable (T:Type) : Type ≝
  { order: nat;
    repr: nat → T;
-   repr_inj: ∀n,n'. n≤order → n'≤order → repr n ≠ repr n';
-   repr_sur: ∀x.∃n.n≤order ∧ repr n = x
+   index_of: T → nat;
+   index_of_sur: ∀x.index_of x ≤ order;
+   index_of_repr: ∀n. n≤order → index_of (repr n) = n;
+   repr_index_of: ∀x. repr (index_of x) = x
  }.
+
+notation < "hvbox(C \sub i)" with precedence 89
+for @{ 'repr $C $i }.
+
+interpretation "Finite_enumerable representation" 'repr C i =
+ (cic:/matita/algebra/groups/repr.con C _ i).
  
+notation < "hvbox(|C|)" with precedence 89
+for @{ 'card $C }.
+
+interpretation "Finite_enumerable order" 'card C =
+ (cic:/matita/algebra/groups/order.con C _).
+
+theorem repr_inj:
+ ∀T:Type. ∀H:finite_enumerable T.
+  ∀n,n'. n ≤ order ? H → n' ≤ order ? H →
+   repr ? H n = repr ? H n' → n=n'.
+intros;
+rewrite < (index_of_repr ? ? ? H1);
+rewrite > H3;
+apply index_of_repr;
+assumption.
+qed.
 
 theorem foo:
  ∀G:SemiGroup.
-  enumerable (carrier G) →
+  finite_enumerable (carrier G) →
    left_cancellable (carrier G) (op G) →
     right_cancellable (carrier G) (op G) →
-     ∃e:G. is_left_unit ? e.
+     ∃e:G. isMonoid ? e.
 intros (G H);
-unfold left_cancellable in H1;
-letin x ≝ (repr ? H O);
-letin f ≝ (λy.x·(repr ? H y));
-generalize in match (H1 x);
-intro;
-*)
\ No newline at end of file
+letin f ≝ (λn.index_of ? H ((repr ? H O)·(repr ? H n)));
+cut (∀n.n ≤ order ? H → ∃m.f m = n);
+[ letin EX ≝ (Hcut O ?);
+  [ apply le_O_n
+  | clearbody EX;
+    clear Hcut;
+    unfold f in EX;
+    elim EX;
+    letin HH ≝ (eq_f ? ? (repr ? H) ? ? H3);
+    clearbody HH;
+    rewrite > (repr_index_of ? H) in HH;
+    apply (ex_intro ? ? (repr ? H a));
+    letin GOGO ≝ (refl_eq ? (repr ? H O));
+    clearbody GOGO;
+    rewrite < HH in GOGO;
+    rewrite < HH in GOGO:(? ? % ?);
+    rewrite > (semigroup_properties G) in GOGO;
+    letin GaGa ≝ (H1 ? ? ? GOGO);
+    clearbody GaGa;
+    clear GOGO;
+    constructor 1;
+    [ unfold is_left_unit; intro;
+      letin GaxGax ≝ (refl_eq ? ((repr ? H a)·x));
+      clearbody GaxGax;
+      rewrite < GaGa in GaxGax:(? ? % ?);
+      rewrite > (semigroup_properties G) in GaxGax;
+      apply (H1 ? ? ? GaxGax)
+    | unfold is_right_unit; intro;
+      letin GaxGax ≝ (refl_eq ? (x·(repr ? H a)));
+      clearbody GaxGax;
+      rewrite < GaGa in GaxGax:(? ? % ?);
+      rewrite < (semigroup_properties G) in GaxGax;
+      apply (H2 ? ? ? GaxGax)
+  ]
+|
+].
\ No newline at end of file

diff --git a/helm/matita/library/algebra/semigroups.ma b/helm/matita/library/algebra/semigroups.ma
index 64c2d13c9670f4e66a94448fb414895a1dfaeb34..d41c416f8484e9d0ce0c0e7143dd77a29b4d7608 100644 (file)
--- a/helm/matita/library/algebra/semigroups.ma
+++ b/helm/matita/library/algebra/semigroups.ma
@@ -42,6 +42,12 @@ interpretation "Semigroup operation" 'ptimesi a b =
 interpretation "Semigroup operation" 'ptimes S a b =
  (cic:/matita/algebra/semigroups/op.con S a b). *)
 
+notation < "S"
+for @{ 'carrier $S }.
+
+interpretation "Carrier coercion" 'carrier S =
+ (cic:/matita/algebra/semigroups/carrier.con S).
+
 definition is_left_unit ≝
  λS:SemiGroup. λe:S. ∀x:S. e·x = x.