X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;h=04a00c6f7e4184805e92a2263fd19d8fc4101550;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=bec57fb4c2ca845a9d49bcd511c74b15a44e81bb;hpb=1db3c6d81f853f98f145cd9924dd18b79ca846e9;p=helm.git

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index bec57fb4c..04a00c6f7 100644
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -16,25 +16,30 @@ set "baseuri" "cic:/matita/algebra/groups/".
 
 include "algebra/monoids.ma".
 include "nat/le_arith.ma".
+include "datatypes/bool.ma".
+include "nat/compare.ma".
 
-record isGroup (M:Monoid) (opp: M -> M) : Prop ≝
- { opp_is_left_inverse: is_left_inverse M opp;
-   opp_is_right_inverse: is_right_inverse M opp
+record PreGroup : Type ≝
+ { premonoid:> PreMonoid;
+   opp: premonoid -> premonoid
+ }.
+
+record isGroup (G:PreGroup) : Prop ≝
+ { is_monoid: isMonoid G;
+   opp_is_left_inverse: is_left_inverse (mk_Monoid ? is_monoid) (opp G);
+   opp_is_right_inverse: is_right_inverse (mk_Monoid ? is_monoid) (opp G)
  }.
  
 record Group : Type ≝
- { monoid: Monoid;
-   opp: monoid -> monoid;
-   group_properties: isGroup ? opp
+ { pregroup:> PreGroup;
+   group_properties:> isGroup pregroup
  }.
 
-coercion cic:/matita/algebra/groups/monoid.con.
-
-notation < "G"
+(*notation < "G"
 for @{ 'monoid $G }.
 
 interpretation "Monoid coercion" 'monoid G =
- (cic:/matita/algebra/groups/monoid.con G).
+ (cic:/matita/algebra/groups/monoid.con G).*)
 
 notation < "G"
 for @{ 'type_of_group $G }.
@@ -43,10 +48,10 @@ 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 }.
+for @{ 'magma_of_group $G }.
 
-interpretation "Semigroup_of_group coercion" 'semigroup_of_group G =
- (cic:/matita/algebra/groups/SemiGroup_of_Group.con G).
+interpretation "magma_of_group coercion" 'magma_of_group G =
+ (cic:/matita/algebra/groups/Magma_of_Group.con G).
 
 notation "hvbox(x \sup (-1))" with precedence 89
 for @{ 'gopp $x }.
@@ -68,11 +73,11 @@ intros;
 unfold left_cancellable;
 unfold injective;
 intros (x y z);
-rewrite < (e_is_left_unit ? ? (monoid_properties G));
-rewrite < (e_is_left_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_left_inverse ? ? (group_properties G) x);
-rewrite > (semigroup_properties G);
-rewrite > (semigroup_properties G);
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_left_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_left_inverse ? (group_properties G) x);
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite > (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
 apply eq_f;
 assumption.
 qed.
@@ -85,11 +90,11 @@ unfold right_cancellable;
 unfold injective;
 simplify;fold simplify (op G); 
 intros (x y z);
-rewrite < (e_is_right_unit ? ? (monoid_properties G));
-rewrite < (e_is_right_unit ? ? (monoid_properties G) z);
-rewrite < (opp_is_right_inverse ? ? (group_properties G) x);
-rewrite < (semigroup_properties G);
-rewrite < (semigroup_properties G);
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)));
+rewrite < (e_is_right_unit ? (is_monoid ? (group_properties G)) z);
+rewrite < (opp_is_right_inverse ? (group_properties G) x);
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
+rewrite < (associative ? (is_semi_group ? (is_monoid ? (group_properties G))));
 rewrite > H;
 reflexivity.
 qed.
@@ -112,20 +117,17 @@ 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
+notation < "hvbox(|C|)" with precedence 89
 for @{ 'card $C }.
 
 interpretation "Finite_enumerable order" 'card C =
  (cic:/matita/algebra/groups/order.con C _).
 
 record finite_enumerable_SemiGroup : Type ≝
- { semigroup: SemiGroup;
-   is_finite_enumerable: finite_enumerable semigroup
+ { semigroup:> SemiGroup;
+   is_finite_enumerable:> finite_enumerable semigroup
  }.
 
-coercion cic:/matita/algebra/groups/semigroup.con.
-coercion cic:/matita/algebra/groups/is_finite_enumerable.con.
-
 notation < "S"
 for @{ 'semigroup_of_finite_enumerable_semigroup $S }.
 
@@ -134,6 +136,14 @@ interpretation "Semigroup_of_finite_enumerable_semigroup"
 =
  (cic:/matita/algebra/groups/semigroup.con S).
 
+notation < "S"
+for @{ 'magma_of_finite_enumerable_semigroup $S }.
+
+interpretation "Magma_of_finite_enumerable_semigroup"
+ 'magma_of_finite_enumerable_semigroup S
+=
+ (cic:/matita/algebra/groups/Magma_of_finite_enumerable_SemiGroup.con S).
+ 
 notation < "S"
 for @{ 'type_of_finite_enumerable_semigroup $S }.
 
@@ -154,12 +164,409 @@ interpretation "Index_of_finite_enumerable representation"
 =
  (cic:/matita/algebra/groups/index_of.con _
   (cic:/matita/algebra/groups/is_finite_enumerable.con _) e).
- 
+
+
+(* several definitions/theorems to be moved somewhere else *)
+
+definition ltb ≝ λn,m. leb n m ∧ notb (eqb n m).
+
+theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
+intros;
+elim (le_to_or_lt_eq ? ? H1);
+[ assumption
+| elim (H H2)
+].
+qed.
+
+theorem ltb_to_Prop :
+ ∀n,m.
+  match ltb n m with
+  [ true ⇒ n < m
+  | false ⇒ n ≮ m
+  ].
+intros;
+unfold ltb;
+apply leb_elim;
+apply eqb_elim;
+intros;
+simplify;
+[ rewrite < H;
+  apply le_to_not_lt;
+  constructor 1
+| apply (not_eq_to_le_to_lt ? ? H H1)
+| rewrite < H;
+  apply le_to_not_lt;
+  constructor 1
+| apply le_to_not_lt;
+  generalize in match (not_le_to_lt ? ? H1);
+  clear H1;
+  intro;
+  apply lt_to_le;
+  assumption
+].
+qed.
+
+theorem ltb_elim: \forall n,m:nat. \forall P:bool \to Prop.
+(n < m \to (P true)) \to (n ≮ m \to (P false)) \to
+P (ltb n m).
+intros.
+cut
+(match (ltb n m) with
+[ true  \Rightarrow n < m
+| false \Rightarrow n ≮ m] \to (P (ltb n m))).
+apply Hcut.apply ltb_to_Prop.
+elim (ltb n m).
+apply ((H H2)).
+apply ((H1 H2)).
+qed.
+
+theorem Not_lt_n_n: ∀n. n ≮ n.
+intro;
+unfold Not;
+intro;
+unfold lt in H;
+apply (not_le_Sn_n ? H).
+qed.
+
+theorem eq_pred_to_eq:
+ ∀n,m. O < n → O < m → pred n = pred m → n = m.
+intros;
+generalize in match (eq_f ? ? S ? ? H2);
+intro;
+rewrite < S_pred in H3;
+rewrite < S_pred in H3;
+assumption.
+qed.
+
+theorem le_pred_to_le:
+ ∀n,m. O < m → pred n ≤ pred m \to n ≤ m.
+intros 2;
+elim n;
+[ apply le_O_n
+| simplify in H2;
+  rewrite > (S_pred m);
+  [ apply le_S_S;
+    assumption
+  | assumption
+  ]
+].
+qed.
+
+theorem le_to_le_pred:
+ ∀n,m. n ≤ m → pred n ≤ pred m.
+intros 2;
+elim n;
+[ simplify;
+  apply le_O_n
+| simplify;
+  generalize in match H1;
+  clear H1;
+  elim m;
+  [ elim (not_le_Sn_O ? H1)
+  | simplify;
+    apply le_S_S_to_le;
+    assumption
+  ]
+].
+qed.
+
+theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
+intros;
+unfold Not;
+intro;
+unfold lt in H;
+unfold lt in H1;
+generalize in match (le_S_S ? ? H);
+intro;
+generalize in match (transitive_le ? ? ? H2 H1);
+intro;
+apply (not_le_Sn_n ? H3).
+qed.
+
+theorem lt_S_S: ∀n,m. n < m → S n < S m.
+intros;
+unfold lt in H;
+apply (le_S_S ? ? H).
+qed.
+
+theorem lt_O_S: ∀n. O < S n.
+intro;
+unfold lt;
+apply le_S_S;
+apply le_O_n.
+qed.
+
+theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
+intros;
+unfold lt in H1;
+generalize in match (le_S_S_to_le ? ? H1);
+intro;
+apply cic:/matita/nat/orders/antisym_le.con;
+assumption.
+qed.
+
+theorem pigeonhole:
+ ∀n:nat.∀f:nat→nat.
+  (∀x,y.x≤n → y≤n → f x = f y → x=y) →
+  (∀m. m ≤ n → f m ≤ n) →
+   ∀x. x≤n \to ∃y.f y = x ∧ y ≤ n.
+intro;
+elim n;
+[ apply (ex_intro ? ? O);
+  split;
+  [ rewrite < (le_n_O_to_eq ? H2);
+    rewrite < (le_n_O_to_eq ? (H1 O ?));
+    [ reflexivity
+    | apply le_n
+    ]
+  | apply le_n
+  ]
+| clear n;
+  letin f' ≝
+   (λx.
+    let fSn1 ≝ f (S n1) in
+     let fx ≝ f x in
+      match ltb fSn1 fx with
+      [ true ⇒ pred fx
+      | false ⇒ fx
+      ]);
+  cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+  [ cut (∀x. x ≤ n1 → f' x ≤ n1);
+    [ apply (nat_compare_elim (f (S n1)) x);
+      [ intro;
+        elim (H f' ? ? (pred x));
+        [ simplify in H5;
+          clear Hcut;
+          clear Hcut1;
+          clear f';
+          elim H5;
+          clear H5;
+          apply (ex_intro ? ? a);
+          split;
+          [ generalize in match (eq_f ? ? S ? ? H6);
+            clear H6;
+            intro;
+            rewrite < S_pred in H5;
+            [ generalize in match H4;
+              clear H4;
+              rewrite < H5;
+              clear H5;
+              apply (ltb_elim (f (S n1)) (f a));
+              [ simplify;
+                intros;
+                rewrite < S_pred;
+                [ reflexivity
+                | apply (ltn_to_ltO ? ? H4)
+                ]
+              | simplify;
+                intros;
+                generalize in match (not_lt_to_le ? ? H4);
+                clear H4;
+                intro;
+                generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
+                intro;
+                generalize in match (H1 ? ? ? ? H4);
+                [ intro;
+                |
+                |
+                ]
+              ]
+            | apply (ltn_to_ltO ? ? H4)
+            ]
+          | apply le_S;
+            assumption
+          ]
+        | apply Hcut
+        | apply Hcut1
+        | apply le_S_S_to_le;
+          rewrite < S_pred;
+          exact H3
+        ]    
+        (* TODO: caso complicato, ma simile al terzo *) 
+      | intros;
+        apply (ex_intro ? ? (S n1));
+        split;
+        [ assumption
+        | constructor 1
+        ] 
+      | intro;
+        elim (H f' ? ? x);
+        [ simplify in H5;
+          clear Hcut;
+          clear Hcut1;
+          clear f';
+          elim H5;
+          clear H5;
+          apply (ex_intro ? ? a);
+          split;
+          [ generalize in match H4;
+            clear H4;
+            rewrite < H6;
+            clear H6;
+            apply (ltb_elim (f (S n1)) (f a));
+            [ simplify;
+              intros;
+              generalize in match (lt_S_S ? ? H5);
+              intro;
+              rewrite < S_pred in H6;
+              [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
+              | apply (ltn_to_ltO ? ? H4)
+              ]
+            | simplify;
+              intros;
+              reflexivity
+            ]        
+          | apply le_S;
+            assumption
+          ]
+        | apply Hcut    
+        | apply Hcut1
+        | rewrite > (pred_Sn n1);
+          simplify;
+          generalize in match (H2 (S n1));
+          intro;
+          generalize in match (lt_to_le_to_lt ? ? ? H4 (H5 (le_n ?)));
+          intro;
+          unfold lt in H6;
+          apply le_S_S_to_le;
+          assumption
+        ]
+      ]
+    | unfold f';
+      simplify;
+      intro;
+      apply (ltb_elim (f (S n1)) (f x1));
+      simplify;
+      intros;
+      [ generalize in match (H2 x1);
+        intro;
+        change in match n1 with (pred (S n1));
+        apply le_to_le_pred;
+        apply H6;
+        apply le_S;
+        assumption
+      | generalize in match (H2 (S n1) (le_n ?));
+        intro;
+        generalize in match (not_lt_to_le ? ? H4);
+        intro;
+        generalize in match (transitive_le ? ? ? H7 H6);
+        intro;
+        cut (f x1 ≠ f (S n1));
+        [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
+          intro;
+          unfold lt in H9;
+          generalize in match (transitive_le ? ? ? H9 H6);
+          intro;
+          apply le_S_S_to_le;
+          assumption
+        | unfold Not;
+          intro;
+          generalize in match (H1 ? ? ? ? H9);
+          [ intro;
+            rewrite > H10 in H5;
+            apply (not_le_Sn_n ? H5)
+          | apply le_S;
+            assumption
+          | apply le_n
+          ]
+        ] 
+      ]
+    ]
+  | intros 4;
+    unfold f';
+    simplify;
+    apply (ltb_elim (f (S n1)) (f x1));
+    simplify;
+    apply (ltb_elim (f (S n1)) (f y));
+    simplify;
+    intros;
+    [ cut (f x1 = f y);
+      [ apply (H1 ? ? ? ? Hcut);
+        apply le_S;
+        assumption
+      | apply eq_pred_to_eq;
+        [ apply (ltn_to_ltO ? ? H7)
+        | apply (ltn_to_ltO ? ? H6)
+        | assumption
+        ]
+      ]         
+    | (* pred (f x1) = f y absurd since y ≠ S n1 and thus f y ≠ f (S n1)
+         so that f y < f (S n1) < f x1; hence pred (f x1) = f y is absurd *)
+       cut (y < S n1);
+       [ generalize in match (lt_to_not_eq ? ? Hcut);
+         intro;
+         cut (f y ≠ f (S n1));
+         [ cut (f y < f (S n1));
+           [ rewrite < H8 in Hcut2;
+             unfold lt in Hcut2;
+             unfold lt in H7;
+             generalize in match (le_S_S ? ? Hcut2);
+             intro;
+             generalize in match (transitive_le ? ? ? H10 H7);
+             intros;
+             rewrite < (S_pred (f x1)) in H11;
+              [ elim (not_le_Sn_n ? H11)
+              | fold simplify ((f (S n1)) < (f x1)) in H7;
+                apply (ltn_to_ltO ? ? H7)
+              ]
+           | apply not_eq_to_le_to_lt;
+             [ assumption
+             | apply not_lt_to_le;
+               assumption
+             ]
+           ]
+         | unfold Not;
+           intro;
+           apply H9;
+           apply (H1 ? ? ? ? H10);
+           [ apply lt_to_le;
+             assumption
+           | constructor 1
+           ]
+         ]
+       | unfold lt;
+         apply le_S_S;
+         assumption
+       ]
+    | (* f x1 = pred (f y) absurd since it implies S (f x1) = f y and
+         f x1 ≤ f (S n1) < f y = S (f x1) so that f x1 = f (S n1); by
+         injectivity x1 = S n1 that is absurd since x1 ≤ n1 *)
+       generalize in match (eq_f ? ? S ? ? H8);
+       intro;
+       rewrite < S_pred in H9;
+       [ rewrite < H9 in H6;
+         generalize in match (not_lt_to_le ? ? H7);
+         intro;
+         unfold lt in H6;
+         generalize in match (le_S_S ? ? H10);
+         intro;
+         generalize in match (antisym_le ? ? H11 H6);
+         intro;
+         generalize in match (inj_S ? ? H12);
+         intro;
+         generalize in match (H1 ? ? ? ? H13);
+         [ intro;
+           rewrite > H14 in H4;
+           elim (not_le_Sn_n ? H4)
+         | apply le_S;
+           assumption
+         | apply le_n
+         ]
+       | apply (ltn_to_ltO ? ? H6) 
+       ]
+    | apply (H1 ? ? ? ? H8);
+      apply le_S;
+      assumption
+    ]
+  ]
+].
+qed.
+
 theorem foo:
  ∀G:finite_enumerable_SemiGroup.
   left_cancellable ? (op G) →
   right_cancellable ? (op G) →
-   ∃e:G. isMonoid G e.
+   ∃e:G. isMonoid (mk_PreMonoid G e).
 intros;
 letin f ≝ (λn.ι(G \sub O · G \sub n));
 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
@@ -178,23 +585,26 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     clearbody GOGO;
     rewrite < HH in GOGO;
     rewrite < HH in GOGO:(? ? % ?);
-    rewrite > (semigroup_properties G) in GOGO;
+    rewrite > (associative ? G) in GOGO;
     letin GaGa ≝ (H ? ? ? GOGO);
     clearbody GaGa;
     clear GOGO;
     constructor 1;
-    [ unfold is_left_unit; intro;
+    [ simplify;
+      apply (semigroup_properties G)
+    | unfold is_left_unit; intro;
       letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
-      rewrite > (semigroup_properties G) in GaxGax;
+      rewrite > (associative ? (semigroup_properties G)) in GaxGax;
       apply (H ? ? ? GaxGax)
     | unfold is_right_unit; intro;
       letin GaxGax ≝ (refl_eq ? (x·G \sub a));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
-      rewrite < (semigroup_properties G) in GaxGax;
+      rewrite < (associative ? (semigroup_properties G)) in GaxGax;
       apply (H1 ? ? ? GaxGax)
+    ]
   ]
-|
-].
\ No newline at end of file
+| apply pigeonhole
+].