X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Falgebra%2Ffinite_groups.ma;h=8dfa31342e468a2a45676217e7cbf93e3b3101c1;hb=6d297b12c480352eb2f156ab4515f73921ea2e81;hp=2078cf1d75cccc151280cc54877f25d1e41156e9;hpb=7815a9150b5581f60e49ad6520f46ac287e073fa;p=helm.git

diff --git a/helm/software/matita/library/algebra/finite_groups.ma b/helm/software/matita/library/algebra/finite_groups.ma
index 2078cf1d7..8dfa31342 100644
--- a/helm/software/matita/library/algebra/finite_groups.ma
+++ b/helm/software/matita/library/algebra/finite_groups.ma
@@ -12,11 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/algebra/finite_groups/".
-
 include "algebra/groups.ma".
 
-record finite_enumerable (T:Type) : Type ≝
+record finite_enumerable (T:Type) : Type≝
  { order: nat;
    repr: nat → T;
    index_of: T → nat;
@@ -33,13 +31,10 @@ for @{ 'repr $C $i }.
 interpretation "Finite_enumerable representation" 'repr C i =
  (cic:/matita/algebra/finite_groups/repr.con C _ i).*)
  
-notation < "hvbox(|C|)" with precedence 89
-for @{ 'card $C }.
-
 interpretation "Finite_enumerable order" 'card C =
  (cic:/matita/algebra/finite_groups/order.con C _).
 
-record finite_enumerable_SemiGroup : Type ≝
+record finite_enumerable_SemiGroup : Type≝
  { semigroup:> SemiGroup;
    is_finite_enumerable:> finite_enumerable semigroup
  }.
@@ -48,7 +43,7 @@ interpretation "Finite_enumerable representation" 'repr S i =
  (cic:/matita/algebra/finite_groups/repr.con S
   (cic:/matita/algebra/finite_groups/is_finite_enumerable.con S) i).
 
-notation "hvbox(ι e)" with precedence 60
+notation "hvbox(\iota e)" with precedence 60
 for @{ 'index_of_finite_enumerable_semigroup $e }.
 
 interpretation "Index_of_finite_enumerable representation"
@@ -60,143 +55,6 @@ interpretation "Index_of_finite_enumerable representation"
 
 (* 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: ∀n,m:nat. ∀P:bool → Prop.
-(n < m → (P true)) → (n ≮ m → (P false)) →
-P (ltb n m).
-intros.
-cut
-(match (ltb n m) with
-[ true  ⇒ n < m
-| false ⇒ n ≮ m] → (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 → 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) →
@@ -216,8 +74,8 @@ elim n;
 | clear n;
   letin f' ≝
    (λx.
-    let fSn1 ≝ f (S n1) in
-     let fx ≝ f x in
+    let fSn1 ≝f (S n1) in
+     let fx ≝f x in
       match ltb fSn1 fx with
       [ true ⇒ pred fx
       | false ⇒ fx
@@ -230,6 +88,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -298,6 +157,7 @@ elim n;
         [ simplify in H5;
           clear Hcut;
           clear Hcut1;
+          unfold f' in H5;
           clear f';
           elim H5;
           clear H5;
@@ -310,7 +170,7 @@ elim n;
             apply (ltb_elim (f (S n1)) (f a));
             [ simplify;
               intros;
-              generalize in match (lt_S_S ? ? H5);
+              generalize in match (lt_to_lt_S_S ? ? H5);
               intro;
               rewrite < S_pred in H6;
               [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
@@ -388,7 +248,8 @@ elim n;
       [ apply (H1 ? ? ? ? Hcut);
         apply le_S;
         assumption
-      | apply eq_pred_to_eq;
+      | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
+apply eq_pred_to_eq;
         [ apply (ltn_to_ltO ? ? H7)
         | apply (ltn_to_ltO ? ? H6)
         | assumption
@@ -465,45 +326,45 @@ elim n;
   ]
 ].
 qed.
-
+(* demo *)
 theorem finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid:
  ∀G:finite_enumerable_SemiGroup.
   left_cancellable ? (op G) →
   right_cancellable ? (op G) →
    ∃e:G. isMonoid (mk_PreMonoid G e).
 intros;
-letin f ≝ (λn.ι(G \sub O · G \sub n));
+letin f ≝(λn.ι(G \sub O · G \sub n));
 cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
-[ letin EX ≝ (Hcut O ?);
+[ letin EX ≝(Hcut O ?);
   [ apply le_O_n
   | clearbody EX;
     clear Hcut;
     unfold f in EX;
     elim EX;
     clear EX;
-    letin HH ≝ (eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
+    letin HH ≝(eq_f ? ? (repr ? (is_finite_enumerable G)) ? ? H2);
     clearbody HH;
     rewrite > (repr_index_of ? (is_finite_enumerable G)) in HH;
     apply (ex_intro ? ? (G \sub a));
-    letin GOGO ≝ (refl_eq ? (repr ? (is_finite_enumerable G) O));
+    letin GOGO ≝(refl_eq ? (repr ? (is_finite_enumerable G) O));
     clearbody GOGO;
     rewrite < HH in GOGO;
     rewrite < HH in GOGO:(? ? % ?);
     rewrite > (op_associative ? G) in GOGO;
-    letin GaGa ≝ (H ? ? ? GOGO);
+    letin GaGa ≝(H ? ? ? GOGO);
     clearbody GaGa;
     clear GOGO;
     constructor 1;
     [ simplify;
       apply (semigroup_properties G)
     | unfold is_left_unit; intro;
-      letin GaxGax ≝ (refl_eq ? (G \sub a ·x));
-      clearbody GaxGax;
+      letin GaxGax ≝(refl_eq ? (G \sub a ·x));
+      clearbody GaxGax; (* demo *)
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite > (op_associative ? (semigroup_properties G)) in GaxGax;
       apply (H ? ? ? GaxGax)
     | unfold is_right_unit; intro;
-      letin GaxGax ≝ (refl_eq ? (x·G \sub a));
+      letin GaxGax ≝(refl_eq ? (x·G \sub a));
       clearbody GaxGax;
       rewrite < GaGa in GaxGax:(? ? % ?);
       rewrite < (op_associative ? (semigroup_properties G)) in GaxGax;
@@ -516,7 +377,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
     elim H3;
     assumption
   | intros;
-    change in H5 with (ι(G \sub O · G \sub x) = ι(G \sub O · G \sub y));
+    simplify in H5;
     cut (G \sub (ι(G \sub O · G \sub x)) = G \sub (ι(G \sub O · G \sub y)));
     [ rewrite > (repr_index_of ? ? (G \sub O · G \sub x))  in Hcut;
       rewrite > (repr_index_of ? ? (G \sub O · G \sub y))  in Hcut;
@@ -531,6 +392,7 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
       assumption
     ]
   | intros;
+    unfold f;
     apply index_of_sur
   ] 
 ].