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 *)
[ 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));
| 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
]
]
].
projects / helm.git / blobdiff