From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 17 Feb 2007 22:37:23 +0000 (+0000)
Subject: contribs: some improvements
X-Git-Tag: 0.4.95@7852~592
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00f8f919262e3c84dd9e42477092cc1312171493;p=helm.git

contribs: some improvements
---

diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
deleted file mode 100644
index 4da3c95d7..000000000
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Context/defs".
-
-(* FLAT CONTEXTS
-   - Naming policy:
-     - contexts: c d
-*)
-
-include "Term/defs.ma".
-
-inductive Context: Set \def
-   | leaf: Context
-   | intb: Context \to IntB \to Term \to Context
-.
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
index 131d65133..d8ee64fe5 100644
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma
@@ -18,7 +18,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs".
    - Usage: invoke with positive polarity
 *)
 
-include "Term/defs.ma".
+include "datatypes/Term.ma".
 
 inductive Lift (l: Nat): Nat \to Term \to Term \to Prop \def
    | lift_sort   : \forall i,h. 
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma
new file mode 100644
index 000000000..fd794fe9b
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fun".
+
+include "Lift/inv.ma".
+
+(* Functional properties ****************************************************)
+(*
+theorem lift_total: \forall l, t, i. \exists u. Lift l i t u.
+ intros 2. elim t; clear t;
+ [ 
+*)
+theorem lift_mono: \forall l,i,t,t1. Lift l i t t1 \to
+                   \forall t2. Lift l i t t2 \to
+                   t1 = t2.
+ intros 5. elim H; clear H i t t1;
+ [ lapply linear lift_inv_sort_1 to H1
+ | lapply linear lift_inv_lref_1_gt to H2, H1
+ | lapply linear lift_inv_lref_1_le to H3, H1, H2
+ | lapply linear lift_inv_bind_1 to H5. decompose
+ | lapply linear lift_inv_flat_1 to H5. decompose
+ ]; subst; auto.
+qed.
+
+theorem lift_inj: \forall l,i,t1,t. Lift l i t1 t \to
+                  \forall t2. Lift l i t2 t \to
+                  t2 = t1.
+ intros 5. elim H; clear H i t1 t;
+ [ lapply linear lift_inv_sort_2 to H1
+ | lapply linear lift_inv_lref_2_gt to H2, H1
+ | lapply nle_nplus to H2 as H. (**)
+   lapply linear nle_trans to H1, H as H0.
+   lapply lift_inv_lref_2_le to H3, H0, H2
+ | lapply linear lift_inv_bind_2 to H5. decompose
+ | lapply linear lift_inv_flat_2 to H5. decompose
+ ]; subst; auto.
+qed.
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
index 8c3d27d7c..d664e5f07 100644
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma
@@ -16,6 +16,8 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/inv".
 
 include "Lift/defs.ma".
 
+(* Inversion properties *****************************************************)
+
 theorem lift_inv_sort_1: \forall l, i, h, x.
                          Lift l i (leaf (sort h)) x \to
                          x = leaf (sort h).
@@ -72,3 +74,104 @@ theorem lift_inv_flat_1: \forall l, i, r, u1, t1, x.
  | destruct H5. clear H5 H1 H3. subst. auto depth = 5
  ].
 qed.
+
+theorem lift_inv_sort_2: \forall l, i, x, h.
+                         Lift l i x (leaf (sort h)) \to
+                         x = leaf (sort h).
+ intros. inversion H; clear H; intros;
+ [ auto
+ | destruct H3
+ | destruct H4
+ | destruct H6
+ | destruct H6
+ ].
+qed.
+
+theorem lift_inv_lref_2: \forall l, i, x, j2.
+                         Lift l i x (leaf (lref j2)) \to
+                         (i > j2 \land x = leaf (lref j2)) \lor
+                         (i <= j2 \land 
+                          \exists j1. (l + j1 == j2) \land x = leaf (lref j1)
+                         ).
+ intros. inversion H; clear H; intros;
+ [ destruct H2
+ | destruct H3. clear H3. subst. auto
+ | destruct H4. clear H4. subst. auto depth = 5
+ | destruct H6
+ | destruct H6
+ ].
+qed.
+
+theorem lift_inv_bind_2: \forall l, i, r, x, u2, t2.
+                         Lift l i x (intb r u2 t2) \to
+                         \exists u1, t1. 
+                         Lift l i u1 u2 \land
+                         Lift l (succ i) t1 t2 \land
+                         x = intb r u1 t1.
+ intros. inversion H; clear H; intros;
+ [ destruct H2
+ | destruct H3
+ | destruct H4
+ | destruct H6. clear H5 H1 H3. subst. auto depth = 5
+ | destruct H6
+ ].
+qed.
+
+theorem lift_inv_flat_2: \forall l, i, r, x, u2, t2.
+                         Lift l i x (intf r u2 t2) \to
+                         \exists u1, t1. 
+                         Lift l i u1 u2 \land
+                         Lift l i t1 t2 \land
+                         x = intf r u1 t1.
+ intros. inversion H; clear H; intros;
+ [ destruct H2
+ | destruct H3
+ | destruct H4
+ | destruct H6 
+ | destruct H6. clear H6 H1 H3. subst. auto depth = 5
+ ].
+qed.
+
+(* Corollaries of inversion properties ***************************************)
+
+theorem lift_inv_lref_1_gt: \forall l, i, j1, x.
+                            Lift l i (leaf (lref j1)) x \to
+                            i > j1 \to x = leaf (lref j1).
+ intros 5.
+ lapply linear lift_inv_lref_1 to H. decompose; subst;
+ [ auto
+ | lapply linear nle_false to H2, H1. decompose
+ ].
+ qed.
+
+theorem lift_inv_lref_1_le: \forall l, i, j1, x.
+                            Lift l i (leaf (lref j1)) x \to
+                            i <= j1 \to \forall j2. (l + j1 == j2) \to
+                            x = leaf (lref j2).
+ intros 5.
+ lapply linear lift_inv_lref_1 to H. decompose; subst;
+ [ lapply linear nle_false to H1, H3. decompose
+ | lapply linear nplus_mono to H2, H4. subst. auto
+ ].
+qed.
+
+theorem lift_inv_lref_2_gt: \forall l, i, x, j2.
+                            Lift l i x (leaf (lref j2)) \to
+                            i > j2 \to x = leaf (lref j2).
+ intros 5.
+ lapply linear lift_inv_lref_2 to H. decompose; subst;
+ [ auto
+ | lapply linear nle_false to H2, H1. decompose
+ ].
+ qed.
+
+theorem lift_inv_lref_2_le: \forall l, i, x, j2.
+                            Lift l i x (leaf (lref j2)) \to
+                            i <= j2 \to \forall j1. (l + j1 == j2) \to
+                            x = leaf (lref j1).
+ intros 5.
+ lapply linear lift_inv_lref_2 to H. decompose; subst;
+ [ lapply linear nle_false to H1, H3. decompose
+ | lapply linear nplus_inj_2 to H2, H4. subst. auto
+ ].
+qed.
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
index 8c3df062e..a5c566dab 100644
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma
@@ -14,35 +14,14 @@
 
 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
 
-include "Lift/inv.ma".
+include "Lift/fun.ma".
 
-theorem lift_conf: \forall l,i,t,x. Lift l i t x \to
-                   \forall y. Lift l i t y \to
-                   x = y.
- intros 5. elim H; clear H i t x;
- [ lapply linear lift_inv_sort_1 to H1.
-   subst. auto
- | lapply linear lift_inv_lref_1 to H2.
-   decompose; subst;
-   [ auto | lapply nle_false to H2, H1. decompose ]
- | lapply linear lift_inv_lref_1 to H3.
-   decompose; subst;
-   [ lapply linear nle_false to H1, H3. decompose
-   | lapply linear nplus_conf to H2, H4. subst. auto
-   ]
- | lapply linear lift_inv_bind_1 to H5.
-   decompose. subst. auto.
- | lapply linear lift_inv_flat_1 to H5.
-   decompose. subst. auto.
- ].
-qed.
-
-theorem lift_comp_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
-                      \forall l2,i2,x. (Lift l2 i2 t x) \to
-                      \forall z. (Lift l2 i2 y z) \to
-                      i2 <= i1 \to \forall i. (l2 + i1 == i) \to
-                      (Lift l1 i x z).
- intros 5. elim H; clear H i1 t y;
+theorem lift_comp_ge_1: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
+                        \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
+                        \forall u2. Lift l2 i2 t2 u2 \to
+                        i1 >= i2 \to \forall i. (l2 + i1 == i) \to
+                        Lift l1 i u1 u2.
+ intros 5. elim H; clear H i1 t1 t2;
  [ lapply lift_conf to H1, H2. clear H2. subst.
    lapply linear lift_inv_sort_1 to H1.
    subst. auto
@@ -69,4 +48,80 @@ theorem lift_comp_le: \forall l1,i1,t,y. (Lift l1 i1 t y) \to
        lapply nle_nplus_comp to H6, H7; auto.
      ]
    ]
- |
\ No newline at end of file
+ | clear H1 H3.
+   lapply linear lift_inv_bind_1 to H5.
+   lapply linear lift_inv_bind_1 to H6.
+   decompose. subst. auto width = 4
+ | clear H1 H3.
+   lapply linear lift_inv_flat_1 to H5.
+   lapply linear lift_inv_flat_1 to H6.
+   decompose. subst. auto width = 4
+ ].
+qed.
+
+theorem lift_comp_ge_2: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
+                        \forall l2,i2,u1. Lift l2 i2 t1 u1 \to
+                        \forall i,u2. Lift l2 i t2 u2 \to
+                        i2 >= i1 \to (l1 + i2 == i) \to
+                        Lift l1 i1 u1 u2.
+ intros 5. elim H; clear H i1 t1 t2;
+ [ lapply linear lift_inv_sort_1 to H1.
+   lapply linear lift_inv_sort_1 to H2.
+   subst. auto
+ | lapply linear lift_inv_lref_1 to H2.
+   lapply linear lift_inv_lref_1 to H3.
+   decompose; subst; (* clear H2 H4 i2; *)
+   [ clear H H3 H4 H5. auto
+   | clear H1 H4 H7.
+     lapply linear nle_nplus to H5 as H0. (**)
+     lapply linear nle_trans to H3, H0 as H2.
+     lapply nle_false to H, H2. decompose
+   | clear H H5 H6.
+     lapply linear nle_trans to H4, H3 as H.
+     lapply nle_false to H, H1. decompose
+   | clear H H2 H5 H7. 
+     lapply linear nle_trans to H4, H3 as H.
+     lapply nle_false to H, H1. decompose
+   ]
+(* 
+ | lapply linear lift_inv_lref_1 to H3.
+   decompose; subst;
+   [ clear H2 H4 H6 n3 l2.
+     lapply linear nle_trans to H3, H5 as H0.
+     lapply linear nle_false to H1, H0. decompose
+   | lapply linear lift_inv_lref_1 to H4.
+     decompose; subst;
+     [ clear H1 H5 H6 H7 n1.
+       lapply linear nle_nplus to H2 as H0. (**)
+       lapply linear nle_trans to H3, H0 as H2.
+       lapply linear nle_false to H2, H4. decompose
+     | clear H3 H4 H5.
+       lapply nle_nplus_comp to H6, H7; auto.
+     ]
+   ]
+ | clear H1 H3.
+   lapply linear lift_inv_bind_1 to H5.
+   lapply linear lift_inv_bind_1 to H6.
+   decompose. subst. auto width = 4
+ | clear H1 H3.
+   lapply linear lift_inv_flat_1 to H5.
+   lapply linear lift_inv_flat_1 to H6.
+   decompose. subst. auto width = 4
+ ].
+qed.
+
+
+(*
+theorem lift_trans_le: \forall l1,i1,t1,t2. Lift l1 i1 t1 t2 \to
+                       \forall l2,i2,z. Lift l2 i2 t2 t3 \to
+		       i1 <= i2 \to 
+		       \forall i. \to i2 <= i \to (l1 + i1 == i) \to
+		       \forall l. (l1 + l2 == l) \to Lift l i1 t1 t3.
+*)
+axiom lift_conf_back_ge: \forall l1,i1,u1,u2. Lift l1 i1 u1 u2 \to
+	                 \forall l2,i,t2. Lift l2 i t2 u2 \to
+	                 \forall i2. i2 >= i1 \to (l1 + i2 == i) \to
+                         \exists t1. | Lift l2 i2 t1 u1 \land
+                                       Lift l1 i1 t1 t2.
+
+*)
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma
deleted file mode 100644
index e0b165e4f..000000000
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma
+++ /dev/null
@@ -1,58 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Term/defs".
-
-(* POLARIZED TERMS
-   - Naming policy:
-     - natural numbers      : sorts h k, local references i j, lengths l o
-     - boolean values       : p q
-     - generic leaf items   : m n
-     - generic binding items: r s 
-     - generic flat items   : r s
-     - generic head items   : m n
-     - terms                : t u
-*)
-
-include "preamble.ma".
-
-inductive Leaf: Set \def
-   | sort: Nat \to Leaf
-   | lref: Nat \to Leaf
-.
-
-inductive Bind: Set \def
-   | abbr: Bind
-   | abst: Bind
-   | excl: Bind
-.
-
-inductive Flat: Set \def
-   | appl: Flat
-   | cast: Flat
-.
-
-inductive IntB: Set \def
-   | bind: Bool \to Bind \to IntB
-.
-
-inductive IntF: Set \def
-   | flat: Bool \to Flat \to IntF
-.
-
-inductive Term: Set \def
-   | leaf: Leaf \to Term
-   | intb: IntB \to Term \to Term \to Term
-   | intf: IntF \to Term \to Term \to Term
-.
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma
new file mode 100644
index 000000000..844b19c34
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Context".
+
+(* FLAT CONTEXTS
+   - Naming policy:
+     - contexts: c d
+*)
+
+include "datatypes/Term.ma".
+
+inductive Context: Set \def
+   | leaf: Context
+   | intb: Context \to IntB \to Term \to Context
+.
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma
new file mode 100644
index 000000000..ba37390d9
--- /dev/null
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term".
+
+(* POLARIZED TERMS
+   - Naming policy:
+     - natural numbers      : sorts h k, local references i j, lengths l o
+     - boolean values       : p q
+     - generic leaf items   : m n
+     - generic binding items: r s 
+     - generic flat items   : r s
+     - generic head items   : m n
+     - terms                : t u
+*)
+
+include "preamble.ma".
+
+inductive Leaf: Set \def
+   | sort: Nat \to Leaf
+   | lref: Nat \to Leaf
+.
+
+inductive Bind: Set \def
+   | abbr: Bind
+   | abst: Bind
+   | excl: Bind
+.
+
+inductive Flat: Set \def
+   | appl: Flat
+   | cast: Flat
+.
+
+inductive IntB: Set \def
+   | bind: Bool \to Bind \to IntB
+.
+
+inductive IntF: Set \def
+   | flat: Bool \to Flat \to IntF
+.
+
+inductive Term: Set \def
+   | leaf: Leaf \to Term
+   | intb: IntB \to Term \to Term \to Term
+   | intf: IntF \to Term \to Term \to Term
+.
diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
index 3b532dd55..d889c3995 100644
--- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
+++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma
@@ -21,7 +21,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/preamble".
 
 include "logic/equality.ma".
 include "../../RELATIONAL/datatypes/Bool.ma".
-include "../../RELATIONAL/NPlus/props.ma".
+include "../../RELATIONAL/NPlus/monoid.ma".
 include "../../RELATIONAL/NLE/props.ma".
 include "../../RELATIONAL/NLE/nplus.ma".
 
diff --git a/matita/contribs/RELATIONAL/NPlus/fun.ma b/matita/contribs/RELATIONAL/NPlus/fun.ma
new file mode 100644
index 000000000..d2d686c51
--- /dev/null
+++ b/matita/contribs/RELATIONAL/NPlus/fun.ma
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/NPlus/fun".
+
+include "NPlus/inv.ma".
+
+(* Functional properties ****************************************************)
+
+theorem nplus_total: \forall p,q. \exists r. p + q == r.
+ intros 2. elim q; clear q;
+ [ auto | decompose. auto ].
+qed.
+
+theorem nplus_mono: \forall p,q,r1. (p + q == r1) \to 
+                    \forall r2. (p + q == r2) \to r1 = r2.
+ intros 4. elim H; clear H q r1;
+ [ lapply linear nplus_gen_zero_2 to H1
+ | lapply linear nplus_gen_succ_2 to H3. decompose
+ ]; subst; auto.
+qed.
+
+theorem nplus_inj_1: \forall p1, q, r. (p1 + q == r) \to
+                     \forall p2. (p2 + q == r) \to p2 = p1.
+ intros 4. elim H; clear H q r;
+ [ lapply linear nplus_gen_zero_2 to H1
+ | lapply linear nplus_gen_succ_2_3 to H3
+ ]; auto.
+qed.
diff --git a/matita/contribs/RELATIONAL/NPlus/inv.ma b/matita/contribs/RELATIONAL/NPlus/inv.ma
index c8450346e..68043c84a 100644
--- a/matita/contribs/RELATIONAL/NPlus/inv.ma
+++ b/matita/contribs/RELATIONAL/NPlus/inv.ma
@@ -125,3 +125,10 @@ theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
    subst
  ]; auto new timeout=30.
 qed.
+
+theorem nplus_gen_succ_2_3: \forall p,q,r.
+                            (p + (succ q) == (succ r)) \to p + q == r.
+ intros. 
+ lapply linear nplus_gen_succ_2 to H. decompose. subst.
+ destruct H1. clear H1. subst. auto.
+qed.
diff --git a/matita/contribs/RELATIONAL/NPlus/monoid.ma b/matita/contribs/RELATIONAL/NPlus/monoid.ma
new file mode 100644
index 000000000..804485e54
--- /dev/null
+++ b/matita/contribs/RELATIONAL/NPlus/monoid.ma
@@ -0,0 +1,98 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/RELATIONAL/NPlus/monoid".
+
+include "NPlus/fun.ma".
+
+(* Monoidal properties ******************************************************)
+
+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 
+                      (succ p) + q == (succ r).
+ intros. elim H; clear H q r; auto.
+qed.
+
+theorem nplus_comm_rew: \forall p,q,r. (p + q == r) \to q + p == r.
+ intros. elim H; clear H q r; auto.
+qed.
+
+(* Corollaries of functional properties **************************************)
+
+theorem nplus_inj_2: \forall p, q1, r. (p + q1 == r) \to
+                     \forall q2. (p + q2 == r) \to q1 = q2.
+ intros. auto.
+qed.
+
+(* Corollaries of nonoidal properties ***************************************)
+
+theorem nplus_comm_1_rew: \forall p1,q,r1. (p1 + q == r1) \to
+                          \forall p2,r2. (p2 + q == r2) \to
+                          \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
+ intros 4. elim H; clear H q r1;
+ [ lapply linear nplus_gen_zero_2 to H1. subst
+ | lapply linear nplus_gen_succ_2 to H3. decompose. subst.
+   lapply linear nplus_gen_succ_2 to H4. decompose. subst
+ ]; auto.
+qed.
+
+(*                      
+theorem nplus_shift_succ_sx: \forall p,q,r. 
+                             (p + (succ q) == r) \to (succ p) + q == r.
+ intros.
+ lapply linear nplus_gen_succ_2 to H as H0.
+ decompose. subst. auto new timeout=100.
+qed.
+
+theorem nplus_shift_succ_dx: \forall p,q,r. 
+                             ((succ p) + q == r) \to p + (succ q) == r.
+ intros.
+ lapply linear nplus_gen_succ_1 to H as H0.
+ decompose. subst. auto new timeout=100.
+qed.
+
+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.
+   subst.
+ | lapply linear nplus_gen_succ_2 to H1 as H0.
+   decompose. subst.
+   lapply linear nplus_gen_succ_1 to H2 as H0.
+   decompose. subst.
+   lapply linear H to H4, H3 as H0.
+   decompose.
+ ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
+qed.
+
+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.
+   subst
+ | lapply linear nplus_gen_succ_2 to H1 as H0.
+   decompose. subst.
+   lapply linear nplus_gen_succ_2 to H2 as H0.
+   decompose. subst.
+   lapply linear H to H4, H3 as H0.
+   decompose.
+ ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
+qed.
+*)
+
diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma
deleted file mode 100644
index 43966337b..000000000
--- a/matita/contribs/RELATIONAL/NPlus/props.ma
+++ /dev/null
@@ -1,99 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-set "baseuri" "cic:/matita/RELATIONAL/NPlus/props".
-
-include "NPlus/inv.ma".
-
-(* Monoidal properties *)
-
-theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to 
-                    \forall r2. (p + q == r2) \to r1 = r2.
- intros 4. elim H; clear H q r1;
- [ lapply linear nplus_gen_zero_2 to H1
- | lapply linear nplus_gen_succ_2 to H3. decompose
- ]; subst; auto.
-qed.
-
-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 
-                      (succ p) + q == (succ r).
- intros. elim H; clear H q r; auto.
-qed.
-
-theorem nplus_comm: \forall p,q,r. (p + q == r) \to q + p == r.
- intros. elim H; clear H q r; auto.
-qed.
-
-(* Corollaries *)
-
-theorem nplus_comm_1: \forall p1,q,r1. (p1 + q == r1) \to
-                      \forall p2,r2. (p2 + q == r2) \to
-                      \forall s. (p1 + r2 == s) \to (p2 + r1 == s).
- intros 4. elim H; clear H q r1;
- [ lapply linear nplus_gen_zero_2 to H1. subst
- | lapply linear nplus_gen_succ_2 to H3. decompose. subst.
-   lapply linear nplus_gen_succ_2 to H4. decompose. subst
- ]; auto.
-qed.
-
-(*                      
-theorem nplus_shift_succ_sx: \forall p,q,r. 
-                             (p + (succ q) == r) \to (succ p) + q == r.
- intros.
- lapply linear nplus_gen_succ_2 to H as H0.
- decompose. subst. auto new timeout=100.
-qed.
-
-theorem nplus_shift_succ_dx: \forall p,q,r. 
-                             ((succ p) + q == r) \to p + (succ q) == r.
- intros.
- lapply linear nplus_gen_succ_1 to H as H0.
- decompose. subst. auto new timeout=100.
-qed.
-
-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.
-   subst.
- | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose. subst.
-   lapply linear nplus_gen_succ_1 to H2 as H0.
-   decompose. subst.
-   lapply linear H to H4, H3 as H0.
-   decompose.
- ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
-qed.
-
-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.
-   subst
- | lapply linear nplus_gen_succ_2 to H1 as H0.
-   decompose. subst.
-   lapply linear nplus_gen_succ_2 to H2 as H0.
-   decompose. subst.
-   lapply linear H to H4, H3 as H0.
-   decompose.
- ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
-qed.
-*)
-
diff --git a/matita/contribs/RELATIONAL/Zah/setoid.ma b/matita/contribs/RELATIONAL/Zah/setoid.ma
index 8815ee5bb..e30b5a205 100644
--- a/matita/contribs/RELATIONAL/Zah/setoid.ma
+++ b/matita/contribs/RELATIONAL/Zah/setoid.ma
@@ -14,7 +14,7 @@
 
 set "baseuri" "cic:/matita/RELATIONAL/Zah/setoid".
 
-include "NPlus/props.ma".
+include "NPlus/monoid.ma".
 include "Zah/defs.ma".
 
 theorem nplus_total: \forall p,q. \exists r. p + q == r.
@@ -57,4 +57,4 @@ theorem zeq_trans: \forall z1,z2. z1 = z2 \to
  
  
 
-*)
\ No newline at end of file
+*)