From a373e008bbacd40002c529f3f14da0939af1c404 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 19 May 2016 10:16:22 +0000 Subject: [PATCH] bug fix in cpg allows to prove lsubr_cpg_trans --- .../lambdadelta/basic_2/rt_transition/cpg.ma | 8 +- .../basic_2/rt_transition/cpg_drops.ma | 4 +- .../basic_2/rt_transition/cpg_lsubr.ma | 8 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 74 ++++++++++--------- 4 files changed, 48 insertions(+), 46 deletions(-) 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 22c671d90..d270bd2be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -27,7 +27,7 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝ | cpg_atom : ∀I,G,L. cpg h (𝟘𝟘) G L (⓪{I}) (⓪{I}) | cpg_ess : ∀G,L,s. cpg h (𝟘𝟙) G L (⋆s) (⋆(next h s)) | 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 + ⬆*[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 | cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T → @@ -73,7 +73,7 @@ fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[c, h] T2 → ∀ ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙 | ∃∃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 | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙 | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[c, h] T & ⬆*[1] T ≡ T2 & @@ -98,7 +98,7 @@ lemma cpg_inv_atom1: ∀c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[c, h] T2 → ∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘 | ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙 | ∃∃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 | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓛV1 & J = LRef 0 & c = (↓cV)+𝟘𝟙 | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[c, h] T & ⬆*[1] T ≡ T2 & @@ -118,7 +118,7 @@ qed-. lemma cpg_inv_zero1: ∀c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[c, h] T2 → ∨∨ (T2 = #0 ∧ c = 𝟘𝟘) | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 & - L = K.ⓓV1 & c = ↓cV + L = K.ⓓV1 & c = cV | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[cV, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓛV1 & c = (↓cV)+𝟘𝟙. #c #h #G #L #T2 #H 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 4ccf66fdf..950b046a4 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 @@ -22,7 +22,7 @@ include "basic_2/rt_transition/cpg.ma". (* Advanced properties ******************************************************) lemma cpg_delta_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_delta/ | #i #IH #L0 #T0 #H0 #HV2 #HVT2 @@ -46,7 +46,7 @@ qed. lemma cpg_inv_lref1_drops: ∀c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ➡[c, h] T2 → ∨∨ T2 = #i ∧ c = 𝟘𝟘 | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[cV, h] V2 & - ⬆*[⫯i] V2 ≡ T2 & c = ↓cV + ⬆*[⫯i] V2 ≡ T2 & c = cV | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[cV, h] V2 & ⬆*[⫯i] V2 ≡ T2 & c = (↓cV) + 𝟘𝟙. #c #h #G #i elim i -i diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma index f5b94d905..93d12c2ed 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_lsubr.ma @@ -22,18 +22,18 @@ include "basic_2/rt_transition/cpg.ma". lemma lsubr_cpg_trans: ∀c,h,G. lsub_trans … (cpg h c G) lsubr. #c #h #G #L1 #T1 #T2 #H elim H -c -G -L1 -T1 -T2 [ // -| /2 width=2 by cpg_st/ +| /2 width=2 by cpg_ess/ | #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H elim (lsubr_inv_abbr2 … H) -H #L2 #HL21 #H destruct /3 width=3 by cpg_delta/ | #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H elim (lsubr_inv_abst2 … H) -H * #L2 [2: #V ] #HL21 #H destruct - /4 width=3 by cpg_delta, cpg_lt, cpg_ct/ + /4 width=3 by cpg_delta, cpg_ell, cpg_ee/ | #c #I1 #G #L1 #V1 #T1 #U1 #i #_ #HTU1 #IH #X #H elim (lsubr_fwd_pair2 … H) -H #I2 #L2 #V2 #HL21 #H destruct - /3 width=3 by cpt_lref/ + /3 width=3 by cpg_lref/ |6,11: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/ -|7,9,10: /3 width=1 by cpg_flat, cpg_eps, cpg_ct/ +|7,9,10: /3 width=1 by cpg_flat, cpg_eps, cpg_ee/ |8,12: /4 width=3 by cpg_zeta, cpg_theta, lsubr_pair/ ] 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 9d6e316b0..a871f92bc 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 @@ -128,62 +128,32 @@ table { ] } ] +*) class "water" - [ { "reduction" * } { + [ { "rt-transition" * } { +(* [ { "parallel qrst-reduction" * } { [ "fpbq ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_alt ( ⦃?,?,?⦄ ≽≽[?,?] ⦃?,?,?⦄ )" "fpbq_lift" + "fpbq_aaa" * ] [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_lleq" + "fpb_fleq" * ] } ] - [ { "normal forms for context-sensitive rt-reduction" * } { - [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] - } - ] [ { "context-sensitive rt-reduction" * } { [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lreq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ] } ] - [ { "irreducible forms for context-sensitive rt-reduction" * } { - [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ] - } - ] - [ { "reducible forms for context-sensitive rt-reduction" * } { - [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ] - } - ] - [ { "normal forms for context-sensitive reduction" * } { - [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] - } - ] [ { "context-sensitive reduction" * } { [ "lpr ( ⦃?,?⦄ ⊢ ➡ ? )" "lpr_drop" + "lpr_lpr" * ] [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_llpx_sn" + "cpr_cir" * ] } ] - [ { "irreducible forms for context-sensitive reduction" * } { - [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ] - } - ] - [ { "reducible forms for context-sensitive reduction" * } { - [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ] - } - ] - } - ] - class "green" - [ { "unfold" * } { - [ { "unfold" * } { - [ "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ] - } - ] - [ { "iterated static type assignment" * } { - [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ] +*) + [ { "counted context-sensitive rt-transition" * } { + [ "cpg ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ] } ] } ] -*) class "green" [ { "static typing" * } { [ { "parameters" * } { @@ -299,6 +269,38 @@ class "capitalize italic" { 0 } class "italic" { 1 } (* + [ { "normal forms for context-sensitive rt-reduction" * } { + [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] + } + ] + [ { "irreducible forms for context-sensitive rt-reduction" * } { + [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ] + } + ] + [ { "reducible forms for context-sensitive rt-reduction" * } { + [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ] + } + ] + [ { "normal forms for context-sensitive reduction" * } { + [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] + } + ] + [ { "irreducible forms for context-sensitive reduction" * } { + [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ] + } + ] + [ { "reducible forms for context-sensitive reduction" * } { + [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ] + } + ] + [ { "unfold" * } { + [ "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ] + } + ] + [ { "iterated static type assignment" * } { + [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ] + } + ] [ { "local env. ref. for degree assignment" * } { [ "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ] } -- 2.39.2