X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Falgebra%2Fgroups.ma;h=5cefa0db156a209cc9af9f26f05cf77857b87041;hb=a7063fc0997a9d9eae6c329443e67ab92c4b6a0f;hp=6deb73bd5cee4e285e4f7d87ae6e7a42b96f60d0;hpb=489ee5290cce2247291b8c5c53b98d493e7f6b99;p=helm.git

diff --git a/helm/matita/library/algebra/groups.ma b/helm/matita/library/algebra/groups.ma
index 6deb73bd5..5cefa0db1 100644
--- 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 *) 
@@ -309,30 +313,86 @@ elim n;
         [ 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') *)
+    cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+    [ 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;
-        | simplify;
-          intros;
-          reflexivity
-        ]        
-      | apply le_S;
-        assumption
+          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 H7;
+          apply le_S;
+          assumption
+        | generalize in match (H2 (S n1) (le_n ?));
+          intro;
+          generalize in match (not_lt_to_le ? ? H5);
+          intro;
+          generalize in match (transitive_le ? ? ? H8 H7);
+          intro;
+          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
+            ]
+          ] 
+        ]
       ]
-    | (* This branch proves injectivity of f' *)    
+    | intros 4;
+      unfold f';
       simplify;
-      intros 4;
       apply (ltb_elim (f (S n1)) (f x1));
       simplify;
       apply (ltb_elim (f (S n1)) (f y));
@@ -348,41 +408,74 @@ elim n;
           | 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' *)
+      | (* 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 < H9 in Hcut2;
+               unfold lt in Hcut2;
+               unfold lt in H8;
+               generalize in match (le_S_S ? ? Hcut2);
+               intro;
+               generalize in match (transitive_le ? ? ? H11 H8);
+               intros;
+               rewrite < (S_pred (f x1)) in H12;
+                [ elim (not_le_Sn_n ? H12)
+                | fold simplify ((f (S n1)) < (f x1)) in H8;
+                 apply (ltn_to_ltO ? ? H8)
+                ]
+             | apply not_eq_to_le_to_lt;
+               [ assumption
+               | apply not_lt_to_le;
+                 assumption
+               ]
+             ]
+           | unfold Not;
+             intro;
+             apply H10;
+             apply (H1 ? ? ? ? H11);
+             [ 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 ? ? H9);
+         intro;
+         rewrite < S_pred in H10;
+         [ rewrite < H10 in H7;
+           generalize in match (not_lt_to_le ? ? H8);
+           intro;
+           unfold lt in H7;
+           generalize in match (le_S_S ? ? H11);
+           intro;
+           generalize in match (antisym_le ? ? H12 H7);
+           intro;
+           generalize in match (inj_S ? ? H13);
+           intro;
+           generalize in match (H1 ? ? ? ? H14);
+           [ 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);
         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
     ]
   ]
 ].