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
- ]
-].
+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:
].
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.
| apply le_n
]
| 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
- ]);
- cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
- [ cut (∀x. x ≤ n1 → f' x ≤ n1);
- [ elim (H f' ? ? x);
+ letin f' ≝
+ (λx.
+ let fSn1 ≝ f (S n1) in
+ let fx ≝ f x in
+ match ltb fSn1 fx with
+ [ true ⇒ pred fx
+ | false ⇒ fx
+ ]);
+ cut (∀x,y. x ≤ n1 → y ≤ n1 → f' x = f' y → x=y);
+ [ cut (∀x. x ≤ n1 → f' x ≤ n1);
+ [ apply (nat_compare_elim (f (S n1)) x);
+ [ intro;
+ elim (H f' ? ? (pred x));
+ [ simplify in H5;
+ clear Hcut;
+ clear Hcut1;
+ clear f';
+ elim H5;
+ clear H5;
+ apply (ex_intro ? ? a);
+ split;
+ [ generalize in match (eq_f ? ? S ? ? H6);
+ clear H6;
+ intro;
+ rewrite < S_pred in H5;
+ [ generalize in match H4;
+ clear H4;
+ rewrite < H5;
+ clear H5;
+ apply (ltb_elim (f (S n1)) (f a));
+ [ simplify;
+ intros;
+ rewrite < S_pred;
+ [ reflexivity
+ | apply (ltn_to_ltO ? ? H4)
+ ]
+ | simplify;
+ intros;
+ generalize in match (not_lt_to_le ? ? H4);
+ clear H4;
+ intro;
+ generalize in match (le_n_m_to_lt_m_Sn_to_eq_n_m ? ? H6 H5);
+ intro;
+ generalize in match (H1 ? ? ? ? H4);
+ [ intro;
+ |
+ |
+ ]
+ ]
+ | apply (ltn_to_ltO ? ? H4)
+ ]
+ | apply le_S;
+ assumption
+ ]
+ | apply Hcut
+ | apply Hcut1
+ | apply le_S_S_to_le;
+ rewrite < S_pred;
+ exact H3
+ ]
+ (* TODO: caso complicato, ma simile al terzo *)
+ | intros;
+ apply (ex_intro ? ? (S n1));
+ split;
+ [ assumption
+ | constructor 1
+ ]
+ | intro;
+ elim (H f' ? ? x);
[ simplify in H5;
clear Hcut;
clear Hcut1;
rewrite < H6;
clear H6;
apply (ltb_elim (f (S n1)) (f a));
- [ (* TODO: caso impossibile (uso l'iniettivita') *)
- simplify;
+ [ simplify;
+ intros;
+ generalize in match (lt_S_S ? ? H5);
+ intro;
+ rewrite < S_pred in H6;
+ [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
+ | apply (ltn_to_ltO ? ? H4)
+ ]
| simplify;
intros;
reflexivity
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
- ]
- ]
- ]
]
- | intros 4;
- unfold f';
+ | unfold f';
simplify;
+ intro;
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;
+ [ generalize in match (H2 x1);
+ intro;
+ change in match n1 with (pred (S n1));
+ apply le_to_le_pred;
+ apply H6;
+ apply le_S;
+ assumption
+ | generalize in match (H2 (S n1) (le_n ?));
+ intro;
+ generalize in match (not_lt_to_le ? ? H4);
+ intro;
+ generalize in match (transitive_le ? ? ? H7 H6);
+ intro;
+ cut (f x1 ≠ f (S n1));
+ [ generalize in match (not_eq_to_le_to_lt ? ? Hcut1 H7);
+ intro;
+ unfold lt in H9;
+ generalize in match (transitive_le ? ? ? H9 H6);
+ intro;
+ apply le_S_S_to_le;
assumption
- | apply eq_pred_to_eq;
- [ apply (ltn_to_ltO ? ? H8)
- | apply (ltn_to_ltO ? ? H7)
- | assumption
+ | unfold Not;
+ intro;
+ generalize in match (H1 ? ? ? ? H9);
+ [ intro;
+ rewrite > H10 in H5;
+ apply (not_le_Sn_n ? H5)
+ | apply le_S;
+ assumption
+ | apply le_n
]
- ]
- | (* 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;
+ ]
+ ]
+ ]
+ | intros 4;
+ unfold f';
+ simplify;
+ 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 ? ? H7)
+ | apply (ltn_to_ltO ? ? H6)
+ | assumption
+ ]
+ ]
+ | (* 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 < H8 in Hcut2;
+ unfold lt in Hcut2;
+ unfold lt in H7;
+ generalize in match (le_S_S ? ? Hcut2);
intro;
- apply H10;
- apply (H1 ? ? ? ? H11);
- [ apply lt_to_le;
+ generalize in match (transitive_le ? ? ? H10 H7);
+ intros;
+ rewrite < (S_pred (f x1)) in H11;
+ [ elim (not_le_Sn_n ? H11)
+ | fold simplify ((f (S n1)) < (f x1)) in H7;
+ apply (ltn_to_ltO ? ? H7)
+ ]
+ | apply not_eq_to_le_to_lt;
+ [ assumption
+ | apply not_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);
+ | unfold Not;
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;
+ apply H9;
+ apply (H1 ? ? ? ? H10);
+ [ apply lt_to_le;
assumption
- | apply le_n
+ | constructor 1
]
- | apply (ltn_to_ltO ?? H7)
]
- | apply (H1 ? ? ? ? H9);
- apply le_S;
- assumption
- ]
+ | 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 ? ? H8);
+ intro;
+ rewrite < S_pred in H9;
+ [ rewrite < H9 in H6;
+ generalize in match (not_lt_to_le ? ? H7);
+ intro;
+ unfold lt in H6;
+ generalize in match (le_S_S ? ? H10);
+ intro;
+ generalize in match (antisym_le ? ? H11 H6);
+ intro;
+ generalize in match (inj_S ? ? H12);
+ intro;
+ generalize in match (H1 ? ? ? ? H13);
+ [ intro;
+ rewrite > H14 in H4;
+ elim (not_le_Sn_n ? H4)
+ | apply le_S;
+ assumption
+ | apply le_n
+ ]
+ | apply (ltn_to_ltO ? ? H6)
+ ]
+ | apply (H1 ? ? ? ? H8);
+ apply le_S;
+ assumption
]
]
].
projects / helm.git / blobdiff