From 8ed01fd6a38bea715ceb449bb7b72a46bad87851 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 3 Aug 2013 14:37:51 +0000 Subject: [PATCH] partial commit: "reduction" component --- .../relations/{predsn_2.ma => normal_3.ma} | 4 +- .../{notreducible_4.ma => normal_5.ma} | 4 +- .../{pred_3.ma => notreducible_3.ma} | 4 +- .../notation/relations/notreducible_5.ma | 19 ++ .../basic_2/notation/relations/pred_4.ma | 19 ++ .../basic_2/notation/relations/pred_5.ma | 19 -- .../basic_2/notation/relations/pred_6.ma | 19 ++ .../relations/{normal_2.ma => predsn_3.ma} | 4 +- .../basic_2/notation/relations/predsn_4.ma | 19 -- .../relations/{normal_4.ma => predsn_5.ma} | 4 +- .../basic_2/notation/relations/reducible_2.ma | 19 -- .../{notreducible_2.ma => reducible_3.ma} | 4 +- .../basic_2/notation/relations/reducible_4.ma | 19 -- .../basic_2/notation/relations/reducible_5.ma | 19 ++ .../lambdadelta/basic_2/reduction/cir.ma | 53 ++-- .../basic_2/reduction/cir_append.ma | 8 +- .../lambdadelta/basic_2/reduction/cir_lift.ma | 6 +- .../lambdadelta/basic_2/reduction/cix.ma | 56 ++--- .../basic_2/reduction/cix_append.ma | 4 +- .../lambdadelta/basic_2/reduction/cix_lift.ma | 10 +- .../lambdadelta/basic_2/reduction/cnr.ma | 46 ++-- .../lambdadelta/basic_2/reduction/cnr_cir.ma | 8 +- .../lambdadelta/basic_2/reduction/cnr_crr.ma | 4 +- .../lambdadelta/basic_2/reduction/cnr_lift.ma | 20 +- .../lambdadelta/basic_2/reduction/cnx.ma | 62 ++--- .../lambdadelta/basic_2/reduction/cnx_cix.ma | 8 +- .../lambdadelta/basic_2/reduction/cnx_crx.ma | 4 +- .../lambdadelta/basic_2/reduction/cnx_lift.ma | 14 +- .../lambdadelta/basic_2/reduction/cpr.ma | 227 +++++++++-------- .../lambdadelta/basic_2/reduction/cpr_cir.ma | 18 +- .../lambdadelta/basic_2/reduction/cpr_lift.ma | 40 +-- .../lambdadelta/basic_2/reduction/cpx.ma | 233 +++++++++--------- .../lambdadelta/basic_2/reduction/cpx_cix.ma | 23 +- .../lambdadelta/basic_2/reduction/cpx_lift.ma | 78 +++--- .../lambdadelta/basic_2/reduction/crr.ma | 70 +++--- .../basic_2/reduction/crr_append.ma | 18 +- .../lambdadelta/basic_2/reduction/crr_lift.ma | 12 +- .../lambdadelta/basic_2/reduction/crx.ma | 73 +++--- .../basic_2/reduction/crx_append.ma | 8 +- .../lambdadelta/basic_2/reduction/crx_lift.ma | 10 +- .../lambdadelta/basic_2/reduction/lpr.ma | 40 +-- .../basic_2/reduction/lpr_ldrop.ma | 17 +- .../lambdadelta/basic_2/reduction/lpr_lpr.ma | 226 ++++++++--------- .../lambdadelta/basic_2/reduction/lpx.ma | 45 ++-- .../lambdadelta/basic_2/reduction/lpx_aaa.ma | 31 +-- .../basic_2/reduction/lpx_ldrop.ma | 6 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 20 +- 47 files changed, 839 insertions(+), 835 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{predsn_2.ma => normal_3.ma} (90%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{notreducible_4.ma => normal_5.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{pred_3.ma => notreducible_3.ma} (89%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_4.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{normal_2.ma => predsn_3.ma} (90%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_4.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{normal_4.ma => predsn_5.ma} (87%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_2.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{notreducible_2.ma => reducible_3.ma} (90%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_4.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_2.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma index 500d84a02..c720a11c0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⊢ ➡ break term 46 L2 )" +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐍 break ⦃ term 46 T ⦄ )" non associative with precedence 45 - for @{ 'PRedSn $L1 $L2 }. + for @{ 'Normal $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma index 5401a62a0..56ae56448 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐈 break [ term 46 g ] break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ 𝐍 break [ term 46 h , break term 46 g ] break ⦃ term 46 T ⦄ )" non associative with precedence 45 - for @{ 'NotReducible $h $g $L $T }. + for @{ 'Normal $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma similarity index 89% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma index 318edbab6..627be72ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃G, L⦄ ⊢ break term 46 T1 ➡ break term 46 T2 )" +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐈 break ⦃ term 46 T ⦄ )" non associative with precedence 45 - for @{ 'PRed $L $T1 $T2 }. + for @{ 'NotReducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma new file mode 100644 index 000000000..ad1d1187f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.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 h , break term 46 g ] break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'NotReducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_4.ma new file mode 100644 index 000000000..397ac935f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_4.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 T2 )" + non associative with precedence 45 + for @{ 'PRed $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.ma deleted file mode 100644 index c4094a5ff..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_5.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 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )" - non associative with precedence 45 - for @{ 'PRed $h $g $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma new file mode 100644 index 000000000..1a423e465 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_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 T1 ➡ break [ term 46 h , break term 46 g ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRed $h $g $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_2.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma index 92cfc51d9..d06064a29 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃G, L⦄ ⊢ 𝐍 break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G , break term 46 L1 ⦄ ⊢ ➡ break term 46 L2 )" non associative with precedence 45 - for @{ 'Normal $L $T }. + for @{ 'PRedSn $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_4.ma deleted file mode 100644 index 85c72d454..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_4.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 h, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedSn $h $g $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma index 255531770..206566071 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ 𝐍 break [ term 46 g ] break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )" non associative with precedence 45 - for @{ 'Normal $h $g $L $T }. + for @{ 'PRedSn $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_2.ma deleted file mode 100644 index f5cadce5f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_2.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( ⦃G, L⦄ ⊢ 𝐑 break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'Reducible $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_2.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma index 9659a6e23..c8473ccc3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃G, L⦄ ⊢ 𝐈 break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐑 break ⦃ term 46 T ⦄ )" non associative with precedence 45 - for @{ 'NotReducible $L $T }. + for @{ 'Reducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_4.ma deleted file mode 100644 index 8c84faf31..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_4.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 h, break term 46 L ⦄ ⊢ 𝐑 break [ term 46 g ] break ⦃ term 46 T ⦄ )" - non associative with precedence 45 - for @{ 'Reducible $h $g $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma new file mode 100644 index 000000000..ac8033449 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.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 h , break term 46 g ] break ⦃ term 46 T ⦄ )" + non associative with precedence 45 + for @{ 'Reducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma index d9509e17a..276a8a03a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma @@ -12,45 +12,45 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/notreducible_2.ma". +include "basic_2/notation/relations/notreducible_3.ma". include "basic_2/reduction/crr.ma". (* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) -definition cir: lenv → predicate term ≝ λL,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⊥. +definition cir: relation3 genv lenv term ≝ λG,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⊥. interpretation "context-sensitive irreducibility (term)" - 'NotReducible L T = (cir L T). + 'NotReducible G L T = (cir G L T). (* Basic inversion lemmas ***************************************************) -lemma cir_inv_delta: ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥. +lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥. /3 width=3/ qed-. -lemma cir_inv_ri2: ∀I,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈⦃②{I}V.T⦄ → ⊥. +lemma cir_inv_ri2: ∀I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈⦃②{I}V.T⦄ → ⊥. /3 width=1/ qed-. -lemma cir_inv_ib2: ∀a,I,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → - ⦃G, L⦄ ⊢ 𝐈⦃V⦄ ∧ L.ⓑ{I}V ⊢ 𝐈⦃T⦄. +lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → + ⦃G, L⦄ ⊢ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄. /4 width=1/ qed-. -lemma cir_inv_bind: ∀a,I,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & L.ⓑ{I}V ⊢ 𝐈⦃T⦄ & ib2 a I. +lemma cir_inv_bind: ∀a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ & ib2 a I. #a * [ elim a -a ] -[ #L #V #T #H elim H -H /3 width=1/ -|*: #L #V #T #H elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=1/ -] +#G #L #V #T #H [ elim H -H /3 width=1/ ] +elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=1/ qed-. -lemma cir_inv_appl: ∀L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄. -#L #V #T #HVT @and3_intro /3 width=1/ +lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄. +#G #L #V #T #HVT @and3_intro /3 width=1/ generalize in match HVT; -HVT elim T -T // * // #a * #U #T #_ #_ #H elim H -H /2 width=1/ qed-. -lemma cir_inv_flat: ∀I,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓕ{I}V.T⦄ → +lemma cir_inv_flat: ∀I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓕ{I}V.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl. -* #L #V #T #H +* #G #L #V #T #H [ elim (cir_inv_appl … H) -H /2 width=1/ | elim (cir_inv_ri2 … H) -H /2 width=1/ ] @@ -58,21 +58,22 @@ qed-. (* Basic properties *********************************************************) -lemma cir_sort: ∀L,k. ⦃G, L⦄ ⊢ 𝐈⦃⋆k⦄. -/2 width=3 by crr_inv_sort/ qed. +lemma cir_sort: ∀G,L,k. ⦃G, L⦄ ⊢ 𝐈⦃⋆k⦄. +/2 width=4 by crr_inv_sort/ qed. -lemma cir_gref: ∀L,p. ⦃G, L⦄ ⊢ 𝐈⦃§p⦄. -/2 width=3 by crr_inv_gref/ qed. +lemma cir_gref: ∀G,L,p. ⦃G, L⦄ ⊢ 𝐈⦃§p⦄. +/2 width=4 by crr_inv_gref/ qed. -lemma tir_atom: ∀I. ⋆ ⊢ 𝐈⦃⓪{I}⦄. -/2 width=2 by trr_inv_atom/ qed. +lemma tir_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ 𝐈⦃⓪{I}⦄. +/2 width=3 by trr_inv_atom/ qed. -lemma cir_ib2: ∀a,I,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄. -#a #I #L #V #T #HI #HV #HT #H +lemma cir_ib2: ∀a,I,G,L,V,T. + ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄. +#a #I #G #L #V #T #HI #HV #HT #H elim (crr_inv_ib2 … HI H) -HI -H /2 width=1/ qed. -lemma cir_appl: ∀L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄. -#L #V #T #HV #HT #H1 #H2 +lemma cir_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄. +#G #L #V #T #HV #HT #H1 #H2 elim (crr_inv_appl … H2) -H2 /2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma index b91465fc0..bf68aedee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma @@ -19,16 +19,16 @@ include "basic_2/reduction/cir.ma". (* Advanved properties ******************************************************) -lemma cir_labst_last: ∀L,T,W. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW @@ ⦃G, L⦄ ⊢ 𝐈⦃T⦄. +lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ 𝐈⦃T⦄. /3 width=2 by crr_inv_labst_last/ qed. -lemma cir_tif: ∀T,W. ⋆ ⊢ 𝐈⦃T⦄ → ⋆.ⓛW ⊢ 𝐈⦃T⦄. +lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄. /3 width=2 by crr_inv_trr/ qed. (* Advanced inversion lemmas ************************************************) -lemma cir_inv_append_sn: ∀L,K,T. K @@ ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. +lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. /3 width=1/ qed-. -lemma cir_inv_tir: ∀T,W. ⋆.ⓛW ⊢ 𝐈⦃T⦄ → ⋆ ⊢ 𝐈⦃T⦄. +lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄. /3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma index 0dcd1cb81..8ddf8c33b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma @@ -19,10 +19,10 @@ include "basic_2/reduction/cir.ma". (* Properties on relocation *************************************************) -lemma cir_lift: ∀K,T. K ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → +lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈⦃U⦄. /3 width=7 by crr_inv_lift/ qed. -lemma cir_inv_lift: ∀L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → K ⊢ 𝐈⦃T⦄. +lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈⦃T⦄. /3 width=7/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma index f89a5038d..76d0fd82a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma @@ -12,50 +12,50 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/notreducible_4.ma". +include "basic_2/notation/relations/notreducible_5.ma". include "basic_2/reduction/cir.ma". include "basic_2/reduction/crx.ma". (* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************) -definition cix: ∀h. sd h → lenv → predicate term ≝ λh,g,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⊥. +definition cix: ∀h. sd h → relation3 genv lenv term ≝ + λh,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⊥. interpretation "context-sensitive extended irreducibility (term)" - 'NotReducible h g L T = (cix h g L T). + 'NotReducible h g G L T = (cix h g G L T). (* Basic inversion lemmas ***************************************************) -lemma cix_inv_sort: ∀h,g,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄ → ⊥. +lemma cix_inv_sort: ∀h,g,G,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄ → ⊥. /3 width=2/ qed-. -lemma cix_inv_delta: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥. +lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥. /3 width=4/ qed-. -lemma cix_inv_ri2: ∀h,g,I,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃②{I}V.T⦄ → ⊥. +lemma cix_inv_ri2: ∀h,g,I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃②{I}V.T⦄ → ⊥. /3 width=1/ qed-. -lemma cix_inv_ib2: ∀h,g,a,I,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ → - ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ ∧ ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄. +lemma cix_inv_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ → + ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄. /4 width=1/ qed-. -lemma cix_inv_bind: ∀h,g,a,I,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ & ib2 a I. +lemma cix_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ & ib2 a I. #h #g #a * [ elim a -a ] -[ #L #V #T #H elim H -H /3 width=1/ -|*: #L #V #T #H elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=1/ -] +#G #L #V #T #H [ elim H -H /3 width=1/ ] +elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=1/ qed-. -lemma cix_inv_appl: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄ → +lemma cix_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄. -#h #g #L #V #T #HVT @and3_intro /3 width=1/ +#h #g #G #L #V #T #HVT @and3_intro /3 width=1/ generalize in match HVT; -HVT elim T -T // * // #a * #U #T #_ #_ #H elim H -H /2 width=1/ qed-. -lemma cix_inv_flat: ∀h,g,I,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓕ{I}V.T⦄ → +lemma cix_inv_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓕ{I}V.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄ & I = Appl. -#h #g * #L #V #T #H +#h #g * #G #L #V #T #H [ elim (cix_inv_appl … H) -H /2 width=1/ | elim (cix_inv_ri2 … H) -H /2 width=1/ ] @@ -63,31 +63,31 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma cix_inv_cir: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. +lemma cix_inv_cir: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. /3 width=1/ qed-. (* Basic properties *********************************************************) -lemma cix_sort: ∀h,g,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄. -#h #g #L #k #Hk #H elim (crx_inv_sort … H) -L #l #Hkl +lemma cix_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄. +#h #g #G #L #k #Hk #H elim (crx_inv_sort … H) -L #l #Hkl lapply (deg_mono … Hk Hkl) -h -k (cpr_inv_sort1 … H) // qed. (* Basic_1: was: nf2_abst *) -lemma cnr_abst: ∀a,L,W,T. ⦃G, L⦄ ⊢ 𝐍⦃W⦄ → L.ⓛW ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}W.T⦄. -#a #L #W #T #HW #HT #X #H +lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}W.T⦄. +#a #G #L #W #T #HW #HT #X #H elim (cpr_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct >(HW … HW0) -W0 >(HT … HT0) -T0 // qed. (* Basic_1: was only: nf2_appl_lref *) -lemma cnr_appl_simple: ∀L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄. -#L #V #T #HV #HT #HS #X #H +lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄. +#G #L #V #T #HV #HT #HS #X #H elim (cpr_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct >(HV … HV0) -V0 >(HT … HT0) -T0 // qed. (* Basic_1: was: nf2_dec *) -axiom cnr_dec: ∀L,T1. ⦃G, L⦄ ⊢ 𝐍⦃T1⦄ ∨ +axiom cnr_dec: ∀G,L,T1. ⦃G, L⦄ ⊢ 𝐍⦃T1⦄ ∨ ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). (* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma index 269cd6561..487fd68bb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma @@ -19,10 +19,10 @@ include "basic_2/reduction/cnr_crr.ma". (* Main properties on context-sensitive irreducible terms *******************) -theorem cir_cnr: ∀L,T. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. -/2 width=3 by cpr_fwd_cir/ qed. +theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. +/2 width=4 by cpr_fwd_cir/ qed. (* Main inversion lemmas on context-sensitive irreducible terms *************) -theorem cnr_inv_cir: ∀L,T. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. -/2 width=4 by cnr_inv_crr/ qed-. +theorem cnr_inv_cir: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. +/2 width=5 by cnr_inv_crr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma index c52165e3e..7ee9e1f29 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma @@ -20,8 +20,8 @@ include "basic_2/reduction/cnr.ma". (* Advanced inversion lemmas on context-sensitive reducible terms ***********) (* Note: this property is unusual *) -lemma cnr_inv_crr: ∀L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⊥. -#L #T #H elim H -L -T +lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⊥. +#G #L #T #H elim H -L -T [ #L #K #V #i #HLK #H elim (cnr_inv_delta … HLK H) | #L #V #T #_ #IHV #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma index 8d0267c47..ed4280a6a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma @@ -20,16 +20,16 @@ include "basic_2/reduction/cnr.ma". (* Advanced properties ******************************************************) (* Basic_1: was only: nf2_csort_lref *) -lemma cnr_lref_atom: ∀L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄. -#L #i #HL #X #H +lemma cnr_lref_atom: ∀G,L,i. ⇩[0, i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄. +#G #L #i #HL #X #H elim (cpr_inv_lref1 … H) -H // * #K #V1 #V2 #HLK #_ #_ lapply (ldrop_mono … HL … HLK) -L #H destruct qed. (* Basic_1: was: nf2_lref_abst *) -lemma cnr_lref_abst: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄. -#L #K #V #i #HLK #X #H +lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[0, i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄. +#G #L #K #V #i #HLK #X #H elim (cpr_inv_lref1 … H) -H // * #K0 #V1 #V2 #HLK0 #_ #_ lapply (ldrop_mono … HLK … HLK0) -L #H destruct @@ -38,18 +38,18 @@ qed. (* Relocation properties ****************************************************) (* Basic_1: was: nf2_lift *) -lemma cnr_lift: ∀L0,L,T,T0,d,e. - ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → L0 ⊢ 𝐍⦃T0⦄. -#L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H +lemma cnr_lift: ∀G,L0,L,T,T0,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → + ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄. +#G #L0 #L #T #T0 #d #e #HLT #HL0 #HT0 #X #H elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 <(HLT … HT1) in HT0; -L #HT0 >(lift_mono … HT10 … HT0) -T1 -X // qed. (* Note: this was missing in basic_1 *) -lemma cnr_inv_lift: ∀L0,L,T,T0,d,e. - L0 ⊢ 𝐍⦃T0⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. -#L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H +lemma cnr_inv_lift: ∀G,L0,L,T,T0,d,e. ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄ → + ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. +#G #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H elim (lift_total X d e) #X0 #HX0 lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0 >(HLT0 … HTX0) in HX0; -L0 -X0 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma index 5c97081f5..43562dc93 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/normal_4.ma". +include "basic_2/notation/relations/normal_5.ma". include "basic_2/reduction/cnr.ma". include "basic_2/reduction/cpx.ma". (* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************) -definition cnx: ∀h. sd h → lenv → predicate term ≝ - λh,g,L. NF … (cpx h g L) (eq …). +definition cnx: ∀h. sd h → relation3 genv lenv term ≝ + λh,g,G,L. NF … (cpx h g G L) (eq …). interpretation "context-sensitive extended normality (term)" @@ -27,50 +27,50 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma cnx_inv_sort: ∀h,g,L,k. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄ → deg h g k 0. -#h #g #L #k #H elim (deg_total h g k) +lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄ → deg h g k 0. +#h #g #G #L #k #H elim (deg_total h g k) #l @(nat_ind_plus … l) -l // #l #_ #Hkl lapply (H (⋆(next h k)) ?) -H /2 width=2/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *) lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H) qed-. -lemma cnx_inv_delta: ∀h,g,I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥. -#h #g #I #L #K #V #i #HLK #H +lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥. +#h #g #I #G #L #K #V #i #HLK #H elim (lift_total V 0 (i+1)) #W #HVW lapply (H W ?) -H [ /3 width=7/ ] -HLK #H destruct elim (lift_inv_lref2_be … HVW) -HVW // qed-. -lemma cnx_inv_abst: ∀h,g,a,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓛ{a}V.T⦄ → - ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃h, L.ⓛV⦄ ⊢ 𝐍[h, g]⦃T⦄. -#h #g #a #L #V1 #T1 #HVT1 @conj +lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓛ{a}V.T⦄ → + ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍[h, g]⦃T⦄. +#h #g #a #G #L #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // ] qed-. -lemma cnx_inv_abbr: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃-ⓓV.T⦄ → - ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃h, L.ⓓV⦄ ⊢ 𝐍[h, g]⦃T⦄. -#h #g #L #V1 #T1 #HVT1 @conj +lemma cnx_inv_abbr: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃-ⓓV.T⦄ → + ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍[h, g]⦃T⦄. +#h #g #G #L #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2/ -HT2 #H destruct // ] qed-. -lemma cnx_inv_zeta: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃+ⓓV.T⦄ → ⊥. -#h #g #L #V #T #H elim (is_lift_dec T 0 1) +lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃+ⓓV.T⦄ → ⊥. +#h #g #G #L #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU lapply (H U ?) -H /2 width=3/ #H destruct elim (lift_inv_pair_xy_y … HTU) | #HT - elim (cpr_delift (⋆) V T (⋆.ⓓV) 0) // #T2 #T1 #HT2 #HT12 + elim (cpr_delift G(⋆) V T (⋆.ⓓV) 0) // #T2 #T1 #HT2 #HT12 lapply (H (+ⓓV.T2) ?) -H /5 width=1/ -HT2 #H destruct /3 width=2/ ] qed-. -lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄ → +lemma cnx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ & 𝐒⦃T⦄. -#h #g #L #V1 #T1 #HVT1 @and3_intro +#h #g #G #L #V1 #T1 #HVT1 @and3_intro [ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // | generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H @@ -80,43 +80,43 @@ lemma cnx_inv_appl: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄ → ] qed-. -lemma cnx_inv_tau: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓝV.T⦄ → ⊥. -#h #g #L #V #T #H lapply (H T ?) -H /2 width=1/ #H +lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓝV.T⦄ → ⊥. +#h #g #G #L #V #T #H lapply (H T ?) -H /2 width=1/ #H @discr_tpair_xy_y // qed-. (* Basic forward lemmas *****************************************************) -lemma cnx_fwd_cnr: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. -#h #g #L #T #H #U #HTU +lemma cnx_fwd_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. +#h #g #G #L #T #H #U #HTU @H /2 width=1/ (**) (* auto fails because a δ-expansion gets in the way *) qed-. (* Basic properties *********************************************************) -lemma cnx_sort: ∀h,g,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄. -#h #g #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_ +lemma cnx_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄. +#h #g #G #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_ lapply (deg_mono … Hkl Hk) -h -L (HW … HW0) -W0 >(HT … HT0) -T0 // qed. -lemma cnx_appl_simple: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → 𝐒⦃T⦄ → +lemma cnx_appl_simple: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄. -#h #g #L #V #T #HV #HT #HS #X #H +#h #g #G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct >(HV … HV0) -V0 >(HT … HT0) -T0 // qed. -axiom cnx_dec: ∀h,g,L,T1. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T1⦄ ∨ +axiom cnx_dec: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T1⦄ ∨ ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & (T1 = T2 → ⊥). 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 f45801a25..3e62a5c60 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 context-sensitive extended irreducible terms **********) -theorem cix_cnr: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄. -/2 width=5 by cpx_fwd_cix/ qed. +theorem cix_cnr: ∀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 context-sensitive extended irreducible terms ****) -theorem cnr_inv_cix: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄. -/2 width=6 by cnx_inv_crx/ qed-. +theorem cnr_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/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma index 84951db34..f5d125f08 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma @@ -20,8 +20,8 @@ include "basic_2/reduction/cnx.ma". (* Advanced inversion lemmas on context-sensitive reducible terms ***********) (* Note: this property is unusual *) -lemma cnx_inv_crx: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⊥. -#h #g #L #T #H elim H -L -T +lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⊥. +#h #g #G #L #T #H elim H -L -T [ #L #k #l #Hkl #H lapply (cnx_inv_sort … H) -H #H lapply (deg_mono … H Hkl) -h -L -k (lift_mono … HT10 … HT0) -T1 -X // qed. -lemma cnx_inv_lift: ∀h,g,L0,L,T,T0,d,e. ⦃h, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[d, e] L0 ≡ L → +lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,d,e. ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄. -#h #g #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H +#h #g #G #L0 #L #T #T0 #d #e #HLT0 #HL0 #HT0 #X #H elim (lift_total X d e) #X0 #HX0 lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0 >(HLT0 … HTX0) in HX0; -L0 -X0 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index 69b591178..28b040bf8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -12,46 +12,48 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/pred_3.ma". +include "basic_2/notation/relations/pred_4.ma". +include "basic_2/grammar/genv.ma". include "basic_2/grammar/cl_shift.ma". include "basic_2/relocation/ldrop_append.ma". include "basic_2/substitution/lsubr.ma". (* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) +(* activate genv *) (* Basic_1: includes: pr0_delta1 pr2_delta1 pr2_thin_dx *) (* Note: cpr_flat: does not hold in basic_1 *) -inductive cpr: lenv → relation term ≝ -| cpr_atom : ∀I,L. cpr L (⓪{I}) (⓪{I}) -| cpr_delta: ∀L,K,V,V2,W2,i. - ⇩[0, i] L ≡ K. ⓓV → cpr K V V2 → - ⇧[0, i + 1] V2 ≡ W2 → cpr L (#i) W2 -| cpr_bind : ∀a,I,L,V1,V2,T1,T2. - cpr L V1 V2 → cpr (L.ⓑ{I}V1) T1 T2 → - cpr L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) -| cpr_flat : ∀I,L,V1,V2,T1,T2. - cpr L V1 V2 → cpr L T1 T2 → - cpr L (ⓕ{I} V1. T1) (ⓕ{I}V2.T2) -| cpr_zeta : ∀L,V,T1,T,T2. cpr (L.ⓓV) T1 T → - ⇧[0, 1] T2 ≡ T → cpr L (+ⓓV.T1) T2 -| cpr_tau : ∀L,V,T1,T2. cpr L T1 T2 → cpr L (ⓝV.T1) T2 -| cpr_beta : ∀a,L,V1,V2,W1,W2,T1,T2. - cpr L V1 V2 → cpr L W1 W2 → cpr (L.ⓛW1) T1 T2 → - cpr L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2) -| cpr_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2. - cpr L V1 V → ⇧[0, 1] V ≡ V2 → cpr L W1 W2 → cpr (L.ⓓW1) T1 T2 → - cpr L (ⓐV1.ⓓ{a}W1.T1) (ⓓ{a}W2.ⓐV2.T2) +inductive cpr: relation4 genv lenv term term ≝ +| cpr_atom : ∀I,G,L. cpr G L (⓪{I}) (⓪{I}) +| cpr_delta: ∀G,L,K,V,V2,W2,i. + ⇩[0, i] L ≡ K. ⓓV → cpr G K V V2 → + ⇧[0, i + 1] V2 ≡ W2 → cpr G L (#i) W2 +| cpr_bind : ∀a,I,G,L,V1,V2,T1,T2. + cpr G L V1 V2 → cpr G (L.ⓑ{I}V1) T1 T2 → + cpr G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) +| cpr_flat : ∀I,G,L,V1,V2,T1,T2. + cpr G L V1 V2 → cpr G L T1 T2 → + cpr G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) +| cpr_zeta : ∀G,L,V,T1,T,T2. cpr G (L.ⓓV) T1 T → + ⇧[0, 1] T2 ≡ T → cpr G L (+ⓓV.T1) T2 +| cpr_tau : ∀G,L,V,T1,T2. cpr G L T1 T2 → cpr G L (ⓝV.T1) T2 +| cpr_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2. + cpr G L V1 V2 → cpr G L W1 W2 → cpr G (L.ⓛW1) T1 T2 → + cpr G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2) +| cpr_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. + cpr G L V1 V → ⇧[0, 1] V ≡ V2 → cpr G L W1 W2 → cpr G (L.ⓓW1) T1 T2 → + cpr G L (ⓐV1.ⓓ{a}W1.T1) (ⓓ{a}W2.ⓐV2.T2) . interpretation "context-sensitive parallel reduction (term)" - 'PRed L T1 T2 = (cpr L T1 T2). + 'PRed G L T1 T2 = (cpr G L T1 T2). (* Basic properties *********************************************************) -lemma lsubr_cpr_trans: lsub_trans … cpr lsubr. -#L1 #T1 #T2 #H elim H -L1 -T1 -T2 +lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr. +#G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 [ // -| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 +| #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 elim (lsubr_fwd_ldrop2_abbr … HL12 … HLK1) -L1 * /3 width=6/ |3,7: /4 width=1/ |4,6: /3 width=1/ @@ -60,24 +62,24 @@ lemma lsubr_cpr_trans: lsub_trans … cpr lsubr. qed-. (* Basic_1: was by definition: pr2_free *) -lemma tpr_cpr: ∀T1,T2. ⋆ ⊢ T1 ➡ T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡ T2. -#T1 #T2 #HT12 #L +lemma tpr_cpr: ∀G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡ T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡ T2. +#G #T1 #T2 #HT12 #L lapply (lsubr_cpr_trans … HT12 L ?) // qed. (* Basic_1: includes by definition: pr0_refl *) -lemma cpr_refl: ∀T,L. ⦃G, L⦄ ⊢ T ➡ T. -#T elim T -T // * /2 width=1/ +lemma cpr_refl: ∀G,T,L. ⦃G, L⦄ ⊢ T ➡ T. +#G #T elim T -T // * /2 width=1/ qed. (* Basic_1: was: pr2_head_1 *) -lemma cpr_pair_sn: ∀I,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → +lemma cpr_pair_sn: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡ ②{I}V2.T. * /2 width=1/ qed. -lemma cpr_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓓV) → +lemma cpr_delift: ∀G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓓV) → ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡ T2 & ⇧[d, 1] T ≡ T2. -#K #V #T1 elim T1 -T1 +#G #K #V #T1 elim T1 -T1 [ * #i #L #d #HLK /2 width=4/ elim (lt_or_eq_or_gt i d) #Hid [1,3: /3 width=4/ ] destruct @@ -91,9 +93,9 @@ lemma cpr_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓓV) → ] qed-. -lemma cpr_append: l_appendable_sn … cpr. -#K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/ /2 width=3/ -#K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L +lemma cpr_append: ∀G. l_appendable_sn … (cpr G). +#G #K #T1 #T2 #H elim H -G -K -T1 -T2 // /2 width=1/ /2 width=3/ +#G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L lapply (ldrop_fwd_length_lt2 … HK0) #H @(cpr_delta … (L@@K0) V1 … HVW2) // @(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *) @@ -101,153 +103,147 @@ qed. (* Basic inversion lemmas ***************************************************) -fact cpr_inv_atom1_aux: ∀L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀I. T1 = ⓪{I} → +fact cpr_inv_atom1_aux: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I} ∨ - ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & - K ⊢ V ➡ V2 & - ⇧[O, i + 1] V2 ≡ T2 & - I = LRef i. -#L #T1 #T2 * -L -T1 -T2 -[ #I #L #J #H destruct /2 width=1/ -| #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8/ -| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct -| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct -| #L #V #T1 #T #T2 #_ #_ #J #H destruct -| #L #V #T1 #T2 #_ #J #H destruct -| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #J #H destruct -| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #J #H destruct + ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 & + ⇧[O, i + 1] V2 ≡ T2 & I = LRef i. +#G #L #T1 #T2 * -G -L -T1 -T2 +[ #I #G #L #J #H destruct /2 width=1/ +| #L #G #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8/ +| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct +| #G #L #V #T1 #T #T2 #_ #_ #J #H destruct +| #G #L #V #T1 #T2 #_ #J #H destruct +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #J #H destruct +| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #J #H destruct ] qed-. -lemma cpr_inv_atom1: ∀I,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡ T2 → +lemma cpr_inv_atom1: ∀I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡ T2 → T2 = ⓪{I} ∨ - ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & - K ⊢ V ➡ V2 & - ⇧[O, i + 1] V2 ≡ T2 & - I = LRef i. + ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 & + ⇧[O, i + 1] V2 ≡ T2 & I = LRef i. /2 width=3 by cpr_inv_atom1_aux/ qed-. (* Basic_1: includes: pr0_gen_sort pr2_gen_sort *) -lemma cpr_inv_sort1: ∀L,T2,k. ⦃G, L⦄ ⊢ ⋆k ➡ T2 → T2 = ⋆k. -#L #T2 #k #H +lemma cpr_inv_sort1: ∀G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ➡ T2 → T2 = ⋆k. +#G #L #T2 #k #H elim (cpr_inv_atom1 … H) -H // * #K #V #V2 #i #_ #_ #_ #H destruct qed-. (* Basic_1: includes: pr0_gen_lref pr2_gen_lref *) -lemma cpr_inv_lref1: ∀L,T2,i. ⦃G, L⦄ ⊢ #i ➡ T2 → +lemma cpr_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡ T2 → T2 = #i ∨ - ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV & - K ⊢ V ➡ V2 & + ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡ V2 & ⇧[O, i + 1] V2 ≡ T2. -#L #T2 #i #H +#G #L #T2 #i #H elim (cpr_inv_atom1 … H) -H /2 width=1/ * #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6/ qed-. -lemma cpr_inv_gref1: ∀L,T2,p. ⦃G, L⦄ ⊢ §p ➡ T2 → T2 = §p. -#L #T2 #p #H +lemma cpr_inv_gref1: ∀G,L,T2,p. ⦃G, L⦄ ⊢ §p ➡ T2 → T2 = §p. +#G #L #T2 #p #H elim (cpr_inv_atom1 … H) -H // * #K #V #V2 #i #_ #_ #_ #H destruct qed-. -fact cpr_inv_bind1_aux: ∀L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡ U2 → +fact cpr_inv_bind1_aux: ∀G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡ U2 → ∀a,I,V1,T1. U1 = ⓑ{a,I}V1. T1 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & - L. ⓑ{I}V1 ⊢ T1 ➡ T2 & + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡ T2 & U2 = ⓑ{a,I}V2.T2 ) ∨ - ∃∃T. L.ⓓV1 ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr. -#L #U1 #U2 * -L -U1 -U2 -[ #I #L #b #J #W1 #U1 #H destruct -| #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct -| #a #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /3 width=5/ -| #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct -| #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W #U1 #H destruct /3 width=3/ -| #L #V #T1 #T2 #_ #b #J #W #U1 #H destruct -| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #b #J #W #U1 #H destruct -| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W #U1 #H destruct + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & + a = true & I = Abbr. +#G #L #U1 #U2 * -L -U1 -U2 +[ #I #G #L #b #J #W1 #U1 #H destruct +| #L #G #K #V #V2 #W2 #i #_ #_ #_ #b #J #W #U1 #H destruct +| #a #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W #U1 #H destruct /3 width=5/ +| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W #U1 #H destruct +| #G #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W #U1 #H destruct /3 width=3/ +| #G #L #V #T1 #T2 #_ #b #J #W #U1 #H destruct +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #b #J #W #U1 #H destruct +| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W #U1 #H destruct ] qed-. -lemma cpr_inv_bind1: ∀a,I,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡ U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & - L. ⓑ{I}V1 ⊢ T1 ➡ T2 & +lemma cpr_inv_bind1: ∀a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡ U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡ T2 & U2 = ⓑ{a,I}V2.T2 ) ∨ - ∃∃T. L.ⓓV1 ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr. + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & + a = true & I = Abbr. /2 width=3 by cpr_inv_bind1_aux/ qed-. (* Basic_1: includes: pr0_gen_abbr pr2_gen_abbr *) -lemma cpr_inv_abbr1: ∀a,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡ U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & - L. ⓓV1 ⊢ T1 ➡ T2 & +lemma cpr_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡ U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L. ⓓV1⦄ ⊢ T1 ➡ T2 & U2 = ⓓ{a}V2.T2 ) ∨ - ∃∃T. L.ⓓV1 ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true. -#a #L #V1 #T1 #U2 #H + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true. +#a #G #L #V1 #T1 #U2 #H elim (cpr_inv_bind1 … H) -H * /3 width=3/ /3 width=5/ qed-. (* Basic_1: includes: pr0_gen_abst pr2_gen_abst *) -lemma cpr_inv_abst1: ∀a,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡ U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & L.ⓛV1 ⊢ T1 ➡ T2 & +lemma cpr_inv_abst1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡ U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡ T2 & U2 = ⓛ{a}V2.T2. -#a #L #V1 #T1 #U2 #H +#a #G #L #V1 #T1 #U2 #H elim (cpr_inv_bind1 … H) -H * [ /3 width=5/ | #T #_ #_ #_ #H destruct ] qed-. -fact cpr_inv_flat1_aux: ∀L,U,U2. ⦃G, L⦄ ⊢ U ➡ U2 → +fact cpr_inv_flat1_aux: ∀G,L,U,U2. ⦃G, L⦄ ⊢ U ➡ U2 → ∀I,V1,U1. U = ⓕ{I}V1.U1 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ U1 ➡ T2 & U2 = ⓕ{I} V2. T2 | (⦃G, L⦄ ⊢ U1 ➡ U2 ∧ I = Cast) | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ W1 ➡ W2 & - L.ⓛW1 ⊢ T1 ➡ T2 & U1 = ⓛ{a}W1.T1 & + ⦃G, L.ⓛW1⦄ ⊢ T1 ➡ T2 & U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2 & I = Appl | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V & ⇧[0,1] V ≡ V2 & - ⦃G, L⦄ ⊢ W1 ➡ W2 & L.ⓓW1 ⊢ T1 ➡ T2 & + ⦃G, L⦄ ⊢ W1 ➡ W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡ T2 & U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2.ⓐV2.T2 & I = Appl. -#L #U #U2 * -L -U -U2 -[ #I #L #J #W1 #U1 #H destruct -| #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct -| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct -| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=5/ -| #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct -| #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=1/ -| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11/ -| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13/ +#G #L #U #U2 * -L -U -U2 +[ #I #G #L #J #W1 #U1 #H destruct +| #G #L #K #V #V2 #W2 #i #_ #_ #_ #J #W #U1 #H destruct +| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct +| #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=5/ +| #G #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct +| #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=1/ +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11/ +| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13/ ] qed-. -lemma cpr_inv_flat1: ∀I,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡ U2 → +lemma cpr_inv_flat1: ∀I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡ U2 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ U1 ➡ T2 & U2 = ⓕ{I}V2.T2 | (⦃G, L⦄ ⊢ U1 ➡ U2 ∧ I = Cast) | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ W1 ➡ W2 & - L.ⓛW1 ⊢ T1 ➡ T2 & U1 = ⓛ{a}W1.T1 & + ⦃G, L.ⓛW1⦄ ⊢ T1 ➡ T2 & U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2 & I = Appl | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V & ⇧[0,1] V ≡ V2 & - ⦃G, L⦄ ⊢ W1 ➡ W2 & L.ⓓW1 ⊢ T1 ➡ T2 & + ⦃G, L⦄ ⊢ W1 ➡ W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡ T2 & U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2.ⓐV2.T2 & I = Appl. /2 width=3 by cpr_inv_flat1_aux/ qed-. (* Basic_1: includes: pr0_gen_appl pr2_gen_appl *) -lemma cpr_inv_appl1: ∀L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ➡ U2 → +lemma cpr_inv_appl1: ∀G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ➡ U2 → ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ U1 ➡ T2 & U2 = ⓐV2.T2 | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ W1 ➡ W2 & - L.ⓛW1 ⊢ T1 ➡ T2 & + ⦃G, L.ⓛW1⦄ ⊢ T1 ➡ T2 & U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2 | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V & ⇧[0,1] V ≡ V2 & - ⦃G, L⦄ ⊢ W1 ➡ W2 & L.ⓓW1 ⊢ T1 ➡ T2 & + ⦃G, L⦄ ⊢ W1 ➡ W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡ T2 & U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2.ⓐV2.T2. -#L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H * +#G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H * [ /3 width=5/ | #_ #H destruct | /3 width=11/ @@ -256,10 +252,10 @@ lemma cpr_inv_appl1: ∀L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ➡ U2 → qed-. (* Note: the main property of simple terms *) -lemma cpr_inv_appl1_simple: ∀L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ → +lemma cpr_inv_appl1_simple: ∀G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ → ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ T1 ➡ T2 & U = ⓐV2. T2. -#L #V1 #T1 #U #H #HT1 +#G #L #V1 #T1 #U #H #HT1 elim (cpr_inv_appl1 … H) -H * [ /2 width=5/ | #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct @@ -270,12 +266,11 @@ elim (cpr_inv_appl1 … H) -H * qed-. (* Basic_1: includes: pr0_gen_cast pr2_gen_cast *) -lemma cpr_inv_cast1: ∀L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡ U2 → ( +lemma cpr_inv_cast1: ∀G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡ U2 → ( ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 & ⦃G, L⦄ ⊢ U1 ➡ T2 & U2 = ⓝ V2. T2 - ) ∨ - ⦃G, L⦄ ⊢ U1 ➡ U2. -#L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H * + ) ∨ ⦃G, L⦄ ⊢ U1 ➡ U2. +#G #L #V1 #U1 #U2 #H elim (cpr_inv_flat1 … H) -H * [ /3 width=5/ | /2 width=1/ | #a #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #H destruct @@ -285,19 +280,19 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma cpr_fwd_bind1_minus: ∀I,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡ T → ∀b. +lemma cpr_fwd_bind1_minus: ∀I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡ T → ∀b. ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 & T = -ⓑ{I}V2.T2. -#I #L #V1 #T1 #T #H #b +#I #G #L #V1 #T1 #T #H #b elim (cpr_inv_bind1 … H) -H * [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/ | #T2 #_ #_ #H destruct ] qed-. -lemma cpr_fwd_shift1: ∀L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡ T → +lemma cpr_fwd_shift1: ∀G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡ T → ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. -#L1 @(lenv_ind_dx … L1) -L1 normalize +#G #L1 @(lenv_ind_dx … L1) -L1 normalize [ #L #T1 #T #HT1 @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) | #I #L1 #V1 #IH #L #T1 #X diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma index a54e9c420..5cee2e207 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma @@ -19,30 +19,30 @@ include "basic_2/reduction/cpr.ma". (* Advanced forward lemmas on context-sensitive irreducible terms ***********) -lemma cpr_fwd_cir: ∀L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ 𝐈⦃T1⦄ → T2 = T1. -#L #T1 #T2 #H elim H -L -T1 -T2 +lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ 𝐈⦃T1⦄ → T2 = T1. +#G #L #T1 #T2 #H elim H -G -L -T1 -T2 [ // -| #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H +| #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H elim (cir_inv_delta … HLK) // -| #a * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H +| #a * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H [ elim (cir_inv_bind … H) -H #HV1 #HT1 * #H destruct lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct lapply (IHT1 … HT1) -IHT1 #H destruct // | elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=2/ ] -| * #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H +| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H [ elim (cir_inv_appl … H) -H #HV1 #HT1 #_ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // | elim (cir_inv_ri2 … H) /2 width=1/ ] -| #L #V1 #T1 #T #T2 #_ #_ #_ #H +| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H elim (cir_inv_ri2 … H) /2 width=1/ -| #L #V1 #T1 #T2 #_ #_ #H +| #G #L #V1 #T1 #T2 #_ #_ #H elim (cir_inv_ri2 … H) /2 width=1/ -| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H elim (cir_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) -| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H +| #a #G #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H elim (cir_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma index 41c77dc3f..6d626e91d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma @@ -20,11 +20,11 @@ include "basic_2/reduction/cpr.ma". (* Relocation properties ****************************************************) (* Basic_1: includes: pr0_lift pr2_lift *) -lemma cpr_lift: l_liftable cpr. -#K #T1 #T2 #H elim H -K -T1 -T2 -[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2 +lemma cpr_lift: ∀G. l_liftable (cpr G). +#G #K #T1 #T2 #H elim H -G -K -T1 -T2 +[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2 >(lift_mono … H1 … H2) -H1 -H2 // -| #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 +| #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hid #H destruct [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=6/ ] -| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 +| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/ -| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 +| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ -| #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2 +| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2 elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/ -| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 +| #G #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ -| #a #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 +| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5/ -| #a #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 +| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct @@ -58,14 +58,14 @@ lemma cpr_lift: l_liftable cpr. qed. (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *) -lemma cpr_inv_lift1: l_deliftable_sn cpr. -#L #U1 #U2 #H elim H -L -U1 -U2 -[ * #L #i #K #d #e #_ #T1 #H +lemma cpr_inv_lift1: ∀G. l_deliftable_sn (cpr G). +#G #L #U1 #U2 #H elim H -G -L -U1 -U2 +[ * #G #L #i #K #d #e #_ #T1 #H [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ ] -| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H +| #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 @@ -75,29 +75,29 @@ lemma cpr_inv_lift1: l_deliftable_sn cpr. elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie #V1 #HV1 >plus_minus // IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // | elim (cix_inv_ri2 … H) /2 width=1/ ] -| #L #V1 #T1 #T #T2 #_ #_ #_ #H +| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H elim (cix_inv_ri2 … H) /2 width=1/ -| #L #V1 #T1 #T2 #_ #_ #H +| #G #L #V1 #T1 #T2 #_ #_ #H elim (cix_inv_ri2 … H) /2 width=1/ -| #L #V1 #V2 #T #_ #_ #H +| #G #L #V1 #V2 #T #_ #_ #H elim (cix_inv_ri2 … H) /2 width=1/ -| #a #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H elim (cix_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) -| #a #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H +| #a #G #L #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H elim (cix_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) ] qed-. - diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma index 40f6e1e97..217306abf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma @@ -20,14 +20,14 @@ include "basic_2/reduction/cpx.ma". (* Relocation properties ****************************************************) -lemma cpx_lift: ∀h,g. l_liftable (cpx h g). -#h #g #K #T1 #T2 #H elim H -K -T1 -T2 -[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2 +lemma cpx_lift: ∀h,g,G. l_liftable (cpx h g G). +#h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2 +[ #I #G #K #L #d #e #_ #U1 #H1 #U2 #H2 >(lift_mono … H1 … H2) -H1 -H2 // -| #K #k #l #Hkl #L #d #e #_ #U1 #H1 #U2 #H2 +| #G #K #k #l #Hkl #L #d #e #_ #U1 #H1 #U2 #H2 >(lift_inv_sort1 … H1) -U1 >(lift_inv_sort1 … H2) -U2 /2 width=2/ -| #I #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 +| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2 elim (lift_inv_lref1 … H) * #Hid #H destruct [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // plus_plus_comm_23 #HVU2 lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=7/ ] -| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 +| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/ -| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 +| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2 elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/ -| #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2 +| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2 elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/ -| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 +| #G #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2 elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ -| #K #V1 #V2 #T #_ #IHV12 #L #d #e #HLK #U1 #H #U2 #HVU2 +| #G #K #V1 #V2 #T #_ #IHV12 #L #d #e #HLK #U1 #H #U2 #HVU2 elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/ -| #a #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 +| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #X #T3 #HX #HT23 #HX2 destruct elim (lift_inv_flat1 … HX) -HX #W3 #V3 #HW23 #HV23 #HX destruct /4 width=5/ -| #a #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 +| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2 elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct elim (lift_inv_bind1 … HX2) -HX2 #W3 #X #HW23 #HX #HX2 destruct @@ -62,16 +62,16 @@ lemma cpx_lift: ∀h,g. l_liftable (cpx h g). ] qed. -lemma cpx_inv_lift1: ∀h,g. l_deliftable_sn (cpx h g). -#h #g #L #U1 #U2 #H elim H -L -U1 -U2 -[ * #L #i #K #d #e #_ #T1 #H +lemma cpx_inv_lift1: ∀h,g,G. l_deliftable_sn (cpx h g G). +#h #g #G #L #U1 #U2 #H elim H -G -L -U1 -U2 +[ * #G #L #i #K #d #e #_ #T1 #H [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/ ] -| #L #k #l #Hkl #K #d #e #_ #T1 #H +| #G #L #k #l #Hkl #K #d #e #_ #T1 #H lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3/ -| #I #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H +| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 @@ -81,32 +81,32 @@ lemma cpx_inv_lift1: ∀h,g. l_deliftable_sn (cpx h g). elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie #V1 #HV1 >plus_minus // append_length >commutative_plus normalize in ⊢ (??% → ?); #H @@ -49,8 +49,8 @@ fact crr_inv_labst_last_aux: ∀L1,T,W. L1 ⊢ 𝐑⦃T⦄ → ] qed. -lemma crr_inv_labst_last: ∀L,T,W. ⋆.ⓛW @@ ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑⦃T⦄. +lemma crr_inv_labst_last: ∀G,L,T,W. ⦃G, ⋆.ⓛW @@ L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑⦃T⦄. /2 width=4/ qed-. -lemma crr_inv_trr: ∀T,W. ⋆.ⓛW ⊢ 𝐑⦃T⦄ → ⋆ ⊢ 𝐑⦃T⦄. +lemma crr_inv_trr: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐑⦃T⦄ → ⦃G, ⋆⦄ ⊢ 𝐑⦃T⦄. /2 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma index 5d923559d..d64a17d4c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma @@ -19,9 +19,9 @@ include "basic_2/reduction/crr.ma". (* Properties on relocation *************************************************) -lemma crr_lift: ∀K,T. K ⊢ 𝐑⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → +lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑⦃U⦄. -#K #T #H elim H -K -T +#G #K #T #H elim H -K -T [ #K #K0 #V #i #HK0 #L #d #e #HLK #X #H elim (lift_inv_lref1 … H) -H * #Hid #H destruct [ elim (ldrop_trans_lt … HLK … HK0) -K // /2 width=4/ @@ -46,9 +46,9 @@ lemma crr_lift: ∀K,T. K ⊢ 𝐑⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → ] qed. -lemma crr_inv_lift: ∀L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → K ⊢ 𝐑⦃T⦄. -#L #U #H elim H -L -U +lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑⦃T⦄. +#G #L #U #H elim H -L -U [ #L #L0 #W #i #HK0 #K #d #e #HLK #X #H elim (lift_inv_lref2 … H) -H * #Hid #H destruct [ elim (ldrop_conf_lt … HLK … HK0) -L // /2 width=4/ @@ -71,4 +71,4 @@ lemma crr_inv_lift: ∀L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,d,e. ⇩[d, e] L elim (lift_inv_flat2 … H) -H #V #X0 #_ #H0 #H destruct elim (lift_inv_bind2 … H0) -H0 #V0 #T #_ #_ #H0 destruct /2 width=1/ ] -qed. +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma index 922dcd4fe..6a4cbbb4e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma @@ -12,40 +12,41 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/reducible_4.ma". +include "basic_2/notation/relations/reducible_5.ma". include "basic_2/static/sd.ma". include "basic_2/reduction/crr.ma". (* CONTEXT-SENSITIVE EXTENDED REDUCIBLE TERMS *******************************) +(* activate genv *) (* extended reducible terms *) -inductive crx (h) (g): lenv → predicate term ≝ -| crx_sort : ∀L,k,l. deg h g k (l+1) → crx h g L (⋆k) -| crx_delta : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g L (#i) -| crx_appl_sn: ∀L,V,T. crx h g L V → crx h g L (ⓐV.T) -| crx_appl_dx: ∀L,V,T. crx h g L T → crx h g L (ⓐV.T) -| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g L (②{I}V.T) -| crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h g L V → crx h g L (ⓑ{a,I}V.T) -| crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h g (L.ⓑ{I}V) T → crx h g L (ⓑ{a,I}V.T) -| crx_beta : ∀a,L,V,W,T. crx h g L (ⓐV. ⓛ{a}W.T) -| crx_theta : ∀a,L,V,W,T. crx h g L (ⓐV. ⓓ{a}W.T) +inductive crx (h) (g) (G:genv): relation2 lenv term ≝ +| crx_sort : ∀L,k,l. deg h g k (l+1) → crx h g G L (⋆k) +| crx_delta : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g G L (#i) +| crx_appl_sn: ∀L,V,T. crx h g G L V → crx h g G L (ⓐV.T) +| crx_appl_dx: ∀L,V,T. crx h g G L T → crx h g G L (ⓐV.T) +| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g G L (②{I}V.T) +| crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h g G L V → crx h g G L (ⓑ{a,I}V.T) +| crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h g G (L.ⓑ{I}V) T → crx h g G L (ⓑ{a,I}V.T) +| crx_beta : ∀a,L,V,W,T. crx h g G L (ⓐV. ⓛ{a}W.T) +| crx_theta : ∀a,L,V,W,T. crx h g G L (ⓐV. ⓓ{a}W.T) . interpretation "context-sensitive extended reducibility (term)" - 'Reducible h g L T = (crx h g L T). + 'Reducible h g G L T = (crx h g G L T). (* Basic properties *********************************************************) -lemma crr_crx: ∀h,g,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄. -#h #g #L #T #H elim H -L -T // /2 width=1/ /2 width=4/ +lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄. +#h #g #G #L #T #H elim H -L -T // /2 width=1/ /2 width=4/ qed. (* Basic inversion lemmas ***************************************************) -fact crx_inv_sort_aux: ∀h,g,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⋆k → +fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⋆k → ∃l. deg h g k (l+1). -#h #g #L #T #k0 * -L -T +#h #g #G #L #T #k0 * -L -T [ #L #k #l #Hkl #H destruct /2 width=2/ | #I #L #K #V #i #HLK #H destruct | #L #V #T #_ #H destruct @@ -58,12 +59,12 @@ fact crx_inv_sort_aux: ∀h,g,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ] qed-. -lemma crx_inv_sort: ∀h,g,L,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃⋆k⦄ → ∃l. deg h g k (l+1). -/2 width=4 by crx_inv_sort_aux/ qed-. +lemma crx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃⋆k⦄ → ∃l. deg h g k (l+1). +/2 width=5 by crx_inv_sort_aux/ qed-. -fact crx_inv_lref_aux: ∀h,g,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i → +fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V. -#h #g #L #T #j * -L -T +#h #g #G #L #T #j * -L -T [ #L #k #l #_ #H destruct | #I #L #K #V #i #HLK #H destruct /2 width=4/ | #L #V #T #_ #H destruct @@ -76,11 +77,11 @@ fact crx_inv_lref_aux: ∀h,g,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i ] qed-. -lemma crx_inv_lref: ∀h,g,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V. -/2 width=5 by crx_inv_lref_aux/ qed-. +lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V. +/2 width=6 by crx_inv_lref_aux/ qed-. -fact crx_inv_gref_aux: ∀h,g,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = §p → ⊥. -#h #g #L #T #q * -L -T +fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = §p → ⊥. +#h #g #G #L #T #q * -L -T [ #L #k #l #_ #H destruct | #I #L #K #V #i #HLK #H destruct | #L #V #T #_ #H destruct @@ -93,12 +94,12 @@ fact crx_inv_gref_aux: ∀h,g,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = § ] qed-. -lemma crx_inv_gref: ∀h,g,L,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃§p⦄ → ⊥. -/2 width=7 by crx_inv_gref_aux/ qed-. +lemma crx_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃§p⦄ → ⊥. +/2 width=8 by crx_inv_gref_aux/ qed-. -lemma trx_inv_atom: ∀h,g,I. ⦃h, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ → +lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ → ∃∃k,l. deg h g k (l+1) & I = Sort k. -#h #g * #i #H +#h #g * #i #G #H [ elim (crx_inv_sort … H) -H /2 width=4/ | elim (crx_inv_lref … H) -H #I #L #V #H elim (ldrop_inv_atom1 … H) -H #H destruct @@ -106,9 +107,9 @@ lemma trx_inv_atom: ∀h,g,I. ⦃h, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ → ] qed-. -fact crx_inv_ib2_aux: ∀h,g,a,I,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → - T = ⓑ{a,I}W.U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃h, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃U⦄. -#h #g #b #J #L #W0 #U #T #HI * -L -T +fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → + T = ⓑ{a,I}W.U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃U⦄. +#h #g #b #J #G #L #W0 #U #T #HI * -L -T [ #L #k #l #_ #H destruct | #I #L #K #V #i #_ #H destruct | #L #V #T #_ #H destruct @@ -123,13 +124,13 @@ fact crx_inv_ib2_aux: ∀h,g,a,I,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g] ] qed-. -lemma crx_inv_ib2: ∀h,g,a,I,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓑ{a,I}W.T⦄ → - ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃h, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃T⦄. +lemma crx_inv_ib2: ∀h,g,a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓑ{a,I}W.T⦄ → + ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃T⦄. /2 width=5 by crx_inv_ib2_aux/ qed-. -fact crx_inv_appl_aux: ∀h,g,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⓐW.U → +fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⓐW.U → ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ | (𝐒⦃U⦄ → ⊥). -#h #g #L #W0 #U #T * -L -T +#h #g #G #L #W0 #U #T * -L -T [ #L #k #l #_ #H destruct | #I #L #K #V #i #_ #H destruct | #L #V #T #HV #H destruct /2 width=1/ @@ -145,6 +146,6 @@ fact crx_inv_appl_aux: ∀h,g,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ] qed-. -lemma crx_inv_appl: ∀h,g,L,V,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓐV.T⦄ → +lemma crx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓐV.T⦄ → ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃V⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ | (𝐒⦃T⦄ → ⊥). /2 width=3 by crx_inv_appl_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma index bd91ad1d5..8f5286c54 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma @@ -19,13 +19,13 @@ include "basic_2/reduction/crx.ma". (* Advanved properties ******************************************************) -lemma crx_append_sn: ∀h,g,L,K,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃h, K @@ L⦄ ⊢ 𝐑[h, g]⦃T⦄. -#h #g #L #K0 #T #H elim H -L -T /2 width=1/ /2 width=2/ +lemma crx_append_sn: ∀h,g,G,L,K,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, K @@ L⦄ ⊢ 𝐑[h, g]⦃T⦄. +#h #g #G #L #K0 #T #H elim H -L -T /2 width=1/ /2 width=2/ #I #L #K #V #i #HLK lapply (ldrop_fwd_length_lt2 … HLK) #Hi lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=4/ qed. -lemma trx_crx: ∀h,g,L,T. ⦃h, ⋆⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄. -#h #g #L #T #H lapply (crx_append_sn … H) // +lemma trx_crx: ∀h,g,G,L,T. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄. +#h #g #G #L #T #H lapply (crx_append_sn … H) // qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma index 5a5a286ff..c4902bb35 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma @@ -19,9 +19,9 @@ include "basic_2/reduction/crx.ma". (* Properties on relocation *************************************************) -lemma crx_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → +lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,d,e. ⇩[d, e] L ≡ K → ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄. -#h #g #K #T #H elim H -K -T +#h #g #G #K #T #H elim H -K -T [ #K #k #l #Hkl #L #d #e #_ #X #H >(lift_inv_sort1 … H) -X /2 width=2/ | #I #K #K0 #V #i #HK0 #L #d #e #HLK #X #H @@ -48,9 +48,9 @@ lemma crx_lift: ∀h,g,K,T. ⦃h, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,d,e. ⇩[d ] qed. -lemma crx_inv_lift: ∀h,g,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → ⦃h, K⦄ ⊢ 𝐑[h, g]⦃T⦄. -#h #g #L #U #H elim H -L -U +lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,d,e. ⇩[d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄. +#h #g #G #L #U #H elim H -L -U [ #L #k #l #Hkl #K #d #e #_ #X #H >(lift_inv_sort2 … H) -X /2 width=2/ | #I #L #L0 #W #i #HK0 #K #d #e #HLK #X #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma index 9fa1327fa..970673d2e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma @@ -12,62 +12,62 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predsn_2.ma". -include "basic_2/grammar/lpx_sn.ma". +include "basic_2/notation/relations/predsn_3.ma". include "basic_2/reduction/cpr.ma". +include "basic_2/grammar/lpx_sn.ma". (**) (* disambiguation error *) (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) -definition lpr: relation lenv ≝ lpx_sn cpr. +definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (cpr G). interpretation "parallel reduction (local environment, sn variant)" - 'PRedSn L1 L2 = (lpr L1 L2). + 'PRedSn G L1 L2 = (lpr G L1 L2). (* Basic inversion lemmas ***************************************************) (* Basic_1: includes: wcpr0_gen_sort *) -lemma lpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆. +lemma lpr_inv_atom1: ∀G,L2. ⦃G, ⋆⦄ ⊢ ➡ L2 → L2 = ⋆. /2 width=4 by lpx_sn_inv_atom1_aux/ qed-. (* Basic_1: includes: wcpr0_gen_head *) -lemma lpr_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ➡ L2 → - ∃∃K2,V2. K1 ⊢ ➡ K2 & K1 ⊢ V1 ➡ V2 & L2 = K2. ⓑ{I} V2. +lemma lpr_inv_pair1: ∀I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L2 = K2.ⓑ{I}V2. /2 width=3 by lpx_sn_inv_pair1_aux/ qed-. -lemma lpr_inv_atom2: ∀L1. L1 ⊢ ➡ ⋆ → L1 = ⋆. +lemma lpr_inv_atom2: ∀G,L1. ⦃G, L1⦄ ⊢ ➡ ⋆ → L1 = ⋆. /2 width=4 by lpx_sn_inv_atom2_aux/ qed-. -lemma lpr_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➡ K2. ⓑ{I} V2 → - ∃∃K1,V1. K1 ⊢ ➡ K2 & K1 ⊢ V1 ➡ V2 & L1 = K1. ⓑ{I} V1. +lemma lpr_inv_pair2: ∀I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡ K2 & ⦃G, K1⦄ ⊢ V1 ➡ V2 & L1 = K1. ⓑ{I} V1. /2 width=3 by lpx_sn_inv_pair2_aux/ qed-. (* Basic properties *********************************************************) (* Note: lemma 250 *) -lemma lpr_refl: ∀L. ⦃G, L⦄ ⊢ ➡ L. +lemma lpr_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡ L. /2 width=1 by lpx_sn_refl/ qed. -lemma lpr_pair: ∀I,K1,K2,V1,V2. K1 ⊢ ➡ K2 → K1 ⊢ V1 ➡ V2 → - K1.ⓑ{I}V1 ⊢ ➡ K2.ⓑ{I}V2. +lemma lpr_pair: ∀I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡ K2 → ⦃G, K1⦄ ⊢ V1 ➡ V2 → + ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡ K2.ⓑ{I}V2. /2 width=1/ qed. -lemma lpr_append: ∀K1,K2. K1 ⊢ ➡ K2 → ∀L1,L2. L1 ⊢ ➡ L2 → - L1 @@ K1 ⊢ ➡ L2 @@ K2. +lemma lpr_append: ∀G,K1,K2. ⦃G, K1⦄ ⊢ ➡ K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L1 @@ K1⦄ ⊢ ➡ L2 @@ K2. /3 width=1 by lpx_sn_append, cpr_append/ qed. (* Basic forward lemmas *****************************************************) -lemma lpr_fwd_length: ∀L1,L2. L1 ⊢ ➡ L2 → |L1| = |L2|. +lemma lpr_fwd_length: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → |L1| = |L2|. /2 width=2 by lpx_sn_fwd_length/ qed-. (* Advanced forward lemmas **************************************************) -lemma lpr_fwd_append1: ∀K1,L1,L. K1 @@ L1 ⊢ ➡ L → - ∃∃K2,L2. K1 ⊢ ➡ K2 & L = K2 @@ L2. +lemma lpr_fwd_append1: ∀G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡ L → + ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡ K2 & L = K2 @@ L2. /2 width=2 by lpx_sn_fwd_append1/ qed-. -lemma lpr_fwd_append2: ∀L,K2,L2. ⦃G, L⦄ ⊢ ➡ K2 @@ L2 → - ∃∃K1,L1. K1 ⊢ ➡ K2 & L = K1 @@ L1. +lemma lpr_fwd_append2: ∀G,L,K2,L2. ⦃G, L⦄ ⊢ ➡ K2 @@ L2 → + ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡ K2 & L = K1 @@ L1. /2 width=2 by lpx_sn_fwd_append2/ qed-. (* Basic_1: removed theorems 3: wcpr0_getl wcpr0_getl_back diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma index 120e5e60e..734921de3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma @@ -22,25 +22,26 @@ include "basic_2/reduction/lpr.ma". (* Properies on local environment slicing ***********************************) (* Basic_1: includes: wcpr0_drop *) -lemma lpr_ldrop_conf: dropable_sn lpr. +lemma lpr_ldrop_conf: ∀G. dropable_sn (lpr G). /3 width=5 by lpx_sn_deliftable_dropable, cpr_inv_lift1/ qed-. (* Basic_1: includes: wcpr0_drop_back *) -lemma ldrop_lpr_trans: dedropable_sn lpr. +lemma ldrop_lpr_trans: ∀G. dedropable_sn (lpr G). /3 width=9 by lpx_sn_liftable_dedropable, cpr_lift/ qed-. -lemma lpr_ldrop_trans_O1: dropable_dx lpr. +lemma lpr_ldrop_trans_O1: ∀G. dropable_dx (lpr G). /2 width=3 by lpx_sn_dropable/ qed-. (* Properties on context-sensitive parallel reduction for terms *************) -lemma fsup_cpr_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➡ U2 → - ∃∃L,U1. L1 ⊢ ➡ L & ⦃G, L⦄ ⊢ T1 ➡ U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄. -#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] -[ #L #K #U #T #d #e #HLK #HUT #He #U2 #HU2 +lemma fsup_cpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → + ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊃ ⦃G2, L2, U2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ] +[ #G #L #K #U #T #d #e #HLK #HUT #He #U2 #HU2 elim (lift_total U2 d e) #T2 #HUT2 lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9/ -| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 +| #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2 elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2 elim (lift_total T d e) #U #HTU elim (ldrop_lpr_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index 2cc08f081..b3e872e40 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -12,36 +12,36 @@ (* *) (**************************************************************************) +include "basic_2/reduction/lpr_ldrop.ma". (**) (* disambiguation error *) include "basic_2/grammar/lpx_sn_lpx_sn.ma". include "basic_2/substitution/fsupp.ma". -include "basic_2/reduction/lpr_ldrop.ma". (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) (* Main properties on context-sensitive parallel reduction for terms ********) fact cpr_conf_lpr_atom_atom: - ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ➡ T & L2 ⊢ ⓪{I} ➡ T. + ∀I,G,L1,L2. ∃∃T. ⦃G, L1⦄ ⊢ ⓪{I} ➡ T & ⦃G, L2⦄ ⊢ ⓪{I} ➡ T. /2 width=3/ qed-. fact cpr_conf_lpr_atom_delta: - ∀L0,i. ( - ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → + ∀G,L0,i. ( + ∀L,T. ⦃G, L0, #i⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → - ∀V2. K0 ⊢ V0 ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ #i ➡ T & L2 ⊢ T2 ➡ T. -#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 + ∀V2. ⦃G, K0⦄ ⊢ V0 ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ #i ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. +#G #L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (fsupp_lref … HLK0) -HLK0 #HLK0 +lapply (fsupp_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/ @@ -49,19 +49,19 @@ qed-. (* Basic_1: includes: pr0_delta_delta pr2_delta_delta *) fact cpr_conf_lpr_delta_delta: - ∀L0,i. ( - ∀L,T. ⦃L0, #i⦄ ⊃+ ⦃L, T⦄ → + ∀G,L0,i. ( + ∀L,T. ⦃G, L0, #i⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 → - ∀V1. K0 ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 → + ∀V1. ⦃G, K0⦄ ⊢ V0 ➡ V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 → ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX → - ∀V2. KX ⊢ VX ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ T1 ➡ T & L2 ⊢ T2 ➡ T. -#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 + ∀V2. ⦃G, KX⦄ ⊢ VX ➡ V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. +#G #L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 #KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 lapply (ldrop_mono … H … HLK0) -H #H destruct elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1 @@ -70,7 +70,7 @@ lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2 -lapply (fsupp_lref … HLK0) -HLK0 #HLK0 +lapply (fsupp_lref … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (lift_total V 0 (i+1)) #T #HVT lapply (cpr_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1 @@ -78,51 +78,51 @@ lapply (cpr_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/ qed-. fact cpr_conf_lpr_bind_bind: - ∀a,I,L0,V0,T0. ( - ∀L,T. ⦃L0,ⓑ{a,I}V0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀a,I,G,L0,V0,T0. ( + ∀L,T. ⦃G, L0, ⓑ{a,I}V0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0.ⓑ{I}V0 ⊢ T0 ➡ T1 → - ∀V2. L0 ⊢ V0 ➡ V2 → ∀T2. L0.ⓑ{I}V0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ ⓑ{a,I}V1.T1 ➡ T & L2 ⊢ ⓑ{a,I}V2.T2 ➡ T. -#a #I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 + ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡ T1 → + ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀T2. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ ⓑ{a,I}V1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓑ{a,I}V2.T2 ➡ T. +#a #I #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) // elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/ qed-. fact cpr_conf_lpr_bind_zeta: - ∀L0,V0,T0. ( - ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀G,L0,V0,T0. ( + ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0.ⓓV0 ⊢ T0 ➡ T1 → - ∀T2. L0.ⓓV0 ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ +ⓓV1.T1 ➡ T & L2 ⊢ X2 ➡ T. -#L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 + ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T1 → + ∀T2. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ +ⓓV1.T1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T. +#G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 // /2 width=1/ -L0 -V0 -T0 #T #HT1 #HT2 elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ /3 width=3/ qed-. fact cpr_conf_lpr_zeta_zeta: - ∀L0,V0,T0. ( - ∀L,T. ⦃L0,+ⓓV0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀G,L0,V0,T0. ( + ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀T1. L0.ⓓV0 ⊢ T0 ➡ T1 → ∀X1. ⇧[O, 1] X1 ≡ T1 → - ∀T2. L0.ⓓV0 ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ X1 ➡ T & L2 ⊢ X2 ➡ T. -#L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 + ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T1 → ∀X1. ⇧[O, 1] X1 ≡ T1 → + ∀T2. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ X1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T. +#G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 // /2 width=1/ -L0 -T0 #T #HT1 #HT2 elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1/ #T1 #HT1 #HXT1 @@ -131,64 +131,64 @@ lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3/ qed-. fact cpr_conf_lpr_flat_flat: - ∀I,L0,V0,T0. ( - ∀L,T. ⦃L0,ⓕ{I}V0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀I,G,L0,V0,T0. ( + ∀L,T. ⦃G, L0, ⓕ{I}V0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0 ⊢ T0 ➡ T1 → - ∀V2. L0 ⊢ V0 ➡ V2 → ∀T2. L0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ ⓕ{I}V1.T1 ➡ T & L2 ⊢ ⓕ{I}V2.T2 ➡ T. -#I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 + ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → + ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ ⓕ{I}V1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓕ{I}V2.T2 ➡ T. +#I #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01 #V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) // elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/ qed-. fact cpr_conf_lpr_flat_tau: - ∀L0,V0,T0. ( - ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀G,L0,V0,T0. ( + ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1,T1. L0 ⊢ T0 ➡ T1 → ∀T2. L0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ ⓝV1.T1 ➡ T & L2 ⊢ T2 ➡ T. -#L0 #V0 #T0 #IH #V1 #T1 #HT01 + ∀V1,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ ⓝV1.T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. +#G #L0 #V0 #T0 #IH #V1 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3/ qed-. fact cpr_conf_lpr_tau_tau: - ∀L0,V0,T0. ( - ∀L,T. ⦃L0,ⓝV0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀G,L0,V0,T0. ( + ∀L,T. ⦃G, L0, ⓝV0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀T1. L0 ⊢ T0 ➡ T1 → ∀T2. L0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ T1 ➡ T & L2 ⊢ T2 ➡ T. -#L0 #V0 #T0 #IH #T1 #HT01 + ∀T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀T2. ⦃G, L0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T. +#G #L0 #V0 #T0 #IH #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3/ qed-. fact cpr_conf_lpr_flat_beta: - ∀a,L0,V0,W0,T0. ( - ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀a,G,L0,V0,W0,T0. ( + ∀L,T. ⦃G, L0, ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0 ⊢ ⓛ{a}W0.T0 ➡ T1 → - ∀V2. L0 ⊢ V0 ➡ V2 → ∀W2. L0 ⊢ W0 ➡ W2 → ∀T2. L0.ⓛW0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ ⓐV1.T1 ➡ T & L2 ⊢ ⓓ{a}ⓝW2.V2.T2 ➡ T. -#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H + ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓛ{a}W0.T0 ➡ T1 → + ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}ⓝW2.V2.T2 ➡ T. +#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (cpr_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 @@ -203,18 +203,18 @@ qed-. pr0_cong_upsilon_cong pr0_cong_upsilon_delta *) fact cpr_conf_lpr_flat_theta: - ∀a,L0,V0,W0,T0. ( - ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀a,G,L0,V0,W0,T0. ( + ∀L,T. ⦃G, L0, ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1. L0 ⊢ V0 ➡ V1 → ∀T1. L0 ⊢ ⓓ{a}W0.T0 ➡ T1 → - ∀V2. L0 ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → - ∀W2. L0 ⊢ W0 ➡ W2 → ∀T2. L0.ⓓW0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ ⓐV1.T1 ➡ T & L2 ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. -#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H + ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓓ{a}W0.T0 ➡ T1 → + ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → + ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. +#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #X #H #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 elim (lift_total V 0 1) #U #HVU @@ -232,17 +232,17 @@ elim (cpr_inv_abbr1 … H) -H * qed-. fact cpr_conf_lpr_beta_beta: - ∀a,L0,V0,W0,T0. ( - ∀L,T. ⦃L0,ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀a,G,L0,V0,W0,T0. ( + ∀L,T. ⦃G, L0, ⓐV0.ⓛ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1. L0 ⊢ V0 ➡ V1 → ∀W1. L0 ⊢ W0 ➡ W1 → ∀T1. L0.ⓛW0 ⊢ T0 ➡ T1 → - ∀V2. L0 ⊢ V0 ➡ V2 → ∀W2. L0 ⊢ W0 ➡ W2 → ∀T2. L0.ⓛW0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ ⓓ{a}ⓝW1.V1.T1 ➡ T & L2 ⊢ ⓓ{a}ⓝW2.V2.T2 ➡ T. -#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01 + ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀W1. ⦃G, L0⦄ ⊢ W0 ➡ W1 → ∀T1. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡ T1 → + ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓛW0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{a}ⓝW1.V1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}ⓝW2.V2.T2 ➡ T. +#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01 #V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2 @@ -254,19 +254,19 @@ qed-. (* Basic_1: was: pr0_upsilon_upsilon *) fact cpr_conf_lpr_theta_theta: - ∀a,L0,V0,W0,T0. ( - ∀L,T. ⦃L0,ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃L, T⦄ → + ∀a,G,L0,V0,W0,T0. ( + ∀L,T. ⦃G, L0, ⓐV0.ⓓ{a}W0.T0⦄ ⊃+ ⦃G, L, T⦄ → ∀T1. ⦃G, L⦄ ⊢ T ➡ T1 → ∀T2. ⦃G, L⦄ ⊢ T ➡ T2 → ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 → - ∃∃T0. L1 ⊢ T1 ➡ T0 & L2 ⊢ T2 ➡ T0 + ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0 ) → - ∀V1. L0 ⊢ V0 ➡ V1 → ∀U1. ⇧[O, 1] V1 ≡ U1 → - ∀W1. L0 ⊢ W0 ➡ W1 → ∀T1. L0.ⓓW0 ⊢ T0 ➡ T1 → - ∀V2. L0 ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → - ∀W2. L0 ⊢ W0 ➡ W2 → ∀T2. L0.ⓓW0 ⊢ T0 ➡ T2 → - ∀L1. L0 ⊢ ➡ L1 → ∀L2. L0 ⊢ ➡ L2 → - ∃∃T. L1 ⊢ ⓓ{a}W1.ⓐU1.T1 ➡ T & L2 ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. -#a #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01 + ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀U1. ⇧[O, 1] V1 ≡ U1 → + ∀W1. ⦃G, L0⦄ ⊢ W0 ➡ W1 → ∀T1. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T1 → + ∀V2. ⦃G, L0⦄ ⊢ V0 ➡ V2 → ∀U2. ⇧[O, 1] V2 ≡ U2 → + ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 → + ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{a}W1.ⓐU1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T. +#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #U1 #HVU1 #W1 #HW01 #T1 #HT01 #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ @@ -277,9 +277,9 @@ lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ /4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* timeout 40 *) qed-. -theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. -#L0 #T0 @(fsupp_wf_ind … L0 T0) -L0 -T0 #L #T #IH #L0 * [|*] -[ #I0 #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct +theorem cpr_conf_lpr: ∀G. lpx_sn_confluent (cpr G) (cpr G). +#G #L0 #T0 @(fsupp_wf_ind … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [|*] +[ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1 … H1) -H1 elim (cpr_inv_atom1 … H2) -H2 [ #H2 #H1 destruct @@ -292,7 +292,7 @@ theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct /3 width=17 by cpr_conf_lpr_delta_delta/ ] -| #a #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #a #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_bind1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 | #T1 #HT01 #HXT1 #H11 #H12 @@ -306,7 +306,7 @@ theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. | /3 width=11 by cpr_conf_lpr_bind_zeta/ | /3 width=12 by cpr_conf_lpr_zeta_zeta/ ] -| #I #V0 #T0 #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct +| #I #V0 #T0 #HG #HL #HT #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_flat1 … H1) -H1 * [ #V1 #T1 #HV01 #HT01 #H1 | #HX1 #H1 @@ -334,25 +334,25 @@ theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr. qed-. (* Basic_1: includes: pr0_confluence pr2_confluence *) -theorem cpr_conf: ∀L. confluent … (cpr L). +theorem cpr_conf: ∀G,L. confluent … (cpr G L). /2 width=6 by cpr_conf_lpr/ qed-. (* Properties on context-sensitive parallel reduction for terms *************) -lemma lpr_cpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡ L1 → - ∃∃T. L1 ⊢ T0 ➡ T & L1 ⊢ T1 ➡ T. -#L0 #T0 #T1 #HT01 #L1 #HL01 +lemma lpr_cpr_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L1⦄ ⊢ T1 ➡ T. +#G #L0 #T0 #T1 #HT01 #L1 #HL01 elim (cpr_conf_lpr … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/ qed-. -lemma lpr_cpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡ L1 → - ∃∃T. L1 ⊢ T0 ➡ T & L0 ⊢ T1 ➡ T. -#L0 #T0 #T1 #HT01 #L1 #HL01 +lemma lpr_cpr_conf_sn: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡ T1 → ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T0 ➡ T & ⦃G, L0⦄ ⊢ T1 ➡ T. +#G #L0 #T0 #T1 #HT01 #L1 #HL01 elim (cpr_conf_lpr … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/ qed-. (* Main properties **********************************************************) -theorem lpr_conf: confluent … lpr. +theorem lpr_conf: ∀G. confluent … (lpr G). /3 width=6 by lpx_sn_conf, cpr_conf_lpr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma index 547520714..36a713d1c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma @@ -12,63 +12,64 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/predsn_4.ma". +include "basic_2/notation/relations/predsn_5.ma". include "basic_2/reduction/lpr.ma". include "basic_2/reduction/cpx.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) -definition lpx: ∀h. sd h → relation lenv ≝ λh,g. lpx_sn (cpx h g). +definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝ + λh,g,G. lpx_sn (cpx h g G). interpretation "extended parallel reduction (local environment, sn variant)" - 'PRedSn h g L1 L2 = (lpx h g L1 L2). + 'PRedSn h g G L1 L2 = (lpx h g G L1 L2). (* Basic inversion lemmas ***************************************************) -lemma lpx_inv_atom1: ∀h,g,L2. ⦃h, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆. +lemma lpx_inv_atom1: ∀h,g,G,L2. ⦃G, ⋆⦄ ⊢ ➡[h, g] L2 → L2 = ⋆. /2 width=4 by lpx_sn_inv_atom1_aux/ qed-. -lemma lpx_inv_pair1: ∀h,g,I,K1,V1,L2. ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 → - ∃∃K2,V2. ⦃h, K1⦄ ⊢ ➡[h, g] K2 & ⦃h, K1⦄ ⊢ V1 ➡[h, g] V2 & - L2 = K2. ⓑ{I} V2. +lemma lpx_inv_pair1: ∀h,g,I,G,K1,V1,L2. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & + L2 = K2. ⓑ{I} V2. /2 width=3 by lpx_sn_inv_pair1_aux/ qed-. -lemma lpx_inv_atom2: ∀h,g,L1. ⦃h, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆. +lemma lpx_inv_atom2: ∀h,g,G,L1. ⦃G, L1⦄ ⊢ ➡[h, g] ⋆ → L1 = ⋆. /2 width=4 by lpx_sn_inv_atom2_aux/ qed-. -lemma lpx_inv_pair2: ∀h,g,I,L1,K2,V2. ⦃h, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃h, K1⦄ ⊢ ➡[h, g] K2 & ⦃h, K1⦄ ⊢ V1 ➡[h, g] V2 & +lemma lpx_inv_pair2: ∀h,g,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 & L1 = K1. ⓑ{I} V1. /2 width=3 by lpx_sn_inv_pair2_aux/ qed-. (* Basic properties *********************************************************) -lemma lpx_refl: ∀h,g,L. ⦃G, L⦄ ⊢ ➡[h, g] L. +lemma lpx_refl: ∀h,g,G,L. ⦃G, L⦄ ⊢ ➡[h, g] L. /2 width=1 by lpx_sn_refl/ qed. -lemma lpx_pair: ∀h,g,I,K1,K2,V1,V2. ⦃h, K1⦄ ⊢ ➡[h, g] K2 → ⦃h, K1⦄ ⊢ V1 ➡[h, g] V2 → - ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2. +lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ⦃G, K1⦄ ⊢ V1 ➡[h, g] V2 → + ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡[h, g] K2.ⓑ{I}V2. /2 width=1/ qed. -lemma lpx_append: ∀h,g,K1,K2. ⦃h, K1⦄ ⊢ ➡[h, g] K2 → ∀L1,L2. ⦃h, L1⦄ ⊢ ➡[h, g] L2 → - ⦃h, L1 @@ K1⦄ ⊢ ➡[h, g] L2 @@ K2. +lemma lpx_append: ∀h,g,G,K1,K2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 → ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → + ⦃G, L1 @@ K1⦄ ⊢ ➡[h, g] L2 @@ K2. /3 width=1 by lpx_sn_append, cpx_append/ qed. -lemma lpr_lpx: ∀h,g,L1,L2. L1 ⊢ ➡ L2 → ⦃h, L1⦄ ⊢ ➡[h, g] L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /3 width=1/ +lemma lpr_lpx: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡[h, g] L2. +#h #g #G #L1 #L2 #H elim H -L1 -L2 // /3 width=1/ qed. (* Basic forward lemmas *****************************************************) -lemma lpx_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|. +lemma lpx_fwd_length: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → |L1| = |L2|. /2 width=2 by lpx_sn_fwd_length/ qed-. (* Advanced forward lemmas **************************************************) -lemma lpx_fwd_append1: ∀h,g,K1,L1,L. ⦃h, K1 @@ L1⦄ ⊢ ➡[h, g] L → - ∃∃K2,L2. ⦃h, K1⦄ ⊢ ➡[h, g] K2 & L = K2 @@ L2. +lemma lpx_fwd_append1: ∀h,g,G,K1,L1,L. ⦃G, K1 @@ L1⦄ ⊢ ➡[h, g] L → + ∃∃K2,L2. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K2 @@ L2. /2 width=2 by lpx_sn_fwd_append1/ qed-. -lemma lpx_fwd_append2: ∀h,g,L,K2,L2. ⦃G, L⦄ ⊢ ➡[h, g] K2 @@ L2 → - ∃∃K1,L1. ⦃h, K1⦄ ⊢ ➡[h, g] K2 & L = K1 @@ L1. +lemma lpx_fwd_append2: ∀h,g,G,L,K2,L2. ⦃G, L⦄ ⊢ ➡[h, g] K2 @@ L2 → + ∃∃K1,L1. ⦃G, K1⦄ ⊢ ➡[h, g] K2 & L = K1 @@ L1. /2 width=2 by lpx_sn_fwd_append2/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma index 41d1386dd..e21810ea5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma @@ -21,12 +21,13 @@ include "basic_2/reduction/lpx_ldrop.ma". (* Properties on atomic arity assignment for terms **************************) (* Note: lemma 500 *) -lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2. ⦃h, L1⦄ ⊢ ➡[h, g] L2 → L2 ⊢ T2 ⁝ A. -#h #g #L1 #T1 #A #H elim H -L1 -T1 -A -[ #L1 #k #X #H +lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 → + ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. +#h #g #G #L1 #T1 #A #H elim H -G -L1 -T1 -A +[ #g #L1 #k #X #H elim (cpx_inv_sort1 … H) -H // * // -| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 +| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12 elim (cpx_inv_lref1 … H) -H [ #H destruct elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2 @@ -37,15 +38,15 @@ lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/ ] -| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_abbr1 … H) -H * [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/ | #T2 #HT12 #HT2 #H destruct -IHV1 - @(aaa_inv_lift (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/ + @(aaa_inv_lift … (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/ ] -| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 +| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/ -| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 +| #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_appl1 … H) -H * [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/ | #b #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct @@ -54,11 +55,11 @@ lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct lapply (lsuba_aaa_trans … HU2 (L2.ⓓⓝW2.V2) ?) -HU2 /3 width=3/ | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct - lapply (aaa_lift L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2 + lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2 lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H elim (aaa_inv_abbr … H) -H /3 width=3/ ] -| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 +| #G #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12 elim (cpx_inv_cast1 … H) -H [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/ | -IHV1 /2 width=1/ @@ -67,14 +68,14 @@ lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ ] qed-. -lemma aaa_cpx_conf: ∀h,g,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +lemma aaa_cpx_conf: ∀h,g,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. /2 width=7 by aaa_cpx_lpx_conf/ qed-. -lemma aaa_lpx_conf: ∀h,g,L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡[h, g] L2 → L2 ⊢ T ⁝ A. +lemma aaa_lpx_conf: ∀h,g,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 → ⦃G, L2⦄ ⊢ T ⁝ A. /2 width=7 by aaa_cpx_lpx_conf/ qed-. -lemma aaa_cpr_conf: ∀L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. +lemma aaa_cpr_conf: ∀G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T2 ⁝ A. /3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-. -lemma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A. +lemma aaa_lpr_conf: ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T ⁝ A. /3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma index 57459d1a7..468419f6c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma @@ -20,11 +20,11 @@ include "basic_2/reduction/lpx.ma". (* Properies on local environment slicing ***********************************) -lemma lpx_ldrop_conf: ∀h,g. dropable_sn (lpx h g). +lemma lpx_ldrop_conf: ∀h,g,G. dropable_sn (lpx h g G). /3 width=5 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-. -lemma ldrop_lpx_trans: ∀h,g. dedropable_sn (lpx h g). +lemma ldrop_lpx_trans: ∀h,g,G. dedropable_sn (lpx h g G). /3 width=9 by lpx_sn_liftable_dedropable, cpx_lift/ qed-. -lemma lpx_ldrop_trans_O1: ∀h,g. dropable_dx (lpx h g). +lemma lpx_ldrop_trans_O1: ∀h,g,G. dropable_dx (lpx h g G). /2 width=3 by lpx_sn_dropable/ qed-. 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 fb6d828aa..a68019864 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 @@ -115,37 +115,37 @@ table { class "water" [ { "reduction" * } { [ { "context-sensitive extended normal forms" * } { - [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] + [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpx_ldrop" + "lpx_aaa" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_lift" + "cpx_cix" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_aaa" * ] + [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cix" * ] } ] [ { "context-sensitive extended irreducible forms" * } { - [ "cix ( ⦃?,?⦄ ⊢ 𝐈[?]⦃?⦄ )" "cix_append" + "cix_lift" * ] + [ "cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ )" "cix_append" + "cix_lift" * ] } ] [ { "context-sensitive extended reducible forms" * } { - [ "crx ( ⦃?,?⦄ ⊢ 𝐑[?]⦃?⦄ )" "crx_append" + "crx_lift" * ] + [ "crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ )" "crx_append" + "crx_lift" * ] } ] [ { "context-sensitive normal forms" * } { - [ "cnr ( ? ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] + [ "cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] } ] [ { "context-sensitive reduction" * } { - [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpr" * ] - [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cir" * ] + [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpr" * ] + [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cir" * ] } ] [ { "context-sensitive irreducible forms" * } { - [ "cir ( ? ⊢ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ] + [ "cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ] } ] [ { "context-sensitive reducible forms" * } { - [ "crr ( ? ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ] + [ "crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ] } ] } -- 2.39.2