More notation (up to where the open bugs allow me to put it without adding

too many aliases).

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 1a2d65a4f05e6dc8c85654ca7c203fab1e72e41f..60c727cebe9ff7967f2971b1916eb34f8c24cd4b 100644 (file)
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -35,6 +35,10 @@ definition Zle : Z \to Z \to Prop \def
     | (pos m) \Rightarrow True
     | (neg m) \Rightarrow (le m 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.
@@ -55,12 +59,17 @@ definition Zlt : Z \to Z \to Prop \def
     | (pos m) \Rightarrow True
     | (neg m) \Rightarrow (lt 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. 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.
+cut neg n < neg n \to False.
 apply Hcut.apply H.simplify.apply not_le_Sn_n.
-cut (Zlt (pos n) (pos n)) \to False.
+cut pos n < pos n \to False.
 apply Hcut.apply H.simplify.apply not_le_Sn_n.
 qed.
 
@@ -87,30 +96,30 @@ definition Z_compare : Z \to Z \to compare \def
     | (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 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). 
+theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt 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 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). 
+theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt 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)]. 
+[ LT \Rightarrow x < y
+| EQ \Rightarrow x=y
+| GT \Rightarrow y < x]. 
 intros.
 elim x. elim y.
 simplify.apply refl_eq.
@@ -150,20 +159,20 @@ 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.
+theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 intros 2.elim x.
-cut (Zlt OZ y) \to (Zle (Zsucc OZ) y).
+cut OZ < y \to Zsucc OZ \leq 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).
+cut neg n < y \to Zsucc (neg n) \leq y.
 apply Hcut. assumption.elim n.
-cut (Zlt (neg O) y) \to (Zle (Zsucc (neg O)) y).
+cut neg O < y \to Zsucc (neg O) \leq 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).
+cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
 apply Hcut. assumption.simplify.
 elim y.
 simplify.exact I.

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index 9dffcee52c9098e6d4488b443d8ba79f4b5958ec..da249902bc3a251b80c7c0e445a8785b39fb52e5 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -123,8 +123,11 @@ definition Zplus :Z \to Z \to Z \def
                 | EQ \Rightarrow OZ
                 | GT \Rightarrow (neg (pred (minus m n)))]     
          | (neg n) \Rightarrow (neg (S (plus m 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).
          
-theorem Zplus_z_OZ:  \forall z:Z. eq Z (Zplus z OZ) z.
+theorem Zplus_z_OZ:  \forall z:Z. Zplus z OZ = z.
 intro.elim z.
 simplify.reflexivity.
 simplify.reflexivity.

diff --git a/helm/matita/library/datatypes/bool.ma b/helm/matita/library/datatypes/bool.ma
index 8267aa7f63fcb692311dc916f8f325471805952d..cac5ebbe97c2fdad3b421bd98d522c0525c4e413 100644 (file)
--- a/helm/matita/library/datatypes/bool.ma
+++ b/helm/matita/library/datatypes/bool.ma
@@ -24,6 +24,7 @@ definition notb : bool \to bool \def
  [ true \Rightarrow false
  | false \Rightarrow true ].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x).
 
 definition andb : bool \to bool \to bool\def
@@ -33,6 +34,7 @@ definition andb : bool \to bool \to bool\def
        match b2 with [true \Rightarrow true | false \Rightarrow false]
  | false \Rightarrow false ].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y).
 
 definition orb : bool \to bool \to bool\def
@@ -42,6 +44,7 @@ definition orb : bool \to bool \to bool\def
        match b2 with [true \Rightarrow true | false \Rightarrow false]
  | false \Rightarrow false ].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y).
 
 definition if_then_else : bool \to Prop \to Prop \to Prop \def 

diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 5a1ad1fdd0f3aa8254dd2a8f1093e0d369486813..dacf542af2d7a6640f933d502b92cdd149ee6e24 100644 (file)
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -26,7 +26,9 @@ default "false" cic:/matita/logic/connectives/False.ind.
 definition Not: Prop \to Prop \def
 \lambda A. (A \to False).
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical not" 'not x = (cic:/matita/logic/connectives/Not.con x).
+(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
 alias symbol "not" (instance 0) = "logical not".
 
 theorem absurd : \forall A,C:Prop. A \to \lnot A \to C.
@@ -38,7 +40,9 @@ default "absurd" cic:/matita/logic/connectives/absurd.con.
 inductive And (A,B:Prop) : Prop \def
     conj : A \to B \to (And A B).
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical and" 'and x y = (cic:/matita/logic/connectives/And.ind#xpointer(1/1) x y).
+(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
 alias symbol "and" (instance 0) = "logical and".
 
 theorem proj1: \forall A,B:Prop. A \land B \to A.
@@ -53,7 +57,9 @@ inductive Or (A,B:Prop) : Prop \def
      or_introl : A \to (Or A B)
    | or_intror : B \to (Or A B).
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "logical or" 'or x y = (cic:/matita/logic/connectives/Or.ind#xpointer(1/1) x y).
+(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
 alias symbol "or" (instance 0) = "logical or".
    
 definition decidable : Prop \to Prop \def \lambda A:Prop. A \lor \not A.

diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 87fe22bac85c4a9e592b8f38735c3f9e857c67ca..77ef0eb82ca2064213d49b0106cf82994a8917e0 100644 (file)
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -19,8 +19,10 @@ include "higher_order_defs/relations.ma".
 inductive eq (A:Type) (x:A) : A \to Prop \def
     refl_eq : eq A x x.
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "leibnitz's equality"
    'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
+(*CSC: this alias should disappear. It is now required because the notation for Coq is pre-loaded *)
 alias symbol "eq" (instance 0) = "leibnitz's equality".
 
     

diff --git a/helm/matita/library/nat/minus.ma b/helm/matita/library/nat/minus.ma
index 7ba20e821833db53d2d8a283428789ef559d25ff..e725185e004bfaedb6ed3dbbea63720bd91ab4ba 100644 (file)
--- a/helm/matita/library/nat/minus.ma
+++ b/helm/matita/library/nat/minus.ma
@@ -26,6 +26,7 @@ let rec minus n m \def
        [O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
 
 theorem minus_n_O: \forall n:nat.n=n-O.

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index 5389418b5237d7bde8cf4a9424bba777a5b38a62..d269e5fe1b83485fc20203ef08c5e3e6d7c988aa 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -22,22 +22,25 @@ inductive le (n:nat) : nat \to Prop \def
   | le_n : le n n
   | le_S : \forall m:nat. le n m \to le n (S m).
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
-alias symbol "leq" (instance 0) = "natural 'less or equal to'".
 
 definition lt: nat \to nat \to Prop \def
 \lambda n,m:nat.(S n) \leq m.
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
 
 definition gt: nat \to nat \to Prop \def
 \lambda n,m:nat.m<n.
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
 
 theorem transitive_le : transitive nat le.

diff --git a/helm/matita/library/nat/plus.ma b/helm/matita/library/nat/plus.ma
index 6067ebcdcd6b87ffde1fe7bce0059627e6723fb7..1c145dd6141cea519fd99f7c681a179159a72346 100644 (file)
--- a/helm/matita/library/nat/plus.ma
+++ b/helm/matita/library/nat/plus.ma
@@ -21,8 +21,8 @@ let rec plus n m \def
  [ O \Rightarrow m
  | (S p) \Rightarrow S (plus p m) ].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural plus" 'plus x y = (cic:/matita/nat/plus/plus.con x y).
-alias symbol "plus" (instance 0) = "natural plus".
 
 theorem plus_n_O: \forall n:nat. n = n+O.
 intros.elim n.

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index 24a756dc5c3b458b790eee6fa6d336ac991c54bd..d2ce51bfa83dd9605bf5160e227edf3c532aeff0 100644 (file)
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -23,6 +23,7 @@ let rec times n m \def
  [ O \Rightarrow O
  | (S p) \Rightarrow (m+(times p m)) ].
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural times" 'times x y = (cic:/matita/nat/times/times.con x y).
 
 theorem times_n_O: \forall n:nat. O = n*O.