Closer to the proof of the pigeonhole principle... that is already in the

[helm.git] / helm / matita / library / algebra / groups.ma

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 4fcca34993cd060e7a473e3a211e0f3c2e2935f7..5cefa0db156a209cc9af9f26f05cf77857b87041 100644 (file)
--- a/helm/matita/library/algebra/groups.ma
+++ b/helm/matita/library/algebra/groups.ma
@@ -282,15 +282,19 @@ qed.
 theorem pigeonhole:
  ∀n:nat.∀f:nat→nat.
   (∀x,y.x≤n → y≤n → f x = f y → x=y) →
-  (∀m. f m ≤ n) →
+  (∀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
+  [ rewrite < (le_n_O_to_eq ? H2);
+    rewrite < (le_n_O_to_eq ? (H1 O ?));
+    [ reflexivity
+    | apply le_n
+    ]
+  | apply le_n
+  ]
 | clear n;
   apply (nat_compare_elim (f (S n1)) x);
   [ (* TODO: caso complicato, ma simile al terzo *) 
@@ -310,56 +314,81 @@ elim n;
         | false ⇒ fx
         ]);
     cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
-    [ elim (H f' ? ? x);
-      [ simplify in H5;
-        clear Hcut;
-        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;
+    [ cut (∀x. x ≤ n1 → f' x ≤ n1);
+      [ 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));
+            [ (* TODO: caso impossibile (uso l'iniettivita') *)
+              simplify;
+            | 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
         ]
-      | apply Hcut    
-      | simplify;
-        intro;
-        apply (ltb_elim (f (S n1)) (f m));
+      | unfold f';
         simplify;
         intro;
-        [ generalize in match (H2 m);
+        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 H7;
+          apply le_S;
           assumption
-        | generalize in match (H2 (S n1));
+        | generalize in match (H2 (S n1) (le_n ?));
           intro;
           generalize in match (not_lt_to_le ? ? H5);
           intro;
-          generalize in match (transitive_le ? ? ? H7 H6);
+          generalize in match (transitive_le ? ? ? H8 H7);
           intro;
-          (* TODO: qui mi serve dimostrare che f m ≠ f (S n1) (per iniettivita'?) *) 
+          cut (f x1 ≠ f (S n1));
+          [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H8);
+            intro;
+            unfold lt in H10;
+            generalize in match (transitive_le ? ? ? H10 H7);
+            intro;
+            apply le_S_S_to_le;
+            assumption
+          | unfold Not;
+            intro;
+            generalize in match (H1 ? ? ? ? H10);
+            [ intro;
+              rewrite > H11 in H6;
+              apply (not_le_Sn_n ? H6)
+            | apply le_S;
+              assumption
+            | apply le_n
+            ]
+          ] 
         ]
-      | 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
       ]
     | intros 4;
       unfold f';
@@ -434,9 +463,13 @@ elim n;
            generalize in match (inj_S ? ? H13);
            intro;
            generalize in match (H1 ? ? ? ? H14);
-           intro;
-           rewrite > H15 in H5;
-           elim (not_le_Sn_n ? H5)
+           [ intro;
+             rewrite > H15 in H5;
+             elim (not_le_Sn_n ? H5)
+           | apply le_S;
+             assumption
+           | apply le_n
+           ]
          | apply (ltn_to_ltO ?? H7) 
          ]
       | apply (H1 ? ? ? ? H9);