From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 24 Aug 2006 18:42:12 +0000 (+0000)
Subject: - new legature == for \equiv used in the notation for NPlus
X-Git-Tag: 0.4.95@7852~1121
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ac54ae2a52c5e5bda881d2d94f62548202184856;p=helm.git

- new legature == for \equiv used in the notation for NPlus
  FIXME: notation precedence not correct w.r.t. \to \land ...
- added notation for NLE
- added a comment to dependenciesParser.ml :p
---

diff --git a/components/content_pres/cicNotationLexer.ml b/components/content_pres/cicNotationLexer.ml
index fb459a94e..749731bda 100644
--- a/components/content_pres/cicNotationLexer.ml
+++ b/components/content_pres/cicNotationLexer.ml
@@ -123,6 +123,7 @@ let _ =
     [ ("->", <:unicode<to>>);   ("=>", <:unicode<Rightarrow>>);
       ("<=", <:unicode<leq>>);  (">=", <:unicode<geq>>);
       ("<>", <:unicode<neq>>);  (":=", <:unicode<def>>);
+      ("==", <:unicode<equiv>>);
     ]
 
 let regexp uri_step = [ 'a' - 'z' 'A' - 'Z' '0' - '9' '_' '-' ''' ]+
diff --git a/components/grafite_parser/dependenciesParser.ml b/components/grafite_parser/dependenciesParser.ml
index 5e80d8b4c..b7b4151fa 100644
--- a/components/grafite_parser/dependenciesParser.ml
+++ b/components/grafite_parser/dependenciesParser.ml
@@ -25,6 +25,17 @@
 
 (* $Id$ *)
 
+(* FG
+ * From Cambridge dictionary
+ * Dependency:
+ * a country which is supported and governed by another country
+ * Dependence:
+ * when you need something or someone all the time, especially in order to
+ * continue existing or operating
+ *
+ * Fate vobis ...
+ *)
+
 exception UnableToInclude of string
 
   (* statements meaningful for matitadep *)
diff --git a/matita/contribs/RELATIONAL/NLE/defs.ma b/matita/contribs/RELATIONAL/NLE/defs.ma
index 19e45c3bc..59c02653e 100644
--- a/matita/contribs/RELATIONAL/NLE/defs.ma
+++ b/matita/contribs/RELATIONAL/NLE/defs.ma
@@ -14,8 +14,20 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/NLE/defs".
 
+include "logic/equality.ma".
+
 include "Nat/defs.ma".
 
 inductive NLE: Nat \to Nat \to Prop \def
    | NLE_zero: \forall q. NLE zero q
-   | NLE_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q).
+   | NLE_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q)
+.
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'less or equal to'" 'leq x y = 
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) x y).
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'less than'" 'lt x y = 
+   (cic:/matita/RELATIONAL/NLE/defs/NLE.ind#xpointer(1/1) 
+      (cic:/matita/RELATIONAL/Nat/defs/Nat.ind#xpointer(1/1/2) x) y).
diff --git a/matita/contribs/RELATIONAL/NPlus/defs.ma b/matita/contribs/RELATIONAL/NPlus/defs.ma
index 92561bc5c..2bc2e8fe0 100644
--- a/matita/contribs/RELATIONAL/NPlus/defs.ma
+++ b/matita/contribs/RELATIONAL/NPlus/defs.ma
@@ -21,3 +21,11 @@ include "Nat/defs.ma".
 inductive NPlus (p:Nat): Nat \to Nat \to Prop \def
    | nplus_zero_2: NPlus p zero p
    | nplus_succ_2: \forall q, r. NPlus p q r \to NPlus p (succ q) (succ r).
+
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural plus (relational)" 'rel_plus x y z = 
+   (cic:/matita/RELATIONAL/NPlus/defs/NPlus.ind#xpointer(1/1) x y z).
+
+notation "hvbox(a break + b break == c)" 
+  non associative with precedence 95
+for @{ 'rel_plus $a $b $c}.
diff --git a/matita/contribs/RELATIONAL/NPlus/fwd.ma b/matita/contribs/RELATIONAL/NPlus/fwd.ma
index bae48d405..9b23cb2fb 100644
--- a/matita/contribs/RELATIONAL/NPlus/fwd.ma
+++ b/matita/contribs/RELATIONAL/NPlus/fwd.ma
@@ -19,15 +19,15 @@ include "NPlus/defs.ma".
 
 (* primitive generation lemmas proved by elimination and inversion *)
 
-theorem nplus_gen_zero_1: \forall q,r. NPlus zero q r \to q = r.
+theorem nplus_gen_zero_1: \forall q,r. (zero + q == r) \to q = r.
  intros. elim H; clear H q r; intros;
  [ reflexivity
  | clear H1. auto
  ].
 qed.
 
-theorem nplus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to 
-                          \exists s. r = (succ s) \land NPlus p q s.
+theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to 
+                           \exists s. r = (succ s) \land (p + q == s).
  intros. elim H; clear H q r; intros;
  [
  | clear H1.
@@ -36,7 +36,7 @@ theorem nplus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
-theorem nplus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r.
+theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r.
  intros. inversion H; clear H; intros;
  [ auto
  | clear H H1.
@@ -44,8 +44,8 @@ theorem nplus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r.
  ].
 qed.
 
-theorem nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to 
-                          \exists s. r = (succ s) \land NPlus p q s.
+theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to 
+                           \exists s. r = (succ s) \land (p + q == s).
  intros. inversion H; clear H; intros;
  [ lapply eq_gen_succ_zero to H as H0. apply H0
  | clear H1 H3 r.
@@ -55,7 +55,8 @@ theorem nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to
  ].
 qed.
 
-theorem nplus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zero.
+theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to 
+                           p = zero \land q = zero.
  intros. inversion H; clear H; intros;
  [ rewrite < H1. clear H1 p.
    auto
@@ -64,9 +65,9 @@ theorem nplus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zer
  ].
 qed.
 
-theorem nplus_gen_succ_3: \forall p,q,r. NPlus p q (succ r) \to
-                          \exists s. p = succ s \land NPlus s q r \lor
-                                     q = succ s \land NPlus p s r.
+theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to
+                           \exists s. p = succ s \land (s + q == r) \lor
+                                      q = succ s \land (p + s == r).
  intros. inversion H; clear H; intros;
  [ rewrite < H1. clear H1 p
  | clear H1.
@@ -77,7 +78,8 @@ qed.
 (*
 (* alternative proofs invoking nplus_gen_2 *)
 
-variant nplus_gen_zero_3_alt: \forall p,q. NPlus p q zero \to p = zero \land q = zero.
+variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to 
+                               p = zero \land q = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p.
@@ -89,9 +91,9 @@ variant nplus_gen_zero_3_alt: \forall p,q. NPlus p q zero \to p = zero \land q =
  ].
 qed.
 
-variant nplus_gen_succ_3_alt: \forall p,q,r. NPlus p q (succ r) \to
-                              \exists s. p = succ s \land NPlus s q r \lor
-                                         q = succ s \land NPlus p s r.
+variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to
+                               \exists s. p = succ s \land (s + q == r) \lor
+                                          q = succ s \land (p + s == r).
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p
@@ -105,7 +107,7 @@ qed.
 *)
 (* other simplification lemmas *)
 
-theorem nplus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero.
+theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p
@@ -116,7 +118,7 @@ theorem nplus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero.
  ]; auto.
 qed.
 
-theorem nplus_gen_eq_1_3: \forall p,q. NPlus p q p \to q = zero.
+theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  intros 1. elim p; clear p; intros;
  [ lapply linear nplus_gen_zero_1 to H as H0.
    rewrite > H0. clear H0 q
diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma
index 56146a3bf..a80e13fa5 100644
--- a/matita/contribs/RELATIONAL/NPlus/props.ma
+++ b/matita/contribs/RELATIONAL/NPlus/props.ma
@@ -16,11 +16,12 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props".
 
 include "NPlus/fwd.ma".
 
-theorem nplus_zero_1: \forall q. NPlus zero q q.
+theorem nplus_zero_1: \forall q. zero + q == q.
  intros. elim q; clear q; auto.
 qed.
 
-theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to NPlus (succ p) q (succ r).
+theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to 
+                       (succ p) + q == (succ r).
  intros 2. elim q; clear q;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p
@@ -30,7 +31,7 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to NPlus (succ p) q (succ r).
  ]; auto.
 qed.
 
-theorem nplus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r.
+theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
  intros 2. elim q; clear q;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p
@@ -41,7 +42,7 @@ theorem nplus_sym: \forall p,q,r. NPlus p q r \to NPlus q p r.
 qed.
 
 theorem nplus_shift_succ_sx: \forall p,q,r. 
-                             NPlus p (succ q) r \to NPlus (succ p) q r.
+                              (p + (succ q) == r) \to (succ p) + q == r.
  intros.
  lapply linear nplus_gen_succ_2 to H as H0.
  decompose.
@@ -50,7 +51,7 @@ theorem nplus_shift_succ_sx: \forall p,q,r.
 qed.
 
 theorem nplus_shift_succ_dx: \forall p,q,r. 
-                             NPlus (succ p) q r \to NPlus p (succ q) r.
+                              ((succ p) + q == r) \to p + (succ q) == r.
  intros.
  lapply linear nplus_gen_succ_1 to H as H0.
  decompose.
@@ -58,9 +59,9 @@ theorem nplus_shift_succ_dx: \forall p,q,r.
  auto.
 qed.
 
-theorem nplus_trans_1: \forall p,q1,r1. NPlus p q1 r1 \to 
-                       \forall q2,r2. NPlus r1 q2 r2 \to
-                       \exists q. NPlus q1 q2 q \land NPlus p q r2.
+theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to 
+                        \forall q2,r2. (r1 + q2 == r2) \to
+                        \exists q. (q1 + q2 == q) \land p + q == r2.
  intros 2; elim q1; clear q1; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p
@@ -75,9 +76,9 @@ theorem nplus_trans_1: \forall p,q1,r1. NPlus p q1 r1 \to
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
-theorem nplus_trans_2: \forall p1,q,r1. NPlus p1 q r1 \to 
-                       \forall p2,r2. NPlus p2 r1 r2 \to
-                       \exists p. NPlus p1 p2 p \land NPlus p q r2.
+theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to 
+                        \forall p2,r2. (p2 + r1 == r2) \to
+                        \exists p. (p1 + p2 == p) \land p + q == r2.
  intros 2; elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p1
@@ -92,8 +93,8 @@ theorem nplus_trans_2: \forall p1,q,r1. NPlus p1 q r1 \to
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
-theorem nplus_conf: \forall p,q,r1. NPlus p q r1 \to 
-                    \forall r2. NPlus p q r2 \to r1 = r2.
+theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to 
+                     \forall r2. (p + q == r2) \to r1 = r2.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0 in H1. clear H0 p