X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;fp=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=5bef2237103f27308663712a78f78b67d0c3b621;hb=7bbce6bc163892cfd99cfcda65db42001b86789f;hp=0000000000000000000000000000000000000000;hpb=f8404e07a6b8649e85bf7a4f812a382cd3a37fca;p=helm.git

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.