X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Forders.ma;h=c39f693085398eedf4a95a9f15898f05e6cee264;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=1a2d65a4f05e6dc8c85654ca7c203fab1e72e41f;hpb=5e1fd9ee5ced5737c7fd4f25fca47feda1fda8e9;p=helm.git

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 1a2d65a4f..c39f69308 100644
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -15,6 +15,7 @@
 set "baseuri" "cic:/matita/Z/orders".
 
 include "Z/z.ma".
+include "nat/orders.ma".
 
 definition Zle : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -27,14 +28,19 @@ definition Zle : Z \to Z \to Prop \def
   | (pos n) \Rightarrow 
     match y with 
     [ OZ \Rightarrow False
-    | (pos m) \Rightarrow (le n m)
+    | (pos m) \Rightarrow n \leq m
     | (neg m) \Rightarrow False ]
   | (neg n) \Rightarrow 
     match y with 
     [ OZ \Rightarrow True
     | (pos m) \Rightarrow True
-    | (neg m) \Rightarrow (le m n) ]].
+    | (neg m) \Rightarrow m \leq n ]].
 
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer 'neither less nor equal to'" 'nleq x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)).
 
 definition Zlt : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -47,127 +53,78 @@ definition Zlt : Z \to Z \to Prop \def
   | (pos n) \Rightarrow 
     match y with 
     [ OZ \Rightarrow False
-    | (pos m) \Rightarrow (lt n m)
+    | (pos m) \Rightarrow 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) ]].
+    | (neg m) \Rightarrow m<n ]].
     
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer 'not less than'" 'nless x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
+
 theorem irreflexive_Zlt: irreflexive Z Zlt.
-change with \forall x:Z. Zlt x x \to False.
+change with (\forall x:Z. 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.
+cut (neg n < neg n \to False).
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
+cut (pos n < pos n \to False).
+apply Hcut.apply H.simplify.unfold lt.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.
+\forall n,m:nat. neg n < neg m \to 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). 
+theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to 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.
+\forall n,m:nat. pos n < pos m \to 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). 
+theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to 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.
+theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
+intros 2.
+elim x.
+(* goal: x=OZ *)
+  cut (OZ < y \to Zsucc OZ \leq y).
+    apply Hcut. assumption.
+    simplify.elim y. 
+      simplify.exact H1.
+      simplify.apply le_O_n.
+      simplify.exact H1.
+(* goal: x=pos *)      
+  exact H.
+(* goal: x=neg *)      
+  cut (neg n < y \to Zsucc (neg n) \leq y).
+    apply Hcut. assumption.
+    elim n.
+      cut (neg O < y \to Zsucc (neg O) \leq y).
+        apply Hcut. assumption.
+        simplify.elim y.
+          simplify.exact I.
+          simplify.exact I.
+          simplify.apply (not_le_Sn_O n1 H2).
+      cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y).
+        apply Hcut. assumption.simplify.
+        elim y.
+          simplify.exact I.
+          simplify.exact I.
+          simplify.apply (le_S_S_to_le n2 n1 H3).
 qed.