From: Ferruccio Guidi Date: Fri, 1 Jul 2016 13:59:41 +0000 (+0000) Subject: first definition of cpm: X-Git-Tag: make_still_working~555 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f6b452b9c9be141740d4058dfbcf81a4b75fd00b;p=helm.git first definition of cpm: the contextual rule for cast is incorrect :( --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 91449b0ba..bf8778e2d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -79,6 +79,7 @@ c: conversion d: decomposed rt-reduction e: decomposed rt-conversion g: counted rt-transition (generic) +m: semi-counted rt-transition (mixed) q: restricted reduction r: reduction s: substitution 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..3bc75f682 --- /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 n, break term 46 h ] break term 46 T2 )" + non associative with precedence 45 + for @{ 'PRed $n $h $G $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index b8742090c..fd44b81fd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/steps/rtc_shift.ma". include "ground_2/steps/rtc_plus.ma". include "basic_2/notation/relations/predty_6.ma". include "basic_2/grammar/lenv.ma". @@ -29,7 +28,7 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝ | cpg_delta: ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 → ⬆*[1] V2 ≡ W2 → cpg h c G (L.ⓓV1) (#0) W2 | cpg_ell : ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 → - ⬆*[1] V2 ≡ W2 → cpg h ((↓c)+𝟘𝟙) G (L.ⓛV1) (#0) W2 + ⬆*[1] V2 ≡ W2 → cpg h (c+𝟘𝟙) G (L.ⓛV1) (#0) W2 | cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T → ⬆*[1] T ≡ U → cpg h c G (L.ⓑ{I}V) (#⫯i) U | cpg_bind : ∀cV,cT,p,I,G,L,V1,V2,T1,T2. @@ -39,16 +38,16 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝ cpg h cV G L V1 V2 → cpg h cT G L T1 T2 → cpg h ((↓cV)+cT) G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) | cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg h c G (L.ⓓV) T1 T → - ⬆*[1] T2 ≡ T → cpg h ((↓c)+𝟙𝟘) G L (+ⓓV.T1) T2 -| cpg_eps : ∀c,G,L,V,T1,T2. cpg h c G L T1 T2 → cpg h ((↓c)+𝟙𝟘) G L (ⓝV.T1) T2 -| cpg_ee : ∀c,G,L,V1,V2,T. cpg h c G L V1 V2 → cpg h ((↓c)+𝟘𝟙) G L (ⓝV1.T) V2 + ⬆*[1] T2 ≡ T → cpg h (c+𝟙𝟘) G L (+ⓓV.T1) T2 +| cpg_eps : ∀c,G,L,V,T1,T2. cpg h c G L T1 T2 → cpg h (c+𝟙𝟘) G L (ⓝV.T1) T2 +| cpg_ee : ∀c,G,L,V1,V2,T. cpg h c G L V1 V2 → cpg h (c+𝟘𝟙) G L (ⓝV1.T) V2 | cpg_beta : ∀cV,cW,cT,p,G,L,V1,V2,W1,W2,T1,T2. cpg h cV G L V1 V2 → cpg h cW G L W1 W2 → cpg h cT G (L.ⓛW1) T1 T2 → - cpg h ((↓cV)+(↓cW)+(↓cT)+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) + cpg h ((↓cV)+(↓cW)+cT+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2) | cpg_theta: ∀cV,cW,cT,p,G,L,V1,V,V2,W1,W2,T1,T2. cpg h cV G L V1 V → ⬆*[1] V ≡ V2 → cpg h cW G L W1 W2 → cpg h cT G (L.ⓓW1) T1 T2 → - cpg h ((↓cV)+(↓cW)+(↓cT)+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) + cpg h ((↓cV)+(↓cW)+cT+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2) . interpretation @@ -75,7 +74,7 @@ fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2 → ∀ | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓓV1 & J = LRef 0 & c = cV | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 & - L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙 + L = K.ⓛV1 & J = LRef 0 & c = cV+𝟘𝟙 | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V & J = LRef (⫯i). #c #h #G #L #T1 #T2 * -c -G -L -T1 -T2 @@ -100,7 +99,7 @@ lemma cpg_inv_atom1: ∀c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[c, h] T2 → | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓓV1 & J = LRef 0 & c = cV | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 & - L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙 + L = K.ⓛV1 & J = LRef 0 & c = cV+𝟘𝟙 | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V & J = LRef (⫯i). /2 width=3 by cpg_inv_atom1_aux/ qed-. @@ -120,7 +119,7 @@ lemma cpg_inv_zero1: ∀c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈[c, h] T2 → | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓓV1 & c = cV | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 & - L = K.ⓛV1 & c = (↓cV)+𝟘𝟙. + L = K.ⓛV1 & c = cV+𝟘𝟙. #c #h #G #L #T2 #H elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/ [ #s #H destruct @@ -155,7 +154,7 @@ fact cpg_inv_bind1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 → U2 = ⓑ{p,J}V2.T2 & c = (↓cV)+cT ) ∨ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T & - p = true & J = Abbr & c = (↓cT)+𝟙𝟘. + p = true & J = Abbr & c = cT+𝟙𝟘. #c #h #G #L #U #U2 * -c -G -L -U -U2 [ #I #G #L #q #J #W #U1 #H destruct | #G #L #s #q #J #W #U1 #H destruct @@ -177,7 +176,7 @@ lemma cpg_inv_bind1: ∀c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c U2 = ⓑ{p,I}V2.T2 & c = (↓cV)+cT ) ∨ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T & - p = true & I = Abbr & c = (↓cT)+𝟙𝟘. + p = true & I = Abbr & c = cT+𝟙𝟘. /2 width=3 by cpg_inv_bind1_aux/ qed-. lemma cpg_inv_abbr1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[c, h] U2 → ( @@ -185,7 +184,7 @@ lemma cpg_inv_abbr1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[c, h] U2 = ⓓ{p}V2.T2 & c = (↓cV)+cT ) ∨ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T & - p = true & c = (↓cT)+𝟙𝟘. + p = true & c = cT+𝟙𝟘. #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * /3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/ qed-. @@ -203,12 +202,12 @@ fact cpg_inv_flat1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 → ∀J,V1,U1. U = ⓕ{J}V1.U1 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & U2 = ⓕ{J}V2.T2 & c = (↓cV)+cT - | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & J = Cast & c = (↓cT)+𝟙𝟘 - | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & J = Cast & c = (↓cV)+𝟘𝟙 + | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & J = Cast & c = cT+𝟙𝟘 + | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & J = Cast & c = cV+𝟘𝟙 | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 & - J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘 + J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘 | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 & - J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘. + J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘. #c #h #G #L #U #U2 * -c -G -L -U -U2 [ #I #G #L #J #W #U1 #H destruct | #G #L #s #J #W #U1 #H destruct @@ -228,21 +227,21 @@ qed-. lemma cpg_inv_flat1: ∀c,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & U2 = ⓕ{I}V2.T2 & c = (↓cV)+cT - | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & I = Cast & c = (↓cT)+𝟙𝟘 - | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & I = Cast & c = (↓cV)+𝟘𝟙 + | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & I = Cast & c = cT+𝟙𝟘 + | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & I = Cast & c = cV+𝟘𝟙 | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 & - I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘 + I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘 | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 & - I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘. + I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘. /2 width=3 by cpg_inv_flat1_aux/ qed-. lemma cpg_inv_appl1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ⬈[c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & U2 = ⓐV2.T2 & c = (↓cV)+cT | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 & - U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘 + U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘 | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 & - U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+(↓cT)+𝟙𝟘. + U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = (↓cV)+(↓cW)+cT+𝟙𝟘. #c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H * [ /3 width=8 by or3_intro0, ex4_4_intro/ |2,3: #c #_ #H destruct @@ -254,8 +253,8 @@ qed-. lemma cpg_inv_cast1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[c, h] U2 → ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 & U2 = ⓝV2.T2 & c = (↓cV)+cT - | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & c = (↓cT)+𝟙𝟘 - | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & c = (↓cV)+𝟘𝟙. + | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & c = cT+𝟙𝟘 + | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & c = cV+𝟘𝟙. #c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H * [ /3 width=8 by or3_intro0, ex4_4_intro/ |2,3: /3 width=3 by or3_intro1, or3_intro2, ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma index 7c9c79b70..b22fc0938 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_drops.ma @@ -32,7 +32,7 @@ lemma cpg_delta_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓓV → ⦃G, K qed. lemma cpg_ell_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ⬈[c, h] V2 → - ⬆*[⫯i] V2 ≡ T2 → ⦃G, L⦄ ⊢ #i ⬈[(↓c)+𝟘𝟙, h] T2. + ⬆*[⫯i] V2 ≡ T2 → ⦃G, L⦄ ⊢ #i ⬈[c+𝟘𝟙, h] T2. #c #h #G #K #V #V2 #i elim i -i [ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_ell/ | #i #IH #L0 #T0 #H0 #HV2 #HVT2 @@ -48,7 +48,7 @@ lemma cpg_inv_lref1_drops: ∀c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ⬈[c, h] T2 → | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 & ⬆*[⫯i] V2 ≡ T2 & c = cV | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 & - ⬆*[⫯i] V2 ≡ T2 & c = (↓cV) + 𝟘𝟙. + ⬆*[⫯i] V2 ≡ T2 & c = cV + 𝟘𝟙. #c #h #G #i elim i -i [ #L #T2 #H elim (cpg_inv_zero1 … H) -H * /3 width=1 by or3_intro0, conj/ /4 width=8 by drops_refl, ex4_4_intro, or3_intro2, or3_intro1/ @@ -67,7 +67,7 @@ lemma cpg_inv_atom1_drops: ∀c,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ⬈[c, h] T2 | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 & ⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 & - ⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = (↓cV) + 𝟘𝟙. + ⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV + 𝟘𝟙. #c #h * #n #G #L #T2 #H [ elim (cpg_inv_sort1 … H) -H * /3 width=3 by or4_intro0, or4_intro1, ex3_intro, conj/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma new file mode 100644 index 000000000..3201a5b8f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -0,0 +1,313 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/pred_6.ma". +include "basic_2/notation/relations/pred_5.ma". +include "basic_2/rt_transition/cpg.ma". + +(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) + +(* Basic_2A1: includes: cpr *) +definition cpm (n) (h): relation4 genv lenv term term ≝ + λG,L,T1,T2. ∃∃c. 𝐑𝐓⦃n, c⦄ & ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2. + +interpretation + "semi-counted context-sensitive parallel rt-transition (term)" + 'PRed n h G L T1 T2 = (cpm n h G L T1 T2). + +interpretation + "context-sensitive parallel r-transition (term)" + 'PRed h G L T1 T2 = (cpm O h G L T1 T2). + +(* Basic properties *********************************************************) + +lemma cpm_ess: ∀h,G,L,s. ⦃G, L⦄ ⊢ ⋆s ➡[1, h] ⋆(next h s). +/2 width=3 by cpg_ess, ex2_intro/ qed. + +lemma cpm_delta: ∀n,h,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → + ⬆*[1] V2 ≡ W2 → ⦃G, K.ⓓV1⦄ ⊢ #0 ➡[n, h] W2. +#n #h #G #K #V1 #V2 #W2 * +/3 width=5 by cpg_delta, ex2_intro/ +qed. + +lemma cpm_ell: ∀n,h,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → + ⬆*[1] V2 ≡ W2 → ⦃G, K.ⓛV1⦄ ⊢ #0 ➡[⫯n, h] W2. +#n #h #G #K #V1 #V2 #W2 * +/3 width=5 by cpg_ell, ex2_intro, isrt_succ/ +qed. + +lemma cpm_lref: ∀n,h,I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T → + ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ➡[n, h] U. +#n #h #I #G #K #V #T #U #i * +/3 width=5 by cpg_lref, ex2_intro/ +qed. + +lemma cpm_bind: ∀n,h,p,I,G,L,V1,V2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 → + ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] ⓑ{p,I}V2.T2. +#n #h #p #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 * +/5 width=5 by cpg_bind, isrt_plus_O1, isr_shift, ex2_intro/ +qed. + +lemma cpm_flat: ∀n,h,I,G,L,V1,V2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → + ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[n, h] ⓕ{I}V2.T2. +#n #h #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 * +/5 width=5 by isrt_plus_O1, isr_shift, cpg_flat, ex2_intro/ +qed. + +lemma cpm_zeta: ∀n,h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[n, h] T → + ⬆*[1] T2 ≡ T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡[n, h] T2. +#n #h #G #L #V #T1 #T #T2 * +/3 width=5 by cpg_zeta, isrt_plus_O2, ex2_intro/ +qed. + +lemma cpm_eps: ∀n,h,G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 → ⦃G, L⦄ ⊢ ⓝV.T1 ➡[n, h] T2. +#n #h #G #L #V #T1 #T2 * +/3 width=3 by cpg_eps, isrt_plus_O2, ex2_intro/ +qed. + +lemma cpm_ee: ∀n,h,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 → ⦃G, L⦄ ⊢ ⓝV1.T ➡[⫯n, h] V2. +#n #h #G #L #V1 #V2 #T * +/3 width=3 by cpg_ee, isrt_succ, ex2_intro/ +qed. + +lemma cpm_beta: ∀n,h,p,G,L,V1,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ➡[n, h] ⓓ{p}ⓝW2.V2.T2. +#n #h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV12 * #riW #rhW #HW12 * +/6 width=7 by cpg_beta, isrt_plus_O2, isrt_plus, isr_shift, ex2_intro/ +qed. + +lemma cpm_theta: ∀n,h,p,G,L,V1,V,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡[h] V → ⬆*[1] V ≡ V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → + ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡[n, h] ⓓ{p}W2.ⓐV2.T2. +#n #h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #riV #rhV #HV1 #HV2 * #riW #rhW #HW12 * +/6 width=9 by cpg_theta, isrt_plus_O2, isrt_plus, isr_shift, ex2_intro/ +qed. + +(* Basic properties on r-transition *****************************************) + +(* Basic_2A1: includes: cpr_atom *) +lemma cpr_refl: ∀h,G,L. reflexive … (cpm 0 h G L). +/2 width=3 by ex2_intro/ qed. + +lemma cpr_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → + ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡[h] ②{I}V2.T. +#h #I #G #L #V1 #V2 * +/3 width=3 by cpg_pair_sn, isr_shift, ex2_intro/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → + ∨∨ T2 = ⓪{J} ∧ n = 0 + | ∃∃s. T2 = ⋆(next h s) & J = Sort s & n = 1 + | ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓓV1 & J = LRef 0 + | ∃∃m,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[m, h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓛV1 & J = LRef 0 & n = ⫯m + | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≡ T2 & + L = K.ⓑ{I}V & J = LRef (⫯i). +#n #h #J #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1 … H) -H * +[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or5_intro0, conj/ +| #s #H1 #H2 #H3 destruct /4 width=3 by isrt_inv_01, or5_intro1, ex3_intro/ +| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct + /4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/ +| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct + /4 width=9 by or5_intro3, ex5_4_intro, ex2_intro/ +| #I #K #V1 #V2 #i #HV2 #HVT2 #H1 #H2 destruct + /4 width=9 by or5_intro4, ex4_5_intro, ex2_intro/ +] +qed-. + +lemma cpm_inv_sort1: ∀n,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[n,h] T2 → + (T2 = ⋆s ∧ n = 0) ∨ + (T2 = ⋆(next h s) ∧ n = 1). +#n #h #G #L #T2 #s * #c #Hc #H elim (cpg_inv_sort1 … H) -H * +#H1 #H2 destruct +/4 width=1 by isrt_inv_01, isrt_inv_00, or_introl, or_intror, conj/ +qed-. + +lemma cpm_inv_zero1: ∀n,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[n, h] T2 → + ∨∨ (T2 = #0 ∧ n = 0) + | ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓓV1 + | ∃∃m,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[m, h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓛV1 & n = ⫯m. +#n #h #G #L #T2 * #c #Hc #H elim (cpg_inv_zero1 … H) -H * +[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or3_intro0, conj/ +| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct + /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/ +| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct + /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/ +] +qed-. + +lemma cpm_inv_lref1: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ➡[n, h] T2 → + (T2 = #(⫯i) ∧ n = 0) ∨ + ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V. +#n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1 … H) -H * +[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or_introl, conj/ +| #I #K #V1 #V2 #HV2 #HVT2 #H1 destruct + /4 width=7 by ex3_4_intro, ex2_intro, or_intror/ +] +qed-. + +lemma cpm_inv_gref1: ∀n,h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ➡[n, h] T2 → T2 = §l ∧ n = 0. +#n #h #G #L #T2 #l * #c #Hc #H elim (cpg_inv_gref1 … H) -H +#H1 #H2 destruct /3 width=1 by isrt_inv_00, conj/ +qed-. + +lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 & + U2 = ⓑ{p,I}V2.T2 + ) ∨ + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & + p = true & I = Abbr. +#n #h #p #I #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_bind1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + /4 width=5 by ex3_2_intro, ex2_intro, or_introl/ +| #cT #T2 #HT12 #HUT2 #H1 #H2 #H3 destruct + /5 width=3 by isrt_inv_plus_O_dx, ex4_intro, ex2_intro, or_intror/ +] +qed-. + +lemma cpm_inv_abbr1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[n, h] U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T2 & + U2 = ⓓ{p}V2.T2 + ) ∨ + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & p = true. +#n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abbr1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + /4 width=5 by ex3_2_intro, ex2_intro, or_introl/ +| #cT #T2 #HT12 #HUT2 #H1 #H2 destruct + /5 width=3 by isrt_inv_plus_O_dx, ex3_intro, ex2_intro, or_intror/ +] +qed-. + +lemma cpm_inv_abst1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡[n, h] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡[n, h] T2 & + U2 = ⓛ{p}V2.T2. +#n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abst1 … H) -H +#cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct +elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct +elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct +/3 width=5 by ex3_2_intro, ex2_intro/ +qed-. + +lemma cpm_inv_flat1: ∀n,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[n, h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 & + U2 = ⓕ{I}V2.T2 + | (⦃G, L⦄ ⊢ U1 ➡[n, h] U2 ∧ I = Cast) + | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & I = Cast & n = ⫯m + | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ W1 ➡[h] W2 & + ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 & + U1 = ⓛ{p}W1.T1 & + U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl + | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V & ⬆*[1] V ≡ V2 & + ⦃G, L⦄ ⊢ W1 ➡[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 & + U1 = ⓓ{p}W1.T1 & + U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl. +#n #h #I #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_flat1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + /4 width=5 by or5_intro0, ex3_2_intro, ex2_intro/ +| #cU #U12 #H1 #H2 destruct + /5 width=3 by isrt_inv_plus_O_dx, or5_intro1, conj, ex2_intro/ +| #cU #H12 #H1 #H2 destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct + /4 width=3 by or5_intro2, ex3_intro, ex2_intro/ +| #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct + lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc + elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct + /4 width=11 by or5_intro3, ex6_6_intro, ex2_intro/ +| #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct + lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc + elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct + /4 width=13 by or5_intro4, ex7_7_intro, ex2_intro/ +] +qed-. + +lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 & + U2 = ⓐV2.T2 + | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ W1 ➡[h] W2 & + ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 & + U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 + | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V & ⬆*[1] V ≡ V2 & + ⦃G, L⦄ ⊢ W1 ➡[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 & + U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2. +#n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + /4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/ +| #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 destruct + lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc + elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct + /4 width=11 by or3_intro1, ex5_6_intro, ex2_intro/ +| #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 destruct + lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc + elim (isrt_inv_plus … Hc) -Hc #n0 #nT #Hc #HcT #H destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nW #HcV #HcW #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct + /4 width=13 by or3_intro2, ex6_7_intro, ex2_intro/ +] +qed-. + +lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n,h] T2 & + U2 = ⓝV2.T2 + | ⦃G, L⦄ ⊢ U1 ➡[n, h] U2 + | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & n = ⫯m. +#n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H * +[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct + elim (isrt_inv_plus … Hc) -Hc #nV #nT #HcV #HcT #H destruct + elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct + /4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/ +| #cU #U12 #H destruct + /4 width=3 by isrt_inv_plus_O_dx, or3_intro1, ex2_intro/ +| #cU #H12 #H destruct + elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct + /4 width=3 by or3_intro2, ex2_intro/ +] +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma cpm_fwd_bind1_minus: ∀n,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[n, h] T → ∀p. + ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] ⓑ{p,I}V2.T2 & + T = -ⓑ{I}V2.T2. +#n #h #I #G #L #V1 #T1 #T * #c #Hc #H #p elim (cpg_fwd_bind1_minus … H p) -H +/3 width=4 by ex2_2_intro, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index 966e4a17e..9900e8bf1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -26,9 +26,6 @@ interpretation (* Basic properties *********************************************************) -lemma cpx_atom: ∀h,I,G,L. ⦃G, L⦄ ⊢ ⓪{I} ⬈[h] ⓪{I}. -/2 width=2 by cpg_atom, ex_intro/ qed. - (* Basic_2A1: was: cpx_st *) lemma cpx_ess: ∀h,G,L,s. ⦃G, L⦄ ⊢ ⋆s ⬈[h] ⋆(next h s). /2 width=2 by cpg_ess, ex_intro/ qed. @@ -91,6 +88,7 @@ lemma cpx_theta: ∀h,p,G,L,V1,V,V2,W1,W2,T1,T2. /3 width=4 by cpg_theta, ex_intro/ qed. +(* Basic_2A1: includes: cpx_atom *) lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L). /2 width=2 by ex_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 4e25194d8..8658ca5cf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,3 +1,4 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma +cpm.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index 441d3c51f..c5762eacb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -49,7 +49,8 @@ lemma frees_lref_pushs: ∀f,K,j. K ⊢ 𝐅*⦃#j⦄ ≡ f → ∀i,L. ⬇*[i] L ≡ K → L ⊢ 𝐅*⦃#(i+j)⦄ ≡ ↑*[i] f. #f #K #j #Hf #i elim i -i [ #L #H lapply (drops_fwd_isid … H ?) -H // -| #i #IH #L #H elim (drops_inv_succ … H) -H /3 width=1 by frees_lref/ +| #i #IH #L #H elim (drops_inv_succ … H) -H + #I #Y #V #HYK #H destruct /3 width=1 by frees_lref/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 8ce8b954c..9fedf60c0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -51,6 +51,9 @@ qed. (* Equations ****************************************************************) +lemma plus_SO: ∀n. n + 1 = ⫯n. +// qed. + lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m. // qed-. @@ -155,6 +158,9 @@ qed. (* Inversion & forward lemmas ***********************************************) +lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0. +/2 width=1 by plus_le_0/ qed-. + lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0. // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isredtype_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isredtype_2.ma new file mode 100644 index 000000000..72275c55c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/isredtype_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( 𝐑𝐓 ⦃ term 46 n, break term 46 c ⦄ )" + non associative with precedence 45 + for @{ 'IsRedType $n $c }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma index cb25fdb89..cc4329acf 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma @@ -254,6 +254,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. +(* multiple existental quantifier (6, 8) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P5) }. + (* multiple existental quantifier (6, 9) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 , ident x8 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma index 0bf3c4da8..39211d7f2 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/nstream_istot.ma @@ -48,7 +48,8 @@ lemma at_istot: ∀f. 𝐓⦃f⦄. /2 width=2 by ex_intro/ qed. lemma at_plus2: ∀f,i1,i,n,m. @⦃i1, n@f⦄ ≡ i → @⦃i1, (m+n)@f⦄ ≡ m+i. -#f #i1 #i #n #m #H elim m -m /2 width=5 by at_next/ +#f #i1 #i #n #m #H elim m -m // +#m (plus_n_O n) /2 width=1 by isrt_plus/ +qed. + +lemma isrt_succ: ∀n,c. 𝐑𝐓⦃n, c⦄ → 𝐑𝐓⦃⫯n, c+𝟘𝟙⦄. +/2 width=1 by isrt_plus/ qed. + +(* Inversion properties with test for constrained rt-transition counter *****) + +lemma isrt_inv_plus: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → + ∃∃n1,n2. 𝐑𝐓⦃n1, c1⦄ & 𝐑𝐓⦃n2, c2⦄ & n1 + n2 = n. +#n #c1 #c2 * #ri #rs #H +elim (plus_inv_dx … H) -H #ri1 #rs1 #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #_ #_ #H1 #H2 #H3 #H4 +elim (plus_inv_O3 … H1) -H1 /3 width=5 by ex3_2_intro, ex1_2_intro/ +qed-. + +lemma isrt_inv_plus_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄. +#n #c1 #c2 #H #H2 +elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct +lapply (isrt_mono … Hn2 H2) -c2 #H destruct // +qed-. + +lemma isrt_inv_plus_SO_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃1, c2⦄ → + ∃∃m. 𝐑𝐓⦃m, c1⦄ & n = ⫯m. +#n #c1 #c2 #H #H2 +elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct +lapply (isrt_mono … Hn2 H2) -c2 #H destruct +/2 width=3 by ex2_intro/ +qed-. + +(* Properties with shift ****************************************************) + +lemma plus_shift: ∀c1,c2. (↓c1) + (↓c2) = ↓(c1+c2). +* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2 +6 5 6 6 6 7 + 6 8 6 9 7 3 7 4 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma index 7099edae0..af3c36d26 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -210,6 +210,14 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2 interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +(* multiple existental quantifier (6, 8) *) + +inductive ex6_8 (A0,A1,A2,A3,A4,A5,A6,A7:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→A7→Prop) : Prop ≝ + | ex6_8_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7. P0 x0 x1 x2 x3 x4 x5 x6 x7 → P1 x0 x1 x2 x3 x4 x5 x6 x7 → P2 x0 x1 x2 x3 x4 x5 x6 x7 → P3 x0 x1 x2 x3 x4 x5 x6 x7 → P4 x0 x1 x2 x3 x4 x5 x6 x7 → P5 x0 x1 x2 x3 x4 x5 x6 x7 → ex6_8 ? ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 8)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_8 ? ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). + (* multiple existental quantifier (6, 9) *) inductive ex6_9 (A0,A1,A2,A3,A4,A5,A6,A7,A8:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→A7→A8→Prop) : Prop ≝