From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 09:45:13 +0000 (+0000) Subject: Committing all the recent development of Andrea after the merge between his X-Git-Tag: V_0_7_2~28 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7bbce6bc163892cfd99cfcda65db42001b86789f;p=helm.git Committing all the recent development of Andrea after the merge between his commits and my recent commits (that added notation here and there). --- diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma index 1352988df..7e4b10e00 100644 --- a/helm/matita/library/Z/times.ma +++ b/helm/matita/library/Z/times.ma @@ -1,5 +1,5 @@ (**************************************************************************) -(* ___ *) +(* __ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) @@ -14,6 +14,7 @@ set "baseuri" "cic:/matita/Z/times". +include "nat/lt_arith.ma". include "Z/z.ma". definition Ztimes :Z \to Z \to Z \def @@ -41,20 +42,18 @@ simplify.reflexivity. simplify.reflexivity. qed. -(*CSC: da qui in avanti niente notazione *) -(* theorem symmetric_Ztimes : symmetric Z Ztimes. change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x). intros.elim x.rewrite > Ztimes_z_OZ.reflexivity. elim y.simplify.reflexivity. -change with eq Z (pos (pred (times (S e1) (S e)))) (pos (pred (times (S e) (S e1)))). +change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))). rewrite < sym_times.reflexivity. -change with eq Z (neg (pred (times (S e1) (S e2)))) (neg (pred (times (S e2) (S e1)))). +change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))). rewrite < sym_times.reflexivity. elim y.simplify.reflexivity. -change with eq Z (neg (pred (times (S e2) (S e1)))) (neg (pred (times (S e1) (S e2)))). +change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))). rewrite < sym_times.reflexivity. -change with eq Z (pos (pred (times (S e2) (S e)))) (pos (pred (times (S e) (S e2)))). +change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))). rewrite < sym_times.reflexivity. qed. @@ -68,190 +67,161 @@ elim x.simplify.reflexivity. elim y.simplify.reflexivity. elim z.simplify.reflexivity. change with -eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2)))) - (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))). -rewrite < S_pred_S. - -theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z). -intros.elim z. -simplify.reflexivity. -simplify.reflexivity. -elim e2.simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z). -intros.elim z. -simplify.reflexivity. -elim e1.simplify.reflexivity. -simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zplus_pos_pos: -\forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))). -intros. -elim n.elim m. -simplify.reflexivity. -simplify.reflexivity. -elim m. +eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S. +apply lt_O_times_S_S. +change with +eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S.apply lt_O_times_S_S. +elim z.simplify.reflexivity. +change with +eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S.apply lt_O_times_S_S. +change with +eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S. +apply lt_O_times_S_S. +elim y.simplify.reflexivity. +elim z.simplify.reflexivity. +change with +eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S. +apply lt_O_times_S_S. +change with +eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S.apply lt_O_times_S_S. +elim z.simplify.reflexivity. +change with +eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S.apply lt_O_times_S_S. +change with +eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2)))) + (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))). +rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity. +apply lt_O_times_S_S. +apply lt_O_times_S_S. +qed. + +variant assoc_Ztimes : \forall x,y,z:Z. +eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def +associative_Ztimes. + + +theorem distributive_Ztimes: distributive Z Ztimes Zplus. +change with \forall x,y,z:Z. +eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)). +intros.elim x. +simplify.reflexivity. +(* case x = neg n *) +elim y.reflexivity. +elim z.reflexivity. +change with +eq Z (pos (pred (times (S n) (plus (S n1) (S n2))))) + (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))). +rewrite < times_plus_distr.reflexivity. +simplify. (* problemi di naming su n *) +(* sintassi della change ??? *) +cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))). +rewrite > Hcut. +rewrite > Hcut. +rewrite < nat_compare_pred_pred ? ? ? ?. +rewrite < nat_compare_times_l. +rewrite < nat_compare_S_S. +apply nat_compare_elim n1 n2. +intro. +(* per ricavare questo change ci ho messo un'ora; +LA GESTIONE DELLA RIDUZIONE NON VA *) +change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n2) (S n1))))))) + (neg (pred (minus (pred (times (S n) (S n2))) + (pred (times (S n) (S n1))))))). +rewrite < S_pred ? ?. +rewrite > minus_pred_pred ? ? ? ?. +rewrite < distr_times_minus. +reflexivity. +(* we start closing stupid positivity conditions *) +apply lt_O_times_S_S. +apply lt_O_times_S_S. simplify. -rewrite < plus_n_O.reflexivity. +apply le_SO_minus. exact H. +intro.rewrite < H.simplify.reflexivity. +intro. +change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n1) (S n2))))))) + (pos (pred (minus (pred (times (S n) (S n1))) + (pred (times (S n) (S n2))))))). +rewrite < S_pred ? ?. +rewrite > minus_pred_pred ? ? ? ?. +rewrite < distr_times_minus. +reflexivity. +(* we start closing stupid positivity conditions *) +apply lt_O_times_S_S. +apply lt_O_times_S_S. simplify. -rewrite < plus_n_Sm.reflexivity. -qed. - -theorem Zplus_pos_neg: -\forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))). -intros.reflexivity. -qed. - -theorem Zplus_neg_pos : -\forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))). -intros. -elim n.elim m. -simplify.reflexivity. -simplify.reflexivity. -elim m. -simplify.reflexivity. -simplify.reflexivity. -qed. - -theorem Zplus_neg_neg: -\forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))). -intros. -elim n.elim m. -simplify.reflexivity. -simplify.reflexivity. -elim m. -simplify.rewrite < plus_n_Sm.reflexivity. -simplify.rewrite > plus_n_Sm.reflexivity. -qed. - -theorem Zplus_Zsucc_Zpred: -\forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)). -intros. -elim x. elim y. -simplify.reflexivity. -simplify.reflexivity. -rewrite < Zsucc_Zplus_pos_O. -rewrite > Zsucc_Zpred.reflexivity. -elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ). -rewrite < Zpred_Zplus_neg_O. -rewrite > Zpred_Zsucc. -simplify.reflexivity. -rewrite < Zplus_neg_neg.reflexivity. -apply Zplus_neg_pos. -elim y.simplify.reflexivity. -apply Zplus_pos_neg. -apply Zplus_pos_pos. -qed. - -theorem Zplus_Zsucc_pos_pos : -\forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))). +apply le_SO_minus. exact H. +(* questi non so neppure da dove vengano *) +apply lt_O_times_S_S. +apply lt_O_times_S_S. +(* adesso chiudo il cut stupido *) intros.reflexivity. -qed. - -theorem Zplus_Zsucc_pos_neg: -\forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))). -intros. -apply nat_elim2 -(\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro. -intros.elim n1. -simplify. reflexivity. -elim e1.simplify. reflexivity. -simplify. reflexivity. -intros. elim n1. -simplify. reflexivity. -simplify.reflexivity. -intros. -rewrite < (Zplus_pos_neg ? m1). -elim H.reflexivity. -qed. - -theorem Zplus_Zsucc_neg_neg : -\forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))). -intros. -apply nat_elim2 -(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro. -intros.elim n1. -simplify. reflexivity. -elim e1.simplify. reflexivity. -simplify. reflexivity. -intros. elim n1. -simplify. reflexivity. -simplify.reflexivity. -intros. -rewrite < (Zplus_neg_neg ? m1). -reflexivity. -qed. - -theorem Zplus_Zsucc_neg_pos: -\forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))). -intros. -apply nat_elim2 -(\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))). -intros.elim n1. -simplify. reflexivity. -elim e1.simplify. reflexivity. -simplify. reflexivity. -intros. elim n1. -simplify. reflexivity. -simplify.reflexivity. -intros. -rewrite < H. -rewrite < (Zplus_neg_pos ? (S m1)). -reflexivity. -qed. - -theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)). -intros.elim x.elim y. -simplify. reflexivity. -rewrite < Zsucc_Zplus_pos_O.reflexivity. -simplify.reflexivity. -elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity. -apply Zplus_Zsucc_neg_neg. -apply Zplus_Zsucc_neg_pos. -elim y. -rewrite < sym_Zplus OZ.reflexivity. -apply Zplus_Zsucc_pos_neg. -apply Zplus_Zsucc_pos_pos. -qed. - -theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)). -intros. -cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)). +elim z.reflexivity. +simplify. +cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))). rewrite > Hcut. -rewrite > Zplus_Zsucc. -rewrite > Zpred_Zsucc. -reflexivity. -rewrite > Zsucc_Zpred. -reflexivity. -qed. - - -theorem associative_Zplus: associative Z Zplus. -change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)). - -intros.elim x.simplify.reflexivity. -elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)). -rewrite < (Zpred_Zplus_neg_O y). -rewrite < Zplus_Zpred. -reflexivity. -rewrite > Zplus_Zpred (neg e). -rewrite > Zplus_Zpred (neg e). -rewrite > Zplus_Zpred (Zplus (neg e) y). -apply eq_f.assumption. -elim e2.rewrite < Zsucc_Zplus_pos_O. -rewrite < Zsucc_Zplus_pos_O. -rewrite > Zplus_Zsucc. +rewrite > Hcut. +rewrite < nat_compare_pred_pred ? ? ? ?. +rewrite < nat_compare_times_l. +rewrite < nat_compare_S_S. +apply nat_compare_elim n1 n2. +intro. +(* per ricavare questo change ci ho messo un'ora; +LA GESTIONE DELLA RIDUZIONE NON VA *) +change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n2) (S n1))))))) + (pos (pred (minus (pred (times (S n) (S n2))) + (pred (times (S n) (S n1))))))). +rewrite < S_pred ? ?. +rewrite > minus_pred_pred ? ? ? ?. +rewrite < distr_times_minus. +reflexivity. +(* we start closing stupid positivity conditions *) +apply lt_O_times_S_S. +apply lt_O_times_S_S. +simplify. +apply le_SO_minus. exact H. +intro.rewrite < H.simplify.reflexivity. +intro. +change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n1) (S n2))))))) + (neg (pred (minus (pred (times (S n) (S n1))) + (pred (times (S n) (S n2))))))). +rewrite < S_pred ? ?. +rewrite > minus_pred_pred ? ? ? ?. +rewrite < distr_times_minus. +reflexivity. +(* we start closing stupid positivity conditions *) +apply lt_O_times_S_S. +apply lt_O_times_S_S. +simplify. +apply le_SO_minus. exact H. +(* questi non so neppure da dove vengano *) +apply lt_O_times_S_S. +apply lt_O_times_S_S. +(* adesso chiudo il cut stupido *) +intros.reflexivity. +change with +eq Z (neg (pred (times (S n) (plus (S n1) (S n2))))) + (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))). +rewrite < times_plus_distr. reflexivity. -rewrite > Zplus_Zsucc (pos e1). -rewrite > Zplus_Zsucc (pos e1). -rewrite > Zplus_Zsucc (Zplus (pos e1) y). -apply eq_f.assumption. -qed. - -variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)) -\def associative_Zplus. -*) +(* and now the case x = pos n *) diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index d3bc2ee25..cdc0e44d7 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -108,7 +108,7 @@ definition Zplus :Z \to Z \to Z \def | (pos m) \Rightarrow match y with [ OZ \Rightarrow x - | (pos n) \Rightarrow (pos (S (m+n))) + | (pos n) \Rightarrow (pos (pred ((S m)+(S n)))) | (neg n) \Rightarrow match nat_compare m n with [ LT \Rightarrow (neg (pred (n-m))) @@ -122,7 +122,7 @@ definition Zplus :Z \to Z \to Z \def [ LT \Rightarrow (pos (pred (n-m))) | EQ \Rightarrow OZ | GT \Rightarrow (neg (pred (m-n)))] - | (neg n) \Rightarrow (neg (S (m+n)))]]. + | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]]. (*CSC: the URI must disappear: there is a bug now *) interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y). @@ -140,7 +140,7 @@ theorem sym_Zplus : \forall x,y:Z. x+y = y+x. intros.elim x.rewrite > Zplus_z_OZ.reflexivity. elim y.simplify.reflexivity. simplify. -rewrite < sym_plus.reflexivity. +rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. simplify. rewrite > nat_compare_n_m_m_n. simplify.elim nat_compare ? ?.simplify.reflexivity. @@ -151,7 +151,7 @@ simplify.rewrite > nat_compare_n_m_m_n. simplify.elim nat_compare ? ?.simplify.reflexivity. simplify. reflexivity. simplify. reflexivity. -simplify.rewrite < sym_plus.reflexivity. +simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity. qed. theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z. @@ -177,9 +177,9 @@ elim n.elim m. simplify.reflexivity. simplify.reflexivity. elim m. -simplify. +simplify.rewrite < plus_n_Sm. rewrite < plus_n_O.reflexivity. -simplify. +simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.reflexivity. qed. @@ -206,7 +206,7 @@ elim n.elim m. simplify.reflexivity. simplify.reflexivity. elim m. -simplify.rewrite < plus_n_Sm.reflexivity. +simplify.rewrite > plus_n_Sm.reflexivity. simplify.rewrite > plus_n_Sm.reflexivity. qed. diff --git a/helm/matita/library/nat/compare.ma b/helm/matita/library/nat/compare.ma index 60a9d4194..3a8e4a87c 100644 --- a/helm/matita/library/nat/compare.ma +++ b/helm/matita/library/nat/compare.ma @@ -78,6 +78,21 @@ nat_compare n m = nat_compare (S n) (S m). intros.simplify.reflexivity. qed. +theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)). +intro.elim n.apply False_ind.exact not_le_Sn_O O H. +apply eq_f.apply pred_Sn. +qed. + +theorem nat_compare_pred_pred: +\forall n,m:nat.lt O n \to lt O m \to +eq compare (nat_compare n m) (nat_compare (pred n) (pred m)). +intros. +apply lt_O_n_elim n H. +apply lt_O_n_elim m H1. +intros. +simplify.reflexivity. +qed. + theorem nat_compare_to_Prop: \forall n,m:nat. match (nat_compare n m) with [ LT \Rightarrow n < m diff --git a/helm/matita/library/nat/div_and_mod.ma b/helm/matita/library/nat/div_and_mod.ma index ca8b6c3fa..619ba6815 100644 --- a/helm/matita/library/nat/div_and_mod.ma +++ b/helm/matita/library/nat/div_and_mod.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/nat/div_and_mod". include "nat/minus.ma". -include "nat/orders_op.ma". +include "nat/le_arith.ma". include "nat/compare.ma". let rec mod_aux p m n: nat \def @@ -174,3 +174,41 @@ apply le_times_r. apply lt_to_le. apply H6. qed. + +theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O. +intros.constructor 1. +simplify.apply le_S_S.apply le_O_n. +rewrite < plus_n_O.rewrite < sym_times.reflexivity. +qed. + +theorem div_times: \forall n,m:nat. div ((S n)*m) (S n) = m. +intros. +apply div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O. +apply div_mod_spec_div_mod. +simplify.apply le_S_S.apply le_O_n. +apply div_mod_spec_times. +qed. + +theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m). +change with \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q. +intros. +rewrite < div_times n. +rewrite < div_times n q. +apply eq_f2.assumption. +reflexivity. +qed. + +variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def +injective_times_r. + +theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)). +change with \forall n,p,q:nat.p*(S n) = q*(S n) \to p=q. +intros. +apply inj_times_r n p q. +rewrite < sym_times. +rewrite < sym_times q. +assumption. +qed. + +variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def +injective_times_l. diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma new file mode 100644 index 000000000..c0d363773 --- /dev/null +++ b/helm/matita/library/nat/exp.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/exp". + +include "nat/times.ma". + +let rec exp n m on m\def + match m with + [ O \Rightarrow (S O) + | (S p) \Rightarrow (times n (exp n p)) ]. + +theorem exp_plus_times : \forall n,p,q:nat. +eq nat (exp n (plus p q)) (times (exp n p) (exp n q)). +intros.elim p. +simplify.rewrite < plus_n_O.reflexivity. +simplify.rewrite > H.symmetry. +apply assoc_times. +qed. + +theorem exp_n_O : \forall n:nat. eq nat (S O) (exp n O). +intro.simplify.reflexivity. +qed. + +theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)). +intro.simplify.rewrite < times_n_SO.reflexivity. +qed. + +theorem bad : \forall n,p,q:nat. +eq nat (exp (exp n p) q) (exp n (times p q)). +intros. +elim q.simplify.rewrite < times_n_O.simplify.reflexivity. +simplify.rewrite > H.rewrite < exp_plus_times. +rewrite < times_n_Sm.reflexivity. +qed. \ No newline at end of file diff --git a/helm/matita/library/nat/le_arith.ma b/helm/matita/library/nat/le_arith.ma new file mode 100644 index 000000000..a36f96bd4 --- /dev/null +++ b/helm/matita/library/nat/le_arith.ma @@ -0,0 +1,99 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/le_arith". + +include "higher_order_defs/functions.ma". +include "nat/times.ma". +include "nat/orders.ma". +include "nat/compare.ma". + +(* plus *) +theorem monotonic_le_plus_r: +\forall n:nat.monotonic nat le (\lambda m.plus n m). +simplify.intros.elim n. +simplify.assumption. +simplify.apply le_S_S.assumption. +qed. + +theorem le_plus_r: \forall p,n,m:nat. le n m \to le (plus p n) (plus p m) +\def monotonic_le_plus_r. + +theorem monotonic_le_plus_l: +\forall m:nat.monotonic nat le (\lambda n.plus n m). +simplify.intros. +rewrite < sym_plus.rewrite < sym_plus m. +apply le_plus_r.assumption. +qed. + +theorem le_plus_l: \forall p,n,m:nat. le n m \to le (plus n p) (plus m p) +\def monotonic_le_plus_l. + +theorem le_plus: \forall n1,n2,m1,m2:nat. le n1 n2 \to le m1 m2 +\to le (plus n1 m1) (plus n2 m2). +intros. +apply trans_le ? (plus n2 m1). +apply le_plus_l.assumption. +apply le_plus_r.assumption. +qed. + +theorem le_plus_n :\forall n,m:nat. le m (plus n m). +intros.change with le (plus O m) (plus n m). +apply le_plus_l.apply le_O_n. +qed. + +theorem eq_plus_to_le: \forall n,m,p:nat.eq nat n (plus m p) +\to le m n. +intros.rewrite > H. +rewrite < sym_plus. +apply le_plus_n. +qed. + +(* times *) +theorem monotonic_le_times_r: +\forall n:nat.monotonic nat le (\lambda m.times n m). +simplify.intros.elim n. +simplify.apply le_O_n. +simplify.apply le_plus. +assumption. +assumption. +qed. + +theorem le_times_r: \forall p,n,m:nat. le n m \to le (times p n) (times p m) +\def monotonic_le_times_r. + +theorem monotonic_le_times_l: +\forall m:nat.monotonic nat le (\lambda n.times n m). +simplify.intros. +rewrite < sym_times.rewrite < sym_times m. +apply le_times_r.assumption. +qed. + +theorem le_times_l: \forall p,n,m:nat. le n m \to le (times n p) (times m p) +\def monotonic_le_times_l. + +theorem le_times: \forall n1,n2,m1,m2:nat. le n1 n2 \to le m1 m2 +\to le (times n1 m1) (times n2 m2). +intros. +apply trans_le ? (times n2 m1). +apply le_times_l.assumption. +apply le_times_r.assumption. +qed. + +theorem le_times_n: \forall n,m:nat.le (S O) n \to le m (times n m). +intros.elim H.simplify. +elim (plus_n_O ?).apply le_n. +simplify.rewrite < sym_plus.apply le_plus_n. +qed. + diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma new file mode 100644 index 000000000..5bef22371 --- /dev/null +++ b/helm/matita/library/nat/lt_arith.ma @@ -0,0 +1,162 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/nat/lt_arith". + +include "nat/div_and_mod.ma". + +(* plus *) +theorem monotonic_lt_plus_r: +\forall n:nat.monotonic nat lt (\lambda m.plus n m). +simplify.intros. +elim n.simplify.assumption. +simplify. +apply le_S_S.assumption. +qed. + +variant lt_plus_r: \forall n,p,q:nat. lt p q \to lt (plus n p) (plus n q) \def +monotonic_lt_plus_r. + +theorem monotonic_lt_plus_l: +\forall n:nat.monotonic nat lt (\lambda m.plus m n). +change with \forall n,p,q:nat. lt p q \to lt (plus p n) (plus q n). +intros. +rewrite < sym_plus. rewrite < sym_plus n. +apply lt_plus_r.assumption. +qed. + +variant lt_plus_l: \forall n,p,q:nat. lt p q \to lt (plus p n) (plus q n) \def +monotonic_lt_plus_l. + +theorem lt_plus: \forall n,m,p,q:nat. lt n m \to lt p q \to lt (plus n p) (plus m q). +intros. +apply trans_lt ? (plus n q). +apply lt_plus_r.assumption. +apply lt_plus_l.assumption. +qed. + +theorem lt_plus_to_lt_l :\forall n,p,q:nat. lt (plus p n) (plus q n) \to lt p q. +intro.elim n. +rewrite > plus_n_O. +rewrite > plus_n_O q.assumption. +apply H. +simplify.apply le_S_S_to_le. +rewrite > plus_n_Sm. +rewrite > plus_n_Sm q. +exact H1. +qed. + +theorem lt_plus_to_lt_r :\forall n,p,q:nat. lt (plus n p) (plus n q) \to lt p q. +intros.apply lt_plus_to_lt_l n. +rewrite > sym_plus. +rewrite > sym_plus q.assumption. +qed. + +(* times and zero *) +theorem lt_O_times_S_S: \forall n,m:nat.lt O (times (S n) (S m)). +intros.simplify.apply le_S_S.apply le_O_n. +qed. + +(* times *) +theorem monotonic_lt_times_r: +\forall n:nat.monotonic nat lt (\lambda m.times (S n) m). +change with \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q). +intros.elim n. +simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption. +change with lt (plus p (times (S n1) p)) (plus q (times (S n1) q)). +apply lt_plus.assumption.assumption. +qed. + +theorem lt_times_r: \forall n,p,q:nat. lt p q \to lt (times (S n) p) (times (S n) q) +\def monotonic_lt_times_r. + +theorem monotonic_lt_times_l: +\forall m:nat.monotonic nat lt (\lambda n.times n (S m)). +change with +\forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n)). +intros. +rewrite < sym_times.rewrite < sym_times (S n). +apply lt_times_r.assumption. +qed. + +variant lt_times_l: \forall n,p,q:nat. lt p q \to lt (times p (S n)) (times q (S n)) +\def monotonic_lt_times_l. + +theorem lt_times:\forall n,m,p,q:nat. lt n m \to lt p q \to lt (times n p) (times m q). +intro. +elim n. +apply lt_O_n_elim m H. +intro. +cut lt O q. +apply lt_O_n_elim q Hcut. +intro.change with lt O (times (S m1) (S m2)). +apply lt_O_times_S_S. +apply ltn_to_ltO p q H1. +apply trans_lt ? (times (S n1) q). +apply lt_times_r.assumption. +cut lt O q. +apply lt_O_n_elim q Hcut. +intro. +apply lt_times_l. +assumption. +apply ltn_to_ltO p q H2. +qed. + +theorem lt_times_to_lt_l: +\forall n,p,q:nat. lt (times p (S n)) (times q (S n)) \to lt p q. +intros. +(* convertibility problem here *) +cut Or (lt p q) (Not (lt p q)). +elim Hcut. +assumption. +absurd lt (times p (S n)) (times q (S n)). +assumption. +apply le_to_not_lt. +apply le_times_l. +apply not_lt_to_le. +assumption. +exact decidable_lt p q. +qed. + +theorem lt_times_to_lt_r: +\forall n,p,q:nat. lt (times (S n) p) (times(S n) q) \to lt p q. +intros. +apply lt_times_to_lt_l n. +rewrite < sym_times. +rewrite < sym_times (S n). +assumption. +qed. + +theorem nat_compare_times_l : \forall n,p,q:nat. +eq compare (nat_compare p q) (nat_compare (times (S n) p) (times (S n) q)). +intros.apply nat_compare_elim.intro. +apply nat_compare_elim. +intro.reflexivity. +intro.absurd eq nat p q. +apply inj_times_r n.assumption. +apply lt_to_not_eq. assumption. +intro.absurd lt q p. +apply lt_times_to_lt_r n.assumption. +apply le_to_not_lt.apply lt_to_le.assumption. +intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity. +intro.apply nat_compare_elim.intro. +absurd (lt p q). +apply lt_times_to_lt_r n.assumption. +apply le_to_not_lt.apply lt_to_le.assumption. +intro.absurd eq nat q p. +symmetry. +apply inj_times_r n.assumption. +apply lt_to_not_eq.assumption. +intro.reflexivity. +qed. diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma index e725185e0..1b7900314 100644 --- a/helm/matita/library/nat/minus.ma +++ b/helm/matita/library/nat/minus.ma @@ -15,7 +15,7 @@ set "baseuri" "cic:/matita/nat/minus". -include "nat/orders_op.ma". +include "nat/le_arith.ma". include "nat/compare.ma". let rec minus n m \def @@ -98,6 +98,20 @@ symmetry. apply plus_minus_m_m.assumption. qed. +theorem minus_S_S : \forall n,m:nat. +eq nat (minus (S n) (S m)) (minus n m). +intros. +reflexivity. +qed. + +theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to +eq nat (minus (pred n) (pred m)) (minus n m). +intros. +apply lt_O_n_elim n H.intro. +apply lt_O_n_elim m H1.intro. +simplify.reflexivity. +qed. + theorem eq_minus_n_m_O: \forall n,m:nat. n \leq m \to n-m = O. intros 2. diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma index d269e5fe1..4ec4dfc5b 100644 --- a/helm/matita/library/nat/orders.ma +++ b/helm/matita/library/nat/orders.ma @@ -52,6 +52,15 @@ qed. theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p \def transitive_le. +theorem transitive_lt: transitive nat lt. +simplify.intros.elim H1. +apply le_S. assumption. +apply le_S.assumption. +qed. + +theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p +\def transitive_lt. + theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m. intros.elim H. apply le_n. @@ -95,10 +104,11 @@ apply H.assumption. apply le_S_S_to_le.assumption. qed. -(* ??? this needs not le *) -theorem S_pred: \forall n:nat.O H.apply times_n_Sm. qed. +variant sym_times : \forall n,m:nat. n*m = m*n \def +symmetric_times. + theorem distributive_times_plus : distributive nat times plus. simplify. intros.elim x. @@ -64,6 +70,18 @@ apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z. rewrite > assoc_plus.reflexivity. qed. -variant times_plus_distr: \forall n,m,p:nat. n*(m+p)=n*m+n*p +variant times_plus_distr: \forall n,m,p:nat. n*(m+p) = n*m + n*p \def distributive_times_plus. +theorem associative_times: associative nat times. +simplify.intros. +elim x.simplify.apply refl_eq. +simplify.rewrite < sym_times. +rewrite > times_plus_distr. +rewrite < sym_times. +rewrite < sym_times (times n y) z. +rewrite < H.apply refl_eq. +qed. + +variant assoc_times: \forall n,m,p:nat. (n*m)*p = n*(m*p) \def +associative_times.