From: Ferruccio Guidi Date: Tue, 5 Aug 2014 20:49:04 +0000 (+0000) Subject: - basic_2: reaxiomatized snv with improved cpds and cpes simplifies preservation X-Git-Tag: make_still_working~864 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c2211ba58807254e75c6321cbd688db462d80fd2;p=helm.git - basic_2: reaxiomatized snv with improved cpds and cpes simplifies preservation - alpha_1: first commit - ground_2/lib: one addition - Makefile: improved contrib generation --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 2945fc62c..15c38d009 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -34,7 +34,8 @@ CONTRIB := lambdadelta_2 TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib -PACKAGES := ground_2 basic_2 apps_2 +PACKAGES := ground_2 basic_2 apps_2 alpha_1 +XPACKAGES := ground_2 basic_2 LDWS := $(shell find -name "*.ldw.xml") TBLS := $(shell find -name "*.tbl") @@ -59,6 +60,14 @@ endef $(foreach PKG, $(PACKAGES), $(eval $(call MAS_TEMPLATE,$(PKG)))) +# XMAS ####################################################################### + +define XMAS_TEMPLATE + XMAS += $$(MAS_$(1)) +endef + +$(foreach PKG, $(XPACKAGES), $(eval $(call XMAS_TEMPLATE,$(PKG)))) + # xoa ######################################################################## xoa: $(XOA_TARGETS) @@ -239,7 +248,7 @@ trim: $(TRIMS:%=%.trimmed) contrib: @echo " TAR -czf $(CONTRIB).tar.gz root *.ma" - $(H)tar -czf $(CONTRIB).tar.gz root $(MAS) + $(H)tar -czf $(CONTRIB).tar.gz root $(XMAS) ############################################################################## diff --git a/matita/matita/contribs/lambdadelta/alpha_1/grammar/item.ma b/matita/matita/contribs/lambdadelta/alpha_1/grammar/item.ma new file mode 100644 index 000000000..01a767223 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/grammar/item.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* THE FORMAL SYSTEM α: MATITA SOURCE FILES + * Initial invocation : - Patience on me to gain peace and perfection! - + * Developed since : 2014 July 25 + *) + +include "ground_2/lib/bool.ma". +include "ground_2/lib/arith.ma". + +(* ITEMS ********************************************************************) + +(* unary items *) +inductive item1: Type[0] ≝ + | Char: nat → item1 (* character: starting at 0 *) + | LRef: nat → item1 (* reference by index: starting at 0 *) + | GRef: nat → item1 (* reference by position: starting at 0 *) + | Decl: item1 (* global abstraction *) +. + +(* binary items *) +inductive item2: Type[0] ≝ + | Abst: item2 (* local abstraction *) + | Abbr: bool → item2 (* local (Ⓣ) or global (Ⓕ) abbreviation *) + | Proj: bool → item2 (* local (Ⓣ) or global (Ⓕ) projection *) +. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/grammar/term.ma b/matita/matita/contribs/lambdadelta/alpha_1/grammar/term.ma new file mode 100644 index 000000000..9562d4c40 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/grammar/term.ma @@ -0,0 +1,80 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/constructors/snitem2_3.ma". +include "basic_2/notation/constructors/star_0.ma". +include "basic_2/notation/constructors/snabstpos_2.ma". +include "basic_2/notation/constructors/snabbr_3.ma". +include "basic_2/notation/constructors/snabbrpos_2.ma". +include "basic_2/notation/constructors/snabbrneg_2.ma". +include "alpha_1/notation/constructors/snitem1_2.ma". +include "alpha_1/notation/constructors/snstar_2.ma". +include "alpha_1/notation/constructors/snlref_2.ma". +include "alpha_1/notation/constructors/sngref_2.ma". +include "alpha_1/notation/constructors/snabstneg_1.ma". +include "alpha_1/notation/constructors/snproj_3.ma". +include "alpha_1/notation/constructors/snprojpos_2.ma". +include "alpha_1/notation/constructors/snprojneg_2.ma". +include "alpha_1/grammar/item.ma". + +(* TERMS ********************************************************************) + +(* terms *) +inductive term: Type[0] ≝ + | TAtom: term (* atomic item construction *) + | TUnit: item1 → term → term (* unary item construction *) + | TPair: item2 → term → term → term (* binary item construction *) +. + +interpretation "top (term)" + 'Star = TAtom. + +interpretation "term construction (unary)" + 'SnItem1 I T = (TUnit I T). + +interpretation "term construction (binary)" + 'SnItem2 I T1 T2 = (TPair I T1 T2). + +interpretation "character (term)" + 'SnStar k T = (TUnit (Char k) T). + +interpretation "local reference (term)" + 'SnLRef i T = (TUnit (LRef i) T). + +interpretation "global reference (term)" + 'SnGRef p T = (TUnit (GRef p) T). + +interpretation "negative abbreviation (term)" + 'SnAbbrNeg T = (TUnit Decl T). + +interpretation "positive abstraction (term)" + 'SnAbstPos T1 T2 = (TPair Abst T1 T2). + +interpretation "abbreviation (term)" + 'SnAbbr a T1 T2 = (TPair (Abbr a) T1 T2). + +interpretation "positive abbreviation (term)" + 'SnAbbrPos T1 T2 = (TPair (Abbr true) T1 T2). + +interpretation "negative abbreviation (term)" + 'SnAbbrNeg T1 T2 = (TPair (Abbr false) T1 T2). + +interpretation "projection (term)" + 'SnProj a T1 T2 = (TPair (Proj a) T1 T2). + +interpretation "positive projection (term)" + 'SnProjPos T1 T2 = (TPair (Proj true) T1 T2). + +interpretation "negative projection (term)" + 'SnProjNeg T1 T2 = (TPair (Proj false) T1 T2). diff --git a/matita/matita/contribs/lambdadelta/alpha_1/grammar/term_append.ma b/matita/matita/contribs/lambdadelta/alpha_1/grammar/term_append.ma new file mode 100644 index 000000000..98ce3bafd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/grammar/term_append.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "alpha_1/grammar/term.ma". + +(* TERMS ********************************************************************) + +let rec tappend T U on T ≝ match T with +[ TAtom ⇒ U +| TUnit I T ⇒ ①{I}.(tappend T U) +| TPair I V T ⇒ ②{I}V.(tappend T U) +]. + +interpretation "append (term)" 'Append T U = (tappend T U). diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snabstneg_1.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snabstneg_1.ma new file mode 100644 index 000000000..a82ce4605 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snabstneg_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( - 𝛌 . break term 55 T )" + non associative with precedence 55 + for @{ 'SnAbstNeg $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/sngref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/sngref_2.ma new file mode 100644 index 000000000..f28b669d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/sngref_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( § term 90 p . break term 55 T )" + non associative with precedence 55 + for @{ 'SnGRef $p $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snitem1_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snitem1_2.ma new file mode 100644 index 000000000..cef7a31fa --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snitem1_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( ① { term 46 I } . break term 55 T )" + non associative with precedence 55 + for @{ 'SnItem1 $I $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snlref_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snlref_2.ma new file mode 100644 index 000000000..4f9311f1e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snlref_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( # term 90 i . break term 55 T )" + non associative with precedence 55 + for @{ 'SnLRef $i $T }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snproj_3.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snproj_3.ma new file mode 100644 index 000000000..3e985c331 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snproj_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( 𝛑 { term 46 a } break term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnProj $a $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojneg_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojneg_2.ma new file mode 100644 index 000000000..c29417e3c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojneg_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( - 𝛑 term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnProjNeg $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojpos_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojpos_2.ma new file mode 100644 index 000000000..74a573d60 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snprojpos_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( + 𝛑 term 55 T1 . break term 55 T2 )" + non associative with precedence 55 + for @{ 'SnProjPos $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snstar_2.ma b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snstar_2.ma new file mode 100644 index 000000000..b4e1e0dac --- /dev/null +++ b/matita/matita/contribs/lambdadelta/alpha_1/notation/constructors/snstar_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM α *****************************************) + +notation "hvbox( ⋆ term 90 k . break term 55 T )" + non associative with precedence 55 + for @{ 'SnStar $k $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma index bf329f737..a2eb23483 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma @@ -12,36 +12,47 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/dpredstar_6.ma". +include "basic_2/notation/relations/dpredstar_7.ma". include "basic_2/static/da.ma". include "basic_2/unfold/lstas.ma". include "basic_2/computation/cprs.ma". (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) -definition cpds: ∀h. sd h → relation4 genv lenv term term ≝ - λh,g,G,L,T1,T2. - ∃∃T,l1,l2. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2. +definition cpds: ∀h. sd h → nat → relation4 genv lenv term term ≝ + λh,g,l2,G,L,T1,T2. + ∃∃T,l1. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2. interpretation "decomposed extended parallel computation (term)" - 'DPRedStar h g G L T1 T2 = (cpds h g G L T1 T2). + 'DPRedStar h g l G L T1 T2 = (cpds h g l G L T1 T2). (* Basic properties *********************************************************) lemma sta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T → - ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/3 width=7 by sta_lstas, ex4_3_intro/ qed. + ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 1] T2. +/3 width=6 by sta_lstas, ex4_2_intro/ qed. -lemma lstas_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/2 width=7 by ex4_3_intro/ qed. +lemma lstas_cpds: ∀h,g,G,L,T1,T2,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → + ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2] T2. +/2 width=6 by ex4_2_intro/ qed. -lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -/2 width=7 by lstar_O, ex4_3_intro/ qed. +lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 → + ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2. +/2 width=6 by lstar_O, ex4_2_intro/ qed. -lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g] T. +lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g, 0] T. /2 width=2 by cprs_cpds/ qed. -lemma cpds_strap1: ∀h,g,G,L,T1,T,T2. - ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -#h #g #G #L #T1 #T #T2 * /3 width=9 by cprs_strap1, ex4_3_intro/ +lemma cpds_strap1: ∀h,g,G,L,T1,T,T2,l. + ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2. +#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_strap1, ex4_2_intro/ qed. + +(* Basic forward lemmas *****************************************************) + +lemma cpds_fwd_cprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2 → + ⦃G, L⦄ ⊢ T1 ➡* T2. +#h #g #G #L #T1 #T2 * +#T #l #_ #_ #H lapply (lstas_inv_O … H) -l -H +#H destruct // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma index 1c45e715b..8cc7d146e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma @@ -20,6 +20,6 @@ include "basic_2/computation/cpds.ma". (* Properties on atomic arity assignment for terms **************************) -lemma cpds_aaa_conf: ∀h,g,G,L. Conf3 … (aaa G L) (cpds h g G L). -#h #g #G #L #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/ +lemma cpds_aaa_conf: ∀h,g,G,L,l. Conf3 … (aaa G L) (cpds h g l G L). +#h #g #G #L #l #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma index 9bd6b2d87..d09fe1ebb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma @@ -21,55 +21,72 @@ include "basic_2/computation/cpds.ma". (* Advanced properties ******************************************************) -lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2. -#h #g #G #L #T1 #T #T2 #l #Hl #HT1 * -#T0 #l0 #l1 #Hl10 #HT #HT0 #HT02 -lapply (da_sta_conf … HT1 … Hl) ≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. -#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H -@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/ -qed-. - -fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. -#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H -@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ -qed-. - -fact da_cpcs_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → - ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 → - ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2. -#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H -elim (cpcs_inv_cprs … H) -H /4 width=18 by da_cprs_lpr_aux, da_mono/ -qed-. - -fact sta_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •[h] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #H01 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12 -elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) -H01 -Hl -HT12 -HL12 -/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/ -qed-. - -fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=10 by/ ] -#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 -elim (IHT1 L1) // -IHT1 #U #HTU #HU1 -elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 -[2: /3 width=12 by da_cprs_lpr_aux/ -|3: /3 width=10 by snv_cprs_lpr_aux/ -|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/ -] -G0 -L0 -T0 -T1 -T -l1 -/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ -qed-. - -fact lstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → - ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 → - ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1 -elim (lstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0 -lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ -qed-. - -fact snv_sta_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → - ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → - ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → - ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g]. -/3 width=8 by lstas_inv_SO, sta_lstas/ qed-. - -fact lstas_cpds_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → - ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2. -#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2 -lapply (da_mono … H … Hl1) -H #H destruct -lapply (lstas_da_conf … HTU1 … Hl1) #Hl12 -elim (le_or_ge l2 l) #Hl2 -[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T - /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/ -| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l - lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 - elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) -IH3 -IH2 -IH1 -Hl1l -HTU1 -HTT2 - /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l, ex3_2_intro/ -] -qed-. - -fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. -#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 -elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12 -lapply (IH2 … H01 … Hl1 … HT12 … HL12) -L0 -T0 // -T1 -lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 -lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H -elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma new file mode 100644 index 000000000..6db1060e3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma @@ -0,0 +1,199 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/fpbs_lift.ma". +include "basic_2/computation/fpbg_fleq.ma". +include "basic_2/equivalence/cpes_cpcs.ma". +include "basic_2/equivalence/cpes_cpes.ma". +include "basic_2/dynamic/snv.ma". + +(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) + +(* Inductive premises for the preservation results **************************) + +definition IH_snv_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. + +definition IH_da_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. + +definition IH_lstas_cpr_lpr: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. + +definition IH_snv_lstas: ∀h:sh. sd h → relation3 genv lenv term ≝ + λh,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 → + ∀U. ⦃G, L⦄ ⊢ T •*[h, l2] U → ⦃G, L⦄ ⊢ U ¡[h, g]. + +(* Properties for the preservation results **********************************) + +fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H +@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/ +qed-. + +fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. +#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H +@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ +qed-. + +fact da_cpds_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l1. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → + ∀T2,l2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + l2 ≤ l1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l1-l2. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l1 #Hl1 #T2 #l2 * #T #l0 #Hl20 #H #HT1 #HT2 #L2 #HL12 +lapply (da_mono … H … Hl1) -H #H destruct +lapply (lstas_da_conf … HT1 … Hl1) #Hl12 +lapply (da_cprs_lpr_aux … IH2 IH1 … Hl12 … HT2 … HL12) -IH2 -IH1 -HT2 -HL12 +/3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/ +qed-. + +fact da_cpes_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → + ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 → + ∀l21,l22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → + ∧∧ l21 ≤ l11 & l22 ≤ l12 & l11 - l21 = l12 - l22. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l11 #Hl11 #l12 #Hl12 #l21 #l22 * #T #HT1 #HT2 +elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl11 … HT1 … L) -Hl11 -HT1 // +elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl12 … HT2 … L) -Hl12 -HT2 // +/3 width=7 by da_mono, and3_intro/ +qed-. + +fact lstas_cprs_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=10 by/ ] +#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 +elim (IHT1 L1) // -IHT1 #U #HTU #HU1 +elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 +[2: /3 width=12 by da_cprs_lpr_aux/ +|3: /3 width=10 by snv_cprs_lpr_aux/ +|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/ +] -G0 -L0 -T0 -T1 -T -l1 +/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ +qed-. + +fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. +#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 +elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12 +lapply (IH2 … H01 … HTl1 … HT12 … HL12) -L0 -T0 // -T1 +lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 +lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H +elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/ +qed-. + +fact cpes_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → + ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 → + ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2. +#h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12 +elim (cpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1 +elim (cpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2 +elim (cprs_conf … H1 … H2) -T0 +/3 width=5 by cpds_div, cpds_cprs_trans/ +qed-. + +fact lstas_cpds_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → + ∀l,l1. l1 ≤ l → ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀T1. ⦃G, L⦄ ⊢ T •*[h, l1] T1 → + ∀T2,l2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l2-l1, l1-l2] T2. +#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #l #l1 #Hl1 #HTl #T1 #HT1 #T2 #l2 * #X #l0 #Hl20 #H #HTX #HXT2 +lapply (da_mono … H … HTl) -H #H destruct +lapply (lstas_da_conf … HT1 … HTl) #HTl1 +lapply (lstas_da_conf … HTX … HTl) #HXl +lapply (da_cprs_lpr_aux … IH3 IH2 … HXl … HXT2 L ?) +[1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTl2 +elim (le_or_ge l1 l2) #Hl12 >(eq_minus_O … Hl12) +[ /5 width=3 by cpds_refl, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro, ex2_intro/ +| lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1 + elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXl … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXl -HXT1 -HXT2 + /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l/ +] +qed-. + +fact cpes_le_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → + ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 → + ∀l21,l22,l. l21 + l ≤ l11 → l22 + l ≤ l12 → + ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21+l, l22+l] T2. +#h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #l11 #Hl11 #Hl12 #Hl12 #l21 #l22 #l #H1 #H2 * #T0 #HT10 #HT20 +elim (da_inv_sta … Hl11) #X1 #HTX1 +elim (lstas_total … HTX1 (l21+l)) -X1 #X1 #HTX1 +elim (da_inv_sta … Hl12) #X2 #HTX2 +elim (lstas_total … HTX2 (l22+l)) -X2 #X2 #HTX2 +lapply (lstas_cpds_aux … IH4 IH3 IH2 IH1 … Hl11 … HTX1 … HT10) -HT10 +[1,2,3: // | >eq_minus_O [2: // ] eq_minus_O [2: // ] (plus_minus_m_m l1 1) in Hl1; // -H1 #Hl1 + lapply (IH1 … HV1 … Hl1 … HV12 … HL12) -HV1 -Hl1 -HV12 [ /2 by fqup_fpbg/ ] + lapply (IH1 … Hl0 … HW2 … HL12) -Hl0 /2 width=1 by fqup_fpbg/ -HW + lapply (IH1 … HU … Hl … HU2 (L2.ⓛW2) ?) -IH1 -HU -Hl -HU2 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2 /4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/ - | #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH3 -IH2 -V -W0 -T0 -l0 -HV1 -HVW1 + | #b #V0 #V2 #W #W2 #U #U2 #HV10 #HV02 #HW2 #HU2 #H1 #H2 destruct -IH3 -IH2 -b1 -V0 -W1 -U1 -l1 -HV1 elim (snv_inv_bind … HT1) -HT1 #_ lapply (da_inv_bind … Hl) -Hl /5 width=9 by da_bind, da_flat, fqup_fpbg, lpr_pair/ ] | #W1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 - elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1 + elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1 lapply (da_inv_flat … H2) -H2 #Hl elim (cpr_inv_cast1 … H3) -H3 [ * #W2 #T2 #HW12 #HT12 #H destruct /4 width=7 by da_flat, fqup_fpbg/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma index 7ddb258b4..d8fb8d161 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) +include "basic_2/multiple/fqus_alt.ma". include "basic_2/computation/cpds_lift.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -36,18 +36,16 @@ lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,d,e. ⇩[s, d | #a #I #G #K #V #T #_ #_ #IHV #IHT #L #s #d #e #HLK #X #H elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=5 by snv_bind, drop_skip/ -| #a #G #K #V #V0 #V1 #T #T1 #l #_ #_ #Hl #HV0 #HV01 #HT1 #IHV #IHT #L #s #d #e #HLK #X #H +| #a #G #K #V #W0 #T #U0 #l #_ #_ #HVW0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct - elim (lift_total V0 d e) #W0 #HVW0 - elim (lift_total V1 d e) #W1 #HVW1 - elim (lift_total T1 (d+1) e) #U1 #HTU1 - @(snv_appl … a … W0 … W1 … U1 l) - [1,2,3,4,5: /2 width=10 by cprs_lift, sta_lift, da_lift/ ] - @(cpds_lift … HT1 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typecjhecker failure *) -| #G #K #V0 #T #V #l #_ #_ #Hl #HTV #HV0 #IHV0 #IHT #L #s #d #e #HLK #X #H - elim (lift_inv_flat1 … H) -H #W0 #U #HVW0 #HTU #H destruct - elim (lift_total V d e) - /3 width=12 by snv_cast, cpcs_lift, sta_lift, da_lift/ + elim (lift_total W0 d e) #W1 #HW01 + elim (lift_total U0 (d+1) e) #U1 #HU01 + @(snv_appl … a … W1 … U1 l) [1,2,3: /2 width=10 by cpds_lift/ ] -IHV -IHT + @(cpds_lift … HTU0 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typechecker failure *) +| #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H + elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct + elim (lift_total U0 d e) + /3 width=12 by snv_cast, cprs_lift, cpds_lift/ ] qed. @@ -66,25 +64,23 @@ lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[ | #a #I #G #L #W #U #_ #_ #IHW #IHU #K #s #d #e #HLK #X #H elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=5 by snv_bind, drop_skip/ -| #a #G #L #W #W0 #W1 #U #U1 #l #_ #_ #Hl #HW0 #HW01 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H +| #a #G #L #W #W1 #U #U1 #l #_ #_ #HW1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H + elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct + elim (cpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0 + elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0 + elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct + lapply (lift_inj … HY … HW01) -HY #H destruct + /3 width=6 by snv_appl/ +| #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct - lapply (da_inv_lift … Hl … HLK … HVW) -Hl #Hl - elim (sta_inv_lift1 … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0 - elim (cprs_inv_lift1 … HW01 … HLK … HVW0) -W0 #V1 #HVW1 #HV01 - elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU - elim (lift_inv_bind2 … H) -H #Y #T1 #HY #HTU1 #H destruct - lapply (lift_inj … HY … HVW1) -HY #H destruct - /3 width=8 by snv_appl/ -| #G #L #W0 #U #W #l #_ #_ #Hl #HUW #HW0 #IHW0 #IHU #K #s #d #e #HLK #X #H - elim (lift_inv_flat2 … H) -H #V0 #T #HVW0 #HTU #H destruct - lapply (da_inv_lift … Hl … HLK … HTU) -Hl #Hl - elim (sta_inv_lift1 … HUW … HLK … HTU) -HUW #V #HVW #HTV - lapply (cpcs_inv_lift G … HLK … HVW … HVW0 ?) // -W - /3 width=8 by snv_cast/ + elim (cprs_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0 + elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0 + lapply (lift_inj … HX … HU01) -HX #H destruct + /3 width=5 by snv_cast/ ] qed-. -(* Advanced properties ******************************************************) +(* Properties on subclosure *************************************************) lemma snv_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g]. @@ -102,3 +98,21 @@ lemma snv_fqu_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2 ] ] qed-. + +lemma snv_fquq_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_inv_gen … H) -H [|*] +/2 width=5 by snv_fqu_conf/ +qed-. + +lemma snv_fqup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=5 by fqup_strap1, snv_fqu_conf/ +qed-. + +lemma snv_fqus_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ¡[h, g] → ⦃G2, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_gen … H) -H [|*] +/2 width=5 by snv_fqup_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 754c8da4a..3c93fd3fc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -13,7 +13,8 @@ (**************************************************************************) include "basic_2/dynamic/snv_lift.ma". -include "basic_2/dynamic/snv_cpcs.ma". +include "basic_2/dynamic/snv_aaa.ma". +include "basic_2/dynamic/snv_cpes.ma". include "basic_2/dynamic/lsubsv_snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -50,82 +51,68 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, drop_drop/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1 + elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #l0 #HV1 #HT1 #HVW1 #HTU1 elim (cpr_inv_appl1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 - lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0 - elim (sta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12 - elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H - elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct - lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10 - lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 - lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 - elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 - lapply (cpds_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) + elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV + elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H + elim (cprs_inv_abst1 … H) -H #XW #U2 #HXW #_ #H destruct -IH1 -IH3 -IH2 -L1 + elim (cprs_conf … HXV … HXW) -W1 #W2 #HXV #HXW + lapply (cpds_cprs_trans … HVW2 … HXV) -XV + lapply (cpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?) /2 width=7 by snv_appl, cprs_bind/ - | #b #V2 #W20 #W2 #T20 #T2 #HV12 #HW202 #HT202 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 - elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 - lapply (cprs_div … HW10 … HW230) -W30 #HW120 - lapply (snv_sta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10 - lapply (da_sta_conf … HVW1 … Hl0) (plus_minus_m_m l 1) in HV1l; // -Hl #HV1l + lapply (cpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20 + lapply (IH2 … HV1l … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1l #HV2l + lapply (IH2 … HW10l … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10l #HW20l + lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 + lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10 #HW20 + lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 #HT20 + @snv_bind /2 width=1 by snv_cast_cpes/ + @(lsubsv_snv_trans … HT20) -HT20 + @(lsubsv_beta … (l-1)) // + @hsnv_cast [1,2: // ] #l0 #Hl0 + lapply (cpes_le_aux … IH4 IH1 IH2 IH3 … HW20l … HV2l … l0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20l -HV2l -HVW20 + /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4 elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0 elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct - lapply (lpr_cprs_conf … HL12 … HW10) -HW10 #HW10 - elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HTU2 #H - elim (cprs_inv_abst1 … H) -H #W #U2 #HW1 #_ #H destruct -U3 - elim (sta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2 - lapply (cpcs_canc_sn … H2 HW10) -W10 #H2 - elim (lift_total X 0 1) #W20 #H3 - lapply (sta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=2 by drop_drop/ -H1 #HVW20 - lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=2 by drop_drop/ -HW13 -H3 -H2 #HW320 - lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20 - elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3 - lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2 - lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0 - lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=2 by drop_drop/ -Hl0 #Hl0 - lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2 - lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0 + elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1 + elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H + elim (cprs_inv_abst1 … H) -H #W #U2 #HW3 #_ #H destruct -U3 + lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2 + lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0 lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2 - lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, drop_drop/ + lapply (snv_lift … HV0 (L2.ⓓW2) (Ⓕ) … HV02) /2 width=1 by drop_drop/ -HV0 #HV2 + elim (lift_total XV 0 1) #XW #HXVW + lapply (cpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2 + lapply (cprs_lift … HXVW1 (L2.ⓓW2) (Ⓕ) … HW13 … HXVW) /2 width=1 by drop_drop/ -W1 -XV #HXW3 + elim (cprs_conf … HXW3 … HW3) -W3 #W3 #HXW3 #HW3 + lapply (cpds_cprs_trans … HXWV2 … HXW3) -XW + lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W + /3 width=6 by snv_appl, snv_bind/ ] | #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 - elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1 + elim (snv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1 elim (cpr_inv_cast1 … H2) -H2 [ * #W2 #T2 #HW12 #HT12 #H destruct - lapply (cpcs_cprs_strap1 … HUW1 W2 ?) /2 width=1 by cpr_cprs/ -HUW1 #H1 - lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ -HW1 -HW12 #HW2 - lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH1 #HT2 - elim (sta_cpr_lpr_aux … IH3 … Hl0 … HTU1 … HT12 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HTU1 #U2 #HTU2 #HU12 - lapply (IH2 … Hl0 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -HT1 -HT12 -Hl0 #Hl0 - /4 width=7 by snv_cast, lpr_cpcs_conf, cpcs_canc_sn/ - | #H -IH3 -IH2 -HW1 -HTU1 -HUW1 + elim (snv_fwd_da … HW1) #l #HW1l + lapply (cpds_div … W1 … 0 … HTU1) /2 width=2 by cprs_cpds/ -U1 -l #HWT1 + lapply (cpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/ + lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ + lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -L1 + /2 width=1 by snv_cast_cpes/ + | #H -IH3 -IH2 -HW1 -U1 lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma index de2cf0d7a..4213293b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/dynamic/snv_lift.ma". -include "basic_2/dynamic/snv_cpcs.ma". +include "basic_2/dynamic/snv_cpes.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -45,18 +45,15 @@ fact snv_lstas_aux: ∀h,g,G0,L0,T0. lapply (da_inv_bind … Hl1) -Hl1 #Hl1 elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/ | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 + elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #l0 #HV1 #HT1 #HVW1 #HTU1 lapply (da_inv_flat … Hl1) -Hl1 #Hl1 - elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct - lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1 - elim (lstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2 - elim (lstas_inv_bind1 … H) -H #U0 #_ #H destruct -T0 -l - elim (cpes_inv_abst2 … HU10) -HU10 #W2 #U2 #HU12 #HU02 - elim (cprs_inv_abst … HU02) -HU02 #HW02 #_ - /3 width=7 by snv_appl, cprs_trans/ -| #W1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 + elim (lstas_inv_appl1 … H2) -H2 #T0 #HT10 #H destruct + lapply (IH1 … HT1 … Hl1 … HT10) /2 width=1 by fqup_fpbg/ #HT0 + lapply (lstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #H + elim (cpes_inv_abst2 … H) -H /3 width=6 by snv_appl, cpds_cprs_trans/ +| #U1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 [ lapply (lstas_inv_O … H2) -H2 #H destruct // ] - elim (snv_inv_cast … H1) -H1 + elim (snv_inv_cast … H1) -H1 lapply (da_inv_flat … Hl1) -Hl1 lapply (lstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma index 476a420f8..a974f248f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/computation/cpds_cpds.ma". include "basic_2/dynamic/snv_aaa.ma". -include "basic_2/dynamic/snv_cpcs.ma". +include "basic_2/dynamic/snv_cpes.ma". include "basic_2/dynamic/lsubsv_lstas.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -76,56 +75,46 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, drop_drop, ex2_intro/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10 + elim (snv_inv_appl … H1) -H1 #a #W1 #U1 #l0 #HV1 #HT1 #HVW1 #HTU1 lapply (da_inv_flat … Hl1) -Hl1 #Hl1 - elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct + elim (lstas_inv_appl1 … H2) -H2 #X #HT1U #H destruct elim (cpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH4 -IH3 -IH2 - elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 + [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -U1 -HV1 -IH4 -IH3 -IH2 + elim (IH1 … Hl1 … HT1U … HT12 … HL12) -IH1 -Hl1 -HT1U /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lstas_appl, ex2_intro/ | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2 lapply (da_inv_bind … Hl1) -Hl1 #Hl1 - elim (lstas_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct - elim (cpds_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW20 #_ #H destruct - lapply (cprs_div … HW10 … HW20) -W0 #HW12 - lapply (da_sta_conf … HVW1 … Hl0) (plus_minus_m_m l 1) in HV1l; // -H #HV1l + lapply (cpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32 lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3 - lapply (IH2 … Hl … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3l - elim (IH1 … Hl1 … HTU2 … HT23 (L2.ⓛW3)) -HTU2 /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23 - lapply (cpcs_cpr_strap1 … HW12 … HW23) #H - lapply (lpr_cpcs_conf … HL12 … H) -H #H - lapply (cpcs_canc_sn … HW14 H) -H #HW43 + lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 + lapply (IH2 … HW2l … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2l #HW3l + lapply (IH2 … HV1l … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV1l #HV2l + elim (IH1 … Hl1 … HT2U … HT23 (L2.ⓛW3)) -HT2U /2 width=1 by fqup_fpbg, lpr_pair/ #U3 #HTU3 #HU23 elim (lsubsv_lstas_trans … g … HTU3 … Hl21 … (L2.ⓓⓝW3.V2)) -HTU3 - [ #U4 #HT3U4 #HU43 -HW12 -HW3 -HW3l -W4 -IH2 -IH3 -IH4 + [ #U4 #HT3U4 #HU43 -IH1 -IH2 -IH3 -IH4 -l -l1 -HW3 -HV2 -HT2 @(ex2_intro … (ⓓ{b}ⓝW3.V2.U4)) /2 width=1 by lstas_bind/ -HT3U4 @(cpcs_canc_dx … (ⓓ{b}ⓝW3.V2.U3)) /2 width=1 by cpcs_bind_dx/ -HU43 @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/ /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/ | -U3 - @(lsubsv_beta … l) /3 width=7 by fqup_fpbg/ - #W #W0 #l0 #Hl0 #HV2W #HW30 - lapply (lstas_sta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W - @(lstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) // - [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/ - | /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ - ] + @(lsubsv_beta … (l-1)) /3 width=7 by fqup_fpbg/ + @hsnv_cast [1,2: // ] #l0 #Hl0 + lapply (cpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32 + /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/ | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/ ] - | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -W10 -HV1 -IH4 -IH3 -IH2 + | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -a -l0 -W1 -HV1 -IH4 -IH3 -IH2 elim (snv_inv_bind … HT1) -HT1 #_ #HT0 lapply (da_inv_bind … Hl1) -Hl1 #Hl1 - elim (lstas_inv_bind1 … HTU1) -HTU1 #U0 #HTU0 #H destruct + elim (lstas_inv_bind1 … HT1U) -HT1U #U0 #HTU0 #H destruct elim (IH1 … Hl1 … HTU0 … HT02 (L2.ⓓW2)) -IH1 -Hl1 -HTU0 /2 width=1 by fqup_fpbg, lpr_pair/ -T0 #U2 #HTU2 #HU02 lapply (lpr_cpr_conf … HL12 … HV10) -HV10 #HV10 lapply (lpr_cpr_conf … HL12 … HW02) -L1 #HW02 @@ -136,15 +125,14 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. ] | #W1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH4 -IH3 -IH2 [ lapply (lstas_inv_O … H2) -H2 #H destruct -IH1 -H1 -l1 /4 width=5 by lpr_cpcs_conf, cpr_cpcs_dx, ex2_intro/ ] - elim (snv_inv_cast … H1) -H1 #U1 #l #_ #HT1 #_ #_ #_ -U1 -l + elim (snv_inv_cast … H1) -H1 #U1 #_ #HT1 #_ #_ -U1 lapply (da_inv_flat … Hl1) -Hl1 #Hl1 lapply (lstas_inv_cast1 … H2) -H2 #HTU1 elim (cpr_inv_cast1 … H3) -H3 [ * #U2 #T2 #_ #HT12 #H destruct elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 -HL12 /3 width=3 by fqup_fpbg, lstas_cast, ex2_intro/ - | #HT1X3 - elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12 + | #HT1X3 elim (IH1 … Hl1 … HTU1 … HT1X3 … HL12) -IH1 -Hl1 -HTU1 -HL12 /2 width=3 by fqup_fpbg, ex2_intro/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma index c3e0444d2..1ee74e64a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma @@ -53,94 +53,3 @@ theorem lstas_cpr_lpr: ∀h,g,G,L,T. IH_lstas_cpr_lpr h g G L T. qed-. (* Advanced preservation properties *****************************************) - -lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. -#h #g #G #L1 #T1 #HT1 #T2 #H -@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/ -qed-. - -lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. -#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H -@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/ -qed-. - -lemma da_cpcs: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G, L⦄ ⊢ T2 ¡[h, g] → - ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 → - ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2. -#h #g #G #L #T1 #HT1 #T2 #HT2 #l1 #Hl1 #l2 #Hl2 #H -elim (cpcs_inv_cprs … H) -H /3 width=12 by da_cprs_lpr, da_mono/ -qed-. - -lemma sta_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •[h] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G #L1 #T1 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12 -elim (lstas_cpr_lpr … 1 … Hl U1 … HT12 … HL12) -Hl -HT12 -HL12 -/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/ -qed-. - -lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ] -#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 -elim (IHT1 L1) // -IHT1 #U #HTU #HU1 -elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2 -[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1 -/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ -qed-. - -lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] → - ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 → - ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1 -elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2 -lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ -qed-. - -lemma snv_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → - ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → - ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g]. -/3 width=7 by lstas_inv_SO, sta_lstas, snv_lstas/ qed-. - -lemma lstas_cpds: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → - ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2. -#h #g #G #L #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2 -lapply (da_mono … H … Hl1) -H #H destruct -lapply (lstas_da_conf … HTU1 … Hl1) #Hl12 -elim (le_or_ge l2 l) #Hl2 -[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T // - /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/ -| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l - lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 - elim (lstas_cprs_lpr … Hl1l … HTU1 … HTT2 L) -Hl1l -HTU1 -HTT2 - /3 width=7 by snv_lstas, cpcs_cpes, monotonic_le_minus_l, ex3_2_intro/ -] -qed-. - -lemma cpds_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. -#h #g #G #L1 #T1 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 -elim (lstas_cpr_lpr … Hl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12 -lapply (da_cpr_lpr … Hl1 … HT12 … HL12) // -T1 -lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 -lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H -elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma index 04de244ab..4f9223886 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma @@ -17,7 +17,7 @@ include "basic_2/equivalence/cpcs_cpcs.ma". (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************) -(* Main properties about atomic arity assignment on terms *******************) +(* Main inversion lemmas about atomic arity assignment on terms *************) theorem cpcs_aaa_mono: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌* T2 → ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma index 98a0609d4..41ac80b94 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma @@ -12,36 +12,30 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/dpconvstar_6.ma". -include "basic_2/static/da.ma". -include "basic_2/unfold/lstas.ma". -include "basic_2/equivalence/cpcs.ma". +include "basic_2/notation/relations/dpconvstar_8.ma". +include "basic_2/computation/cpds.ma". (* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) -definition cpes: ∀h. sd h → relation4 genv lenv term term ≝ - λh,g,G,L,T1,T2. - ∃∃T,l1,l2. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ⬌* T2. +definition cpes: ∀h. sd h → nat → nat → relation4 genv lenv term term ≝ + λh,g,l1,l2,G,L,T1,T2. + ∃∃T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T & ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T. interpretation "decomposed extended parallel equivalence (term)" - 'DPConvStar h g G L T1 T2 = (cpes h g G L T1 T2). + 'DPConvStar h g l1 l2 G L T1 T2 = (cpes h g l1 l2 G L T1 T2). (* Basic properties *********************************************************) -lemma sta_cpcs_cpes: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T → - ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2. -/3 width=7 by sta_lstas, ex4_3_intro/ qed. +lemma cpds_div: ∀h,g,G,L,T1,T2,T,l1,l2. + ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] T → ⦃G, L⦄ ⊢ T2 •*➡*[h, g, l2] T → + ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2. +/2 width=3 by ex2_intro/ qed. -lemma lstas_cpes: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2. -/2 width=7 by ex4_3_intro/ qed. +lemma cpes_refl_O_O: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → + ⦃G, L⦄ ⊢ T •*⬌*[h, g, 0, 0] T. +/3 width=3 by cpds_refl, cpds_div/ qed. -lemma cpcs_cpes: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ⬌* T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2. -/2 width=7 by lstar_O, ex4_3_intro/ qed. - -lemma cpes_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*⬌*[h, g] T. -/2 width=2 by cpcs_cpes/ qed. - -lemma cpes_strap1: ∀h,g,G,L,T1,T,T2. - ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2. -#h #g #G #L #T1 #T #T2 * /3 width=9 by cpcs_strap1, ex4_3_intro/ -qed. +lemma cpes_sym: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 → + ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l1] T1. +#h #g #G #L #T1 #T2 #L1 #l2 * /2 width=3 by cpds_div/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_aaa.ma new file mode 100644 index 000000000..6d1ad9fc3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_aaa.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cpds_aaa.ma". +include "basic_2/equivalence/cpes.ma". + +(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) + +(* Main inversion lemmas about atomic arity assignment on terms *************) + +theorem cpes_aaa_mono: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 → + ∀A1. ⦃G, L⦄ ⊢ T1 ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T2 ⁝ A2 → + A1 = A2. +#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2 +lapply (cpds_aaa_conf … HA1 … HT1) -T1 #HA1 +lapply (cpds_aaa_conf … HA2 … HT2) -T2 #HA2 +lapply (aaa_mono … HA1 … HA2) -L -T // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpcs.ma new file mode 100644 index 000000000..569f46b64 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpcs.ma @@ -0,0 +1,39 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cpds_cpds.ma". +include "basic_2/equivalence/cpcs_cpcs.ma". +include "basic_2/equivalence/cpes.ma". + +(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) + +(* Inversion lemmas on parallel equivalence for terms ***********************) + +lemma cpes_inv_lstas_eq: ∀h,g,G,L,T1,T2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 → + ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l1] U1 → + ∀U2. ⦃G, L⦄ ⊢ T2 •*[h, l2] U2 → ⦃G, L⦄ ⊢ U1 ⬌* U2. +#h #g #G #L #T1 #T2 #l1 #l2 * #T #HT1 #HT2 #U1 #HTU1 #U2 #HTU2 +/3 width=8 by cpds_inv_lstas_eq, cprs_div/ +qed-. + +(* Properties on parallel equivalence for terms ***********************) + +lemma cpcs_cpes: ∀h,g,G,L,T1,l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → + ∀U1,l12. l12 ≤ l11 → ⦃G, L⦄ ⊢ T1 •*[h, l12] U1 → + ∀T2,l21. ⦃G, L⦄ ⊢ T2 ▪[h, g] l21 → + ∀U2,l22. l22 ≤ l21 → ⦃G, L⦄ ⊢ T2 •*[h, l22] U2 → + ⦃G, L⦄ ⊢ U1 ⬌* U2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l12, l22] T2. +#h #g #G #L #T1 #l11 #HT1 #U1 #l12 #Hl121 #HTU1 #T2 #l21 #HT2 #U2 #l22 #Hl221 #HTU2 #HU12 +elim (cpcs_inv_cprs … HU12) -HU12 /3 width=6 by cpds_div, ex4_2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpds.ma deleted file mode 100644 index 1c3907ec9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpds.ma +++ /dev/null @@ -1,33 +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 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/cpds.ma". -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/equivalence/cpes.ma". - -(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) - -(* Advanced properties ******************************************************) - -lemma cpds_cpes_dx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g] T2. -#h #g #G #L #T1 #T2 * /3 width=7 by cpcs_cprs_dx, ex4_3_intro/ -qed. - -(* Advanced inversion lemmas ************************************************) - -lemma cpes_inv_abst2: ∀h,g,a,G,L,W1,T1,T. ⦃G, L⦄ ⊢ T •*⬌*[h, g] ⓛ{a}W1.T1 → - ∃∃W2,T2. ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. -#h #g #a #G #L #W1 #T1 #T * #T0 #l #l0 #Hl0 #Hl #HT0 #H -elim (cpcs_inv_abst2 … H) -H /3 width=7 by ex4_3_intro, ex2_2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpes.ma new file mode 100644 index 000000000..3843dcc43 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpes.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "basic_2/computation/cpds_cpds.ma". +include "basic_2/equivalence/cpes.ma". + +(* DECOMPOSED EXTENDED PARALLEL EQUIVALENCE FOR TERMS ***********************) + +(* Advanced inversion lemmas ************************************************) + +lemma cpes_inv_abst2: ∀h,g,a,G,L,T1,T2,W2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] ⓛ{a}W2.T2 → + ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & + ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, g, l2] T. +#h #g #a #G #L #T1 #T2 #W2 #l1 #l2 * #T0 #HT10 #H +elim (cpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/ +qed-. + +(* Advanced properties ******************************************************) + +lemma cpes_refl: ∀h,g,G,L,T,l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 → + ⦃G, L⦄ ⊢ T •*⬌*[h, g, l2, l2] T. +#h #g #G #L #T #l1 #l2 #Hl21 #Hl1 +elim (da_inv_sta … Hl1) #U #HTU +elim (lstas_total … HTU l2) -U /3 width=3 by cpds_div, lstas_cpds/ +qed. + +lemma lstas_cpes_trans: ∀h,g,G,L,T1,l0,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l0 → l1 ≤ l0 → + ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T → + ∀T2,l,l2. ⦃G, L⦄ ⊢ T •*⬌*[h,g,l,l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,g,l1+l,l2] T2. +#h #g #G #L #T1 #l0 #l1 #Hl0 #Hl10 #T #HT1 #T2 #l #l2 * +/3 width=3 by cpds_div, lstas_cpds_trans/ qed-. + +(* Main properties **********************************************************) + +theorem cpes_trans: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T → + ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2. +#h #g #G #L #T1 #T #l1 #l * #X1 #HT1X1 #HTX1 #T2 #l2 * #X2 #HTX2 #HT2X2 +elim (cpds_conf_eq … HTX1 … HTX2) -T -l /3 width=5 by cpds_cprs_trans, cpds_div/ +qed-. + +theorem cpes_canc_sn: ∀h,g,G,L,T,T1,l,l1. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l1] T1 → + ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2. +#h #g #G #L #T #T1 #l #l1 #HT1 +@cpes_trans /2 width=1 by cpes_sym/ (**) (* full auto raises NTypeChecker failure *) +qed-. + +theorem cpes_canc_dx: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T → + ∀T2,l2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2. +#h #g #G #L #T1 #T #l1 #l #HT1 #T2 #l2 #HT2 +@(cpes_trans … HT1) -T1 -l1 /2 width=1 by cpes_sym/ (**) (* full auto raises NTypeChecker failure *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpes.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpes.etc new file mode 100644 index 000000000..96574d2ad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpes.etc @@ -0,0 +1,27 @@ +(* Advanced properties ******************************************************) + +lemma cpds_cpes_dx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T2. +#h #g #G #L #T1 #T2 #l * /3 width=6 by cpcs_cprs_dx, ex4_2_intro/ +qed. + +(* Advanced inversion lemmas ************************************************) + +lemma cpes_inv_abst2: ∀h,g,a,G,L,W1,T1,T,l. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l] ⓛ{a}W1.T1 → + ∃∃W2,T2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l] ⓛ{a}W2.T2 & ⦃G, L⦄ ⊢ ⓛ{a}W1.T1 ➡* ⓛ{a}W2.T2. +#h #g #a #G #L #W1 #T1 #T #l2 * #T0 #l1 #Hl21 #HT #HT0 #H +elim (cpcs_inv_abst2 … H) -H /3 width=6 by ex4_2_intro, ex2_2_intro/ +qed-. + +(****************************************************************************) + +lemma sta_cpcs_cpes: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T → + ⦃G, L⦄ ⊢ T ⬌* T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, 1] T2. +/3 width=6 by sta_lstas, ex4_2_intro/ qed. + +lemma lstas_cpes: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 •*[h, l] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T2. +/2 width=6 by ex4_2_intro/ qed. + +lemma cpes_strap1: ∀h,g,G,L,T1,T,T2,l. + ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T → ⦃G, L⦄ ⊢ T ⬌ T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l] T2. +#h #g #G #L #T1 #T #T2 #l * /3 width=8 by cpcs_strap1, ex4_2_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc new file mode 100644 index 000000000..5185215c6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc @@ -0,0 +1,90 @@ +lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G #L1 #T1 #HT1 #T2 #H +@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/ +qed-. + +lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. +#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H +@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/ +qed-. + +lemma da_cpcs: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L⦄ ⊢ T2 ¡[h, g] → + ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 → + ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2. +#h #g #G #L #T1 #HT1 #T2 #HT2 #l1 #Hl1 #l2 #Hl2 #H +elim (cpcs_inv_cprs … H) -H /3 width=12 by da_cprs_lpr, da_mono/ +qed-. + +lemma sta_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •[h] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •[h] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G #L1 #T1 #HT1 #l #Hl #U1 #HTU1 #T2 #HT12 #L2 #HL12 +elim (lstas_cpr_lpr … 1 … Hl U1 … HT12 … HL12) -Hl -HT12 -HL12 +/3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/ +qed-. + +lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ] +#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 +elim (IHT1 L1) // -IHT1 #U #HTU #HU1 +elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2 +[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1 +/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ +qed-. + +lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] → + ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 → + ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1 +elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2 +lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ +qed-. + +lemma snv_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → + ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → + ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g]. +/3 width=7 by lstas_inv_SO, sta_lstas, snv_lstas/ qed-. + +lemma lstas_cpds: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → + ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → + ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2. +#h #g #G #L #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 * #T #l0 #l #Hl0 #H #HT1T #HTT2 +lapply (da_mono … H … Hl1) -H #H destruct +lapply (lstas_da_conf … HTU1 … Hl1) #Hl12 +elim (le_or_ge l2 l) #Hl2 +[ lapply (lstas_conf_le … HTU1 … HT1T) -HT1T // + /5 width=11 by cpds_cpes_dx, monotonic_le_minus_l, ex3_2_intro, ex4_3_intro/ +| lapply (lstas_da_conf … HT1T … Hl1) #Hl1l + lapply (lstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 + elim (lstas_cprs_lpr … Hl1l … HTU1 … HTT2 L) -Hl1l -HTU1 -HTT2 + /3 width=7 by snv_lstas, cpcs_cpes, monotonic_le_minus_l, ex3_2_intro/ +] +qed-. + +lemma cpds_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. +#h #g #G #L1 #T1 #HT1 #U1 * #W1 #l1 #l2 #Hl21 #Hl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 +elim (lstas_cpr_lpr … Hl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12 +lapply (da_cpr_lpr … Hl1 … HT12 … HL12) // -T1 +lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 +lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H +elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_6.ma deleted file mode 100644 index c71c248f4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_6.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * break [ term 46 h , break term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'DPConvStar $h $g $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma new file mode 100644 index 000000000..cb60c21e6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * break [ term 46 h , break term 46 g , break term 46 l1 , break term 46 l2 ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'DPConvStar $h $g $l1 $l2 $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_6.ma deleted file mode 100644 index 81f85b1fe..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_6.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 h , break term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'DPRedStar $h $g $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma new file mode 100644 index 000000000..cbe3d09e2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 h , break term 46 g , break term 46 l ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'DPRedStar $h $g $l $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma new file mode 100644 index 000000000..a192a58cd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h , break term 46 g , break term 46 l ] )" + non associative with precedence 45 + for @{ 'NativeValid $h $g $l $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma index 484306007..a5ad258f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma @@ -19,10 +19,10 @@ include "basic_2/reduction/cnx_crx.ma". (* Main properties on irreducibility ****************************************) -theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄. +theorem cix_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄. /2 width=6 by cpx_fwd_cix/ qed. (* Main inversion lemmas on irreducibility **********************************) -theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄. +theorem cnx_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄. /2 width=7 by cnx_inv_crx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma index 32b00b4bc..c60891d61 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/lib/bool.ma". include "ground_2/lib/lstar.ma". include "basic_2/notation/relations/rdrop_5.ma". include "basic_2/notation/relations/rdrop_4.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index f95fc0600..293ff42c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -51,7 +51,8 @@ table { } ] [ { "stratified native validity" * } { - [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpcs" + "snv_preserve" * ] + [ "hsnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" "hsnv_aaa" * + [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpes" + "snv_preserve" * ] } ] } @@ -59,7 +60,7 @@ table { class "blue" [ { "equivalence" * } { [ { "decomposed extended equivalence" * } { - [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )" "cpes_cpds" * ] + [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "cpes_aaa" + "cpes_cpcs" + "cpes_cpes" * ] } ] [ { "context-sensitive equivalence" * } { @@ -105,7 +106,7 @@ table { } ] [ { "decomposed extended computation" * } { - [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ] + [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ] } ] [ { "context-sensitive extended computation" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 26898d348..203727730 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -19,6 +19,9 @@ include "ground_2/lib/star.ma". (* Equations ****************************************************************) +lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. +// qed-. + (* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *) lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y. #x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus // diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma index 753fc2712..6054aa308 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma @@ -244,6 +244,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. +(* multiple existental quantifier (7, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) }. + (* multiple existental quantifier (7, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" @@ -264,35 +274,25 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }. -(* multiple existental quantifier (8, 5) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }. - -(* multiple existental quantifier (9, 3) *) +(* multiple existental quantifier (8, 4) *) -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P8) }. + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P7) }. -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P8) }. + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) }. -(* multiple existental quantifier (10, 4) *) +(* multiple existental quantifier (8, 5) *) -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)" +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P8) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P9) }. + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }. -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)" +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P8) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P9) }. + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }. (* multiple disjunction connective (3) *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index 43d1b9366..6a564d40d 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -28,11 +28,11 @@ 6 5 6 6 6 7 + 7 3 7 4 7 7 + 8 4 8 5 - 9 3 - 10 4 3 4 5 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma index a4281da4a..f103fe747 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -202,6 +202,14 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2 interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +(* multiple existental quantifier (7, 3) *) + +inductive ex7_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→Prop) : Prop ≝ + | ex7_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → ex7_3 ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_3 ? ? ? P0 P1 P2 P3 P4 P5 P6). + (* multiple existental quantifier (7, 4) *) inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ @@ -218,29 +226,21 @@ inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). -(* multiple existental quantifier (8, 5) *) - -inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝ - | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). - -(* multiple existental quantifier (9, 3) *) +(* multiple existental quantifier (8, 4) *) -inductive ex9_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8:A0→A1→A2→Prop) : Prop ≝ - | ex9_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → P7 x0 x1 x2 → P8 x0 x1 x2 → ex9_3 ? ? ? ? ? ? ? ? ? ? ? ? +inductive ex8_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→Prop) : Prop ≝ + | ex8_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → P7 x0 x1 x2 x3 → ex8_4 ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (9, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 = (ex9_3 ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8). +interpretation "multiple existental quantifier (8, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). -(* multiple existental quantifier (10, 4) *) +(* multiple existental quantifier (8, 5) *) -inductive ex10_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8,P9:A0→A1→A2→A3→Prop) : Prop ≝ - | ex10_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → P7 x0 x1 x2 x3 → P8 x0 x1 x2 x3 → P9 x0 x1 x2 x3 → ex10_4 ? ? ? ? ? ? ? ? ? ? ? ? ? ? +inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple existental quantifier (10, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 P9 = (ex10_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8 P9). +interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). (* multiple disjunction connective (3) *) diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml new file mode 100644 index 000000000..ede212e41 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -0,0 +1,9 @@ + + +
+ contribs/lambdadelta/ + ground_2/xoa/xoa2 + ground_2/notation/xoa2_notation + basics/pts.ma +
+