From 03d30a78581b24842e1f425b41861e5ae8f912b5 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Tue, 13 Mar 2007 10:58:06 +0000 Subject: [PATCH] Few theorems added.` --- matita/library/nat/compare.ma | 60 +++++++++++++++++++++++++------ matita/library/nat/div_and_mod.ma | 4 +-- matita/library/nat/le_arith.ma | 5 +++ matita/library/nat/minus.ma | 51 ++++++++++++++++++++++++++ matita/library/nat/nat.ma | 2 +- matita/library/nat/orders.ma | 24 +++++++++---- matita/library/nat/plus.ma | 5 +++ 7 files changed, 130 insertions(+), 21 deletions(-) diff --git a/matita/library/nat/compare.ma b/matita/library/nat/compare.ma index 264731580..c701cd2e7 100644 --- a/matita/library/nat/compare.ma +++ b/matita/library/nat/compare.ma @@ -112,23 +112,60 @@ match n with match m with [ O \Rightarrow false | (S q) \Rightarrow leb p q]]. - + +theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. +(n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to +P (leb n m). +apply nat_elim2; intros; simplify + [apply H.apply le_O_n + |apply H1.apply not_le_Sn_O. + |apply H;intros + [apply H1.apply le_S_S.assumption. + |apply H2.unfold Not.intros.apply H3.apply le_S_S_to_le.assumption + ] + ] +qed. + +(* +theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. +intros. +apply (leb_elim n m) + [intro.left.assumption + |intro.right.assumption + ] +qed. +*) + +theorem le_to_leb_true: \forall n,m. n \leq m \to leb n m = true. +intros.apply leb_elim;intros + [reflexivity + |apply False_ind.apply H1.apply H. + ] +qed. + +theorem lt_to_leb_false: \forall n,m. m < n \to leb n m = false. +intros.apply leb_elim;intros + [apply False_ind.apply (le_to_not_lt ? ? H1). assumption + |reflexivity + ] +qed. + theorem leb_to_Prop: \forall n,m:nat. match (leb n m) with [ true \Rightarrow n \leq m | false \Rightarrow n \nleq m]. -intros. -apply (nat_elim2 -(\lambda n,m:nat.match (leb n m) with -[ true \Rightarrow n \leq m -| false \Rightarrow n \nleq m])). -simplify.exact le_O_n. -simplify.exact not_le_Sn_O. -intros 2.simplify.elim ((leb n1 m1)). -simplify.apply le_S_S.apply H. -simplify.unfold Not.intros.apply H.apply le_S_S_to_le.assumption. +apply nat_elim2;simplify + [exact le_O_n + |exact not_le_Sn_O + |intros 2.simplify. + elim ((leb n m));simplify + [apply le_S_S.apply H + |unfold Not.intros.apply H.apply le_S_S_to_le.assumption + ] + ] qed. +(* theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop. (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to P (leb n m). @@ -142,6 +179,7 @@ elim (leb n m). apply ((H H2)). apply ((H1 H2)). qed. +*) let rec nat_compare n m: compare \def match n with diff --git a/matita/library/nat/div_and_mod.ma b/matita/library/nat/div_and_mod.ma index 73ff78998..ccddcca3f 100644 --- a/matita/library/nat/div_and_mod.ma +++ b/matita/library/nat/div_and_mod.ma @@ -28,7 +28,7 @@ match (leb m n) with definition mod : nat \to nat \to nat \def \lambda n,m. match m with -[O \Rightarrow m +[O \Rightarrow n | (S p) \Rightarrow mod_aux n n p]. interpretation "natural remainder" 'module x y = @@ -143,7 +143,7 @@ rewrite > distr_times_minus. rewrite > plus_minus. rewrite > sym_times. rewrite < H5. -rewrite < sym_times. +rewrite < sym_times. apply plus_to_minus. apply H3. apply le_times_r. diff --git a/matita/library/nat/le_arith.ma b/matita/library/nat/le_arith.ma index a76183063..ae386d313 100644 --- a/matita/library/nat/le_arith.ma +++ b/matita/library/nat/le_arith.ma @@ -51,6 +51,11 @@ intros.change with (O+m \le n+m). apply le_plus_l.apply le_O_n. qed. +theorem le_plus_n_r :\forall n,m:nat. m \le m + n. +intros.rewrite > sym_plus. +apply le_plus_n. +qed. + theorem eq_plus_to_le: \forall n,m,p:nat.n=m+p \to m \le n. intros.rewrite > H. rewrite < sym_plus. diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma index 710418d72..71c2cc205 100644 --- a/matita/library/nat/minus.ma +++ b/matita/library/nat/minus.ma @@ -57,6 +57,14 @@ intros.rewrite < H.reflexivity. apply le_S_S_to_le. assumption. qed. +theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m). +apply nat_elim2 + [intro.reflexivity + |intro.simplify.auto + |intros.simplify.assumption + ] +qed. + theorem plus_minus: \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m. intros 2. @@ -226,6 +234,49 @@ rewrite > plus_n_Sm.assumption. qed. (* minus and lt - to be completed *) +theorem lt_minus_l: \forall m,l,n:nat. + l < m \to m \le n \to n - m < n - l. +apply nat_elim2 + [intros.apply False_ind.apply (not_le_Sn_O ? H) + |intros.rewrite < minus_n_O. + auto + |intros. + generalize in match H2. + apply (nat_case n1) + [intros.apply False_ind.apply (not_le_Sn_O ? H3) + |intros.simplify. + apply H + [ + apply lt_S_S_to_lt. + assumption + |apply le_S_S_to_le.assumption + ] + ] + ] +qed. + +theorem lt_minus_r: \forall n,m,l:nat. + n \le l \to l < m \to l -n < m -n. +intro.elim n + [applyS H1 + |rewrite > eq_minus_S_pred. + rewrite > eq_minus_S_pred. + apply lt_pred + [unfold lt.apply le_plus_to_minus_r.applyS H1 + |apply H[auto|assumption] + ] + ] +qed. + +lemma lt_to_lt_O_minus : \forall m,n. + n < m \to O < m - n. +intros. +unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus. +rewrite < plus_n_Sm. +rewrite < plus_n_O. +assumption. +qed. + theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p). intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))). intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption. diff --git a/matita/library/nat/nat.ma b/matita/library/nat/nat.ma index b600072c6..b54bc76a9 100644 --- a/matita/library/nat/nat.ma +++ b/matita/library/nat/nat.ma @@ -26,7 +26,7 @@ definition pred: nat \to nat \def | (S p) \Rightarrow p ]. theorem pred_Sn : \forall n:nat.n=(pred (S n)). - intros. reflexivity. + intros. simplify. reflexivity. qed. theorem injective_S : injective nat nat S. diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma index 807906bd2..8c6ce942e 100644 --- a/matita/library/nat/orders.ma +++ b/matita/library/nat/orders.ma @@ -22,9 +22,8 @@ inductive le (n:nat) : nat \to Prop \def | le_n : le n n | le_S : \forall m:nat. le n m \to le n (S m). -(*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y). -(*CSC: the URI must disappear: there is a bug now *) + interpretation "natural 'neither less nor equal to'" 'nleq x y = (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)). @@ -32,24 +31,21 @@ interpretation "natural 'neither less nor equal to'" 'nleq x y = definition lt: nat \to nat \to Prop \def \lambda n,m:nat.(S n) \leq m. -(*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y). -(*CSC: the URI must disappear: there is a bug now *) + interpretation "natural 'not less than'" 'nless x y = (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)). definition ge: nat \to nat \to Prop \def \lambda n,m:nat.m \leq n. -(*CSC: the URI must disappear: there is a bug now *) interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y). definition gt: nat \to nat \to Prop \def \lambda n,m:nat.m plus_n_O. +apply plus_n_Sm. +qed. + theorem sym_plus: \forall n,m:nat. n+m = m+n. intros.elim n. simplify.apply plus_n_O. -- 2.39.2