From: Ferruccio Guidi 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 +*)