Some more progress in the proof of the (ad-hoc ?) pigeonhole principle.

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index ae6b525e3906d9b6f5b153b0c767ed6c47faed08..6deb73bd5cee4e285e4f7d87ae6e7a42b96f60d0 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/algebra/groups/".
 
 include "algebra/monoids.ma".
 include "nat/le_arith.ma".
+include "datatypes/bool.ma".
+include "nat/compare.ma".
 
 record PreGroup : Type ≝
  { premonoid:> PreMonoid;
@@ -115,7 +117,7 @@ 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 =
@@ -162,7 +164,230 @@ 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 2;
+elim n;
+[ elim (Not_lt_n_n ? H)
+| generalize in match H3;
+  clear H3;
+  generalize in match H2;
+  clear H2;
+  elim m;
+  [ elim (Not_lt_n_n ? H2)
+  | simplify in H4;
+    apply (eq_f ? ? S);
+    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 pigeonhole:
+ ∀n:nat.∀f:nat→nat.
+  (∀x,y.x≤n → y≤n → f x = f y → x=y) →
+  (∀m. 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
+| clear n;
+  apply (nat_compare_elim (f (S n1)) x);
+  [ (* TODO: caso complicato, ma simile al terzo *) 
+  | intros;
+    apply (ex_intro ? ? (S n1));
+    split;
+    [ assumption
+    | constructor 1
+    ] 
+  | intro;
+    letin f' ≝
+     (λx.
+       let fSn1 ≝ f (S n1) in
+       let fx ≝ f x in
+        match ltb fSn1 fx with
+        [ true ⇒ pred fx
+        | false ⇒ fx
+        ]);
+    elim (H f' ? ? x);
+    [ simplify in H5;
+      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));
+        [ (* TODO: caso impossibile (uso l'iniettivita') *)
+          simplify;
+        | simplify;
+          intros;
+          reflexivity
+        ]        
+      | apply le_S;
+        assumption
+      ]
+    | (* This branch proves injectivity of f' *)    
+      simplify;
+      intros 4;
+      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 ? ? H8)
+          | apply (ltn_to_ltO ? ? H7)
+          | assumption
+          ]
+        ]         
+      | (* TODO: pred (f x1) = f y assurdo per iniettivita'
+           poiche' y ≠ S n1 da cui f y ≠ f (S n1) da cui f y < f (S n1) < f x1
+           da cui assurdo pred (f x1) = f y *)
+      | (* TODO: f x1 = pred (f y) assurdo per iniettivita' *)
+      | apply (H1 ? ? ? ? H9);
+        apply le_S;
+        assumption
+      ]
+    | simplify;
+      intro;
+      apply (ltb_elim (f (S n1)) (f m));
+      simplify;
+      intro;
+      [ generalize in match (H2 m);
+        intro;
+        change in match n1 with (pred (S n1));
+        apply le_to_le_pred;
+        assumption
+      | generalize in match (H2 (S n1));
+        intro;
+        generalize in match (not_lt_to_le ? ? H5);
+        intro;
+        generalize in match (transitive_le ? ? ? H7 H6);
+        intro;
+        (* TODO: qui mi serve dimostrare che f m ≠ f (S n1) (per iniettivita'?) *) 
+      ]
+    | rewrite > (pred_Sn n1);
+      simplify;
+      generalize in match (H2 (S n1));
+      intro;
+      generalize in match (lt_to_le_to_lt ? ? ? H4 H5);
+      intro;
+      unfold lt in H6;
+      apply le_S_S_to_le;
+      assumption
+    ]
+  ]
+].
+qed.
+
 theorem foo:
  ∀G:finite_enumerable_SemiGroup.
   left_cancellable ? (op G) →
@@ -207,5 +432,5 @@ cut (∀n.n ≤ order ? (is_finite_enumerable G) → ∃m.f m = n);
       apply (H1 ? ? ? GaxGax)
     ]
   ]
-|
+| apply pigeonhole
 ].