New naming policy for local variables.

[helm.git] / helm / matita / library / Z / orders.ma

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
new file mode 100644 (file)
index 0000000..1a2d65a
--- /dev/null
+++ b/helm/matita/library/Z/orders.ma
@@ -0,0 +1,173 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||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/Z/orders".
+
+include "Z/z.ma".
+
+definition Zle : Z \to Z \to Prop \def
+\lambda x,y:Z.
+  match x with
+  [ OZ \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow True
+    | (pos m) \Rightarrow True
+    | (neg m) \Rightarrow False ]
+  | (pos n) \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow False
+    | (pos m) \Rightarrow (le n m)
+    | (neg m) \Rightarrow False ]
+  | (neg n) \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow True
+    | (pos m) \Rightarrow True
+    | (neg m) \Rightarrow (le m n) ]].
+
+
+definition Zlt : Z \to Z \to Prop \def
+\lambda x,y:Z.
+  match x with
+  [ OZ \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow False
+    | (pos m) \Rightarrow True
+    | (neg m) \Rightarrow False ]
+  | (pos n) \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow False
+    | (pos m) \Rightarrow (lt n m)
+    | (neg m) \Rightarrow False ]
+  | (neg n) \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow True
+    | (pos m) \Rightarrow True
+    | (neg m) \Rightarrow (lt m n) ]].
+    
+theorem irreflexive_Zlt: irreflexive Z Zlt.
+change with \forall x:Z. Zlt x x \to False.
+intro.elim x.exact H.
+cut (Zlt (neg n) (neg n)) \to False.
+apply Hcut.apply H.simplify.apply not_le_Sn_n.
+cut (Zlt (pos n) (pos n)) \to False.
+apply Hcut.apply H.simplify.apply not_le_Sn_n.
+qed.
+
+theorem irrefl_Zlt: irreflexive Z Zlt
+\def irreflexive_Zlt.
+
+definition Z_compare : Z \to Z \to compare \def
+\lambda x,y:Z.
+  match x with
+  [ OZ \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow EQ
+    | (pos m) \Rightarrow LT
+    | (neg m) \Rightarrow GT ]
+  | (pos n) \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow GT
+    | (pos m) \Rightarrow (nat_compare n m)
+    | (neg m) \Rightarrow GT]
+  | (neg n) \Rightarrow 
+    match y with 
+    [ OZ \Rightarrow LT
+    | (pos m) \Rightarrow LT
+    | (neg m) \Rightarrow nat_compare m n ]].
+
+theorem Zlt_neg_neg_to_lt: 
+\forall n,m:nat. Zlt (neg n) (neg m) \to lt m n.
+intros.apply H.
+qed.
+
+theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to Zlt (neg n) (neg m). 
+intros.
+simplify.apply H.
+qed.
+
+theorem Zlt_pos_pos_to_lt: 
+\forall n,m:nat. Zlt (pos n) (pos m) \to lt n m.
+intros.apply H.
+qed.
+
+theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to Zlt (pos n) (pos m). 
+intros.
+simplify.apply H.
+qed.
+
+theorem Z_compare_to_Prop : 
+\forall x,y:Z. match (Z_compare x y) with
+[ LT \Rightarrow (Zlt x y)
+| EQ \Rightarrow (eq Z x y)
+| GT \Rightarrow (Zlt y x)]. 
+intros.
+elim x. elim y.
+simplify.apply refl_eq.
+simplify.exact I.
+simplify.exact I.
+elim y. simplify.exact I.
+simplify. 
+cut match (nat_compare n1 n) with
+[ LT \Rightarrow (lt n1 n)
+| EQ \Rightarrow (eq nat n1 n)
+| GT \Rightarrow (lt n n1)] \to 
+match (nat_compare n1 n) with
+[ LT \Rightarrow (le (S n1) n)
+| EQ \Rightarrow (eq Z (neg n) (neg n1))
+| GT \Rightarrow (le (S n) n1)]. 
+apply Hcut. apply nat_compare_to_Prop. 
+elim (nat_compare n1 n).
+simplify.exact H.
+simplify.exact H.
+simplify.apply eq_f.apply sym_eq.exact H.
+simplify.exact I.
+elim y.simplify.exact I.
+simplify.exact I.
+simplify.
+cut match (nat_compare n n1) with
+[ LT \Rightarrow (lt n n1)
+| EQ \Rightarrow (eq nat n n1)
+| GT \Rightarrow (lt n1 n)] \to 
+match (nat_compare n n1) with
+[ LT \Rightarrow (le (S n) n1)
+| EQ \Rightarrow (eq Z (pos n) (pos n1))
+| GT \Rightarrow (le (S n1) n)]. 
+apply Hcut. apply nat_compare_to_Prop. 
+elim (nat_compare n n1).
+simplify.exact H.
+simplify.exact H.
+simplify.apply eq_f.exact H.
+qed.
+
+theorem Zlt_to_Zle: \forall x,y:Z. Zlt x y \to Zle (Zsucc x) y.
+intros 2.elim x.
+cut (Zlt OZ y) \to (Zle (Zsucc OZ) y).
+apply Hcut. assumption.simplify.elim y.
+simplify.exact H1.
+simplify.exact H1.
+simplify.apply le_O_n.
+cut (Zlt (neg n) y) \to (Zle (Zsucc (neg n)) y).
+apply Hcut. assumption.elim n.
+cut (Zlt (neg O) y) \to (Zle (Zsucc (neg O)) y).
+apply Hcut. assumption.simplify.elim y.
+simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
+simplify.exact I.
+cut (Zlt (neg (S n1)) y) \to (Zle (Zsucc (neg (S n1))) y).
+apply Hcut. assumption.simplify.
+elim y.
+simplify.exact I.
+simplify.apply le_S_S_to_le n2 n1 H3.
+simplify.exact I.
+exact H.
+qed.