**** Experimental: ****

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

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 60c727cebe9ff7967f2971b1916eb34f8c24cd4b..756d02271a62705317140ec464f0c6591b316e75 100644 (file)
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -27,18 +27,16 @@ 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: this alias must disappear: there is a bug in the generation of the .moos *)
-alias symbol "leq" (instance 0) = "integer 'less or equal to'".
 
 definition Zlt : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -51,18 +49,16 @@ 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: this alias must disappear: there is a bug in the generation of the .moos *)
-alias symbol "lt" (instance 0) = "integer 'less than'".
 
 theorem irreflexive_Zlt: irreflexive Z Zlt.
 change with \forall x:Z. x < x \to False.
@@ -95,21 +91,25 @@ definition Z_compare : Z \to Z \to compare \def
     | (pos m) \Rightarrow LT
     | (neg m) \Rightarrow nat_compare m n ]].
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_neg_neg_to_lt: 
 \forall n,m:nat. neg n < neg m \to lt m n.
 intros.apply H.
 qed.
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m. 
 intros.
 simplify.apply H.
 qed.
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem Zlt_pos_pos_to_lt: 
 \forall n,m:nat. pos n < pos m \to lt n m.
 intros.apply H.
 qed.
 
+(*CSC: qui uso lt perche' ho due istanze diverse di < *)
 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m. 
 intros.
 simplify.apply H.
@@ -127,13 +127,15 @@ simplify.exact I.
 simplify.exact I.
 elim y. simplify.exact I.
 simplify. 
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+  per via delle coercions! *)
 cut match (nat_compare n1 n) with
-[ LT \Rightarrow (lt n1 n)
-| EQ \Rightarrow (eq nat n1 n)
-| GT \Rightarrow (lt n n1)] \to 
+[ LT \Rightarrow n1<n
+| EQ \Rightarrow n1=n
+| GT \Rightarrow n<n1] \to 
 match (nat_compare n1 n) with
 [ LT \Rightarrow (le (S n1) n)
-| EQ \Rightarrow (eq Z (neg n) (neg n1))
+| EQ \Rightarrow neg n = neg n1
 | GT \Rightarrow (le (S n) n1)]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n1 n).
@@ -144,13 +146,15 @@ simplify.exact I.
 elim y.simplify.exact I.
 simplify.exact I.
 simplify.
+(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
+  per via delle coercions! *)
 cut match (nat_compare n n1) with
-[ LT \Rightarrow (lt n n1)
-| EQ \Rightarrow (eq nat n n1)
-| GT \Rightarrow (lt n1 n)] \to 
+[ LT \Rightarrow n<n1
+| EQ \Rightarrow n=n1
+| GT \Rightarrow n1<n] \to 
 match (nat_compare n n1) with
 [ LT \Rightarrow (le (S n) n1)
-| EQ \Rightarrow (eq Z (pos n) (pos n1))
+| EQ \Rightarrow pos n = pos n1
 | GT \Rightarrow (le (S n1) n)]. 
 apply Hcut. apply nat_compare_to_Prop. 
 elim (nat_compare n n1).