From 00f8f919262e3c84dd9e42477092cc1312171493 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 17 Feb 2007 22:37:23 +0000 Subject: [PATCH] contribs: some improvements --- .../LAMBDA-TYPES/Unified-Sub/Lift/defs.ma | 2 +- .../LAMBDA-TYPES/Unified-Sub/Lift/fun.ma | 49 ++++++++ .../LAMBDA-TYPES/Unified-Sub/Lift/inv.ma | 103 ++++++++++++++++ .../LAMBDA-TYPES/Unified-Sub/Lift/props.ma | 113 +++++++++++++----- .../{Context/defs.ma => datatypes/Context.ma} | 4 +- .../{Term/defs.ma => datatypes/Term.ma} | 2 +- .../LAMBDA-TYPES/Unified-Sub/preamble.ma | 2 +- matita/contribs/RELATIONAL/NPlus/fun.ma | 40 +++++++ matita/contribs/RELATIONAL/NPlus/inv.ma | 7 ++ .../RELATIONAL/NPlus/{props.ma => monoid.ma} | 31 +++-- matita/contribs/RELATIONAL/Zah/setoid.ma | 4 +- 11 files changed, 305 insertions(+), 52 deletions(-) create mode 100644 matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma rename matita/contribs/LAMBDA-TYPES/Unified-Sub/{Context/defs.ma => datatypes/Context.ma} (92%) rename matita/contribs/LAMBDA-TYPES/Unified-Sub/{Term/defs.ma => datatypes/Term.ma} (96%) create mode 100644 matita/contribs/RELATIONAL/NPlus/fun.ma rename matita/contribs/RELATIONAL/NPlus/{props.ma => monoid.ma} (81%) 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/Context/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma similarity index 92% rename from matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma rename to matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma index 4da3c95d7..844b19c34 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Context/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Context/defs". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Context". (* FLAT CONTEXTS - Naming policy: - contexts: c d *) -include "Term/defs.ma". +include "datatypes/Term.ma". inductive Context: Set \def | leaf: Context diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma similarity index 96% rename from matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma rename to matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma index e0b165e4f..ba37390d9 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Term/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Term/defs". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term". (* POLARIZED TERMS - Naming policy: 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/props.ma b/matita/contribs/RELATIONAL/NPlus/monoid.ma similarity index 81% rename from matita/contribs/RELATIONAL/NPlus/props.ma rename to matita/contribs/RELATIONAL/NPlus/monoid.ma index 43966337b..804485e54 100644 --- a/matita/contribs/RELATIONAL/NPlus/props.ma +++ b/matita/contribs/RELATIONAL/NPlus/monoid.ma @@ -12,19 +12,11 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/RELATIONAL/NPlus/props". +set "baseuri" "cic:/matita/RELATIONAL/NPlus/monoid". -include "NPlus/inv.ma". +include "NPlus/fun.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. +(* Monoidal properties ******************************************************) theorem nplus_zero_1: \forall q. zero + q == q. intros. elim q; clear q; auto. @@ -35,15 +27,22 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to intros. elim H; clear H q r; auto. qed. -theorem nplus_comm: \forall p,q,r. (p + q == r) \to q + p == r. +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 *) +(* 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: \forall p1,q,r1. (p1 + q == r1) \to - \forall p2,r2. (p2 + q == r2) \to - \forall s. (p1 + r2 == s) \to (p2 + r1 == s). +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. 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 +*) -- 2.39.2