From: Ferruccio Guidi Date: Sat, 21 May 2016 20:21:35 +0000 (+0000) Subject: - first results on cpx (dericed from those on cpg) X-Git-Tag: make_still_working~586 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e80b8d7a4b2c38729512dee28b3e0ecf9595c2a;p=helm.git - first results on cpx (dericed from those on cpg) - minor bugs fixed --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_cix.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_cix.etc new file mode 100644 index 000000000..9bb51aebc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_cix.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cix.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Advanced forward lemmas on irreducibility ********************************) + +lemma cpx_fwd_cix: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐈⦃T1⦄ → T2 = T1. +#h #o #G #L #T1 #T2 #H elim H -G -L -T1 -T2 +[ // +| #G #L #s #d #Hkd #H elim (cix_inv_sort … Hkd H) +| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H + elim (cix_inv_delta … HLK) // +| #a * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cix_inv_bind … H) -H #HV1 #HT1 * #H destruct + lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct + lapply (IHT1 … HT1) -IHT1 #H destruct // + | elim (cix_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/ + ] +| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H + [ elim (cix_inv_appl … H) -H #HV1 #HT1 #_ + >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // + | elim (cix_inv_ri2 … H) /2 width=1 by/ + ] +| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H + elim (cix_inv_ri2 … H) /2 width=1 by or_introl/ +| #G #L #V1 #T1 #T2 #_ #_ #H + elim (cix_inv_ri2 … H) /2 width=1 by/ +| #G #L #V1 #V2 #T #_ #_ #H + elim (cix_inv_ri2 … H) /2 width=1 by/ +| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H + elim (cix_inv_appl … H) -H #_ #_ #H + elim (simple_inv_bind … 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/etc_new/cpx/cpx_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_drops.etc new file mode 100644 index 000000000..3dd5f3a48 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_drops.etc @@ -0,0 +1,18 @@ +lemma cpx_delift: ∀h,I,G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓑ{I}V) → + ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h] T2 & ⬆[l, 1] T ≡ T2. +#h #o #I #G #K #V #T1 elim T1 -T1 +[ * #i #L #l /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/ + elim (lt_or_eq_or_gt i l) #Hil [1,3: /4 width=4 by cpx_atom, +lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ] + destruct + elim (lift_total V 0 (i+1)) #W #HVW + elim (lift_split … HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/ +| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK + elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 + [ elim (IHU1 (L. ⓑ{I} W1) (l+1)) -IHU1 /3 width=9 by cpx_bind, +drop_drop, lift_bind, ex2_2_intro/ + | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpx_flat, lift_flat, +ex2_2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc new file mode 100644 index 000000000..c769990b2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_length.etc @@ -0,0 +1 @@ +lemma cpx_inv_lref1_ge: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 → |L| ≤ i → T2 = #i. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_sta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_sta.etc new file mode 100644 index 000000000..3925f9d43 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/cpx/cpx_sta.etc @@ -0,0 +1,36 @@ +fact sta_cpx_aux: ∀h,o,G,L,T1,T2,d2,d1. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → d2 = 1 → + ⦃G, L⦄ ⊢ T1 ▪[h, o] d1+1 → ⦃G, L⦄ ⊢ T1 ➡[h, o] T2. +#h #o #G #L #T1 #T2 #d2 #d1 #H elim H -G -L -T1 -T2 -d2 +[ #G #L #d2 #s #H0 destruct normalize + /3 width=4 by cpx_st, da_inv_sort/ +| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #H0 #H destruct + elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 + lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/ +| #G #L #K #V1 #V2 #i #_ #_ #_ #H destruct +| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #HV12 #HVW2 #_ #H0 #H + lapply (discr_plus_xy_y … H0) -H0 #H0 destruct + elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 + lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct + /4 width=7 by cpx_delta, cpr_cpx, lstas_cpr/ +| /4 width=2 by cpx_bind, da_inv_bind/ +| /4 width=3 by cpx_flat, da_inv_flat/ +| /4 width=3 by cpx_eps, da_inv_flat/ +] +qed-. + +lemma sta_cpx: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → + ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 ➡[h, o] T2. +/2 width=3 by sta_cpx_aux/ qed. + +lemma fqu_sta_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 → + ∀d. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d+1 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. +/3 width=5 by fqu_cpx_trans, sta_cpx/ qed-. + +lemma fquq_sta_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 → + ∀d. ⦃G2, L2⦄ ⊢ T2 ▪[h, o] d+1 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +/3 width=5 by fquq_cpx_trans, sta_cpx/ qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index dc8f62eb0..91449b0ba 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -78,13 +78,13 @@ b: (q)rst-reduction c: conversion d: decomposed rt-reduction e: decomposed rt-conversion -g: generic rt-transition +g: counted rt-transition (generic) q: restricted reduction r: reduction s: substitution u: supclosure w: reserved for generic pointwise extension -x: rt-reduction +x: uncounted rt-transition (extended) y: rt-substitution - forth letter (if present) 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 deleted file mode 100644 index 397ac935f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_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 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 new file mode 100644 index 000000000..d2fe2d9f6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_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 T1 ➡ break [ term 46 h ] 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/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index d270bd2be..5dab2812e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -20,7 +20,7 @@ include "basic_2/grammar/genv.ma". include "basic_2/relocation/lifts.ma". include "basic_2/static/sh.ma". -(* CONTEXT-SENSITIVE GENERIC PARALLEL RT-TRANSITION FOR TERMS ***************) +(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) (* avtivate genv *) inductive cpg (h): rtc → relation4 genv lenv term term ≝ @@ -52,7 +52,7 @@ inductive cpg (h): rtc → relation4 genv lenv term term ≝ . interpretation - "context-sensitive generic parallel rt-transition (term)" + "counted context-sensitive parallel rt-transition (term)" 'PRed c h G L T1 T2 = (cpg h c G L T1 T2). (* Basic properties *********************************************************) @@ -266,10 +266,10 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma cpg_fwd_bind1_minus: ∀c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[c, h] T → ∀b. - ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,I}V1.T1 ➡[c, h] ⓑ{b,I}V2.T2 & +lemma cpg_fwd_bind1_minus: ∀c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[c, h] T → ∀p. + ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[c, h] ⓑ{p,I}V2.T2 & T = -ⓑ{I}V2.T2. -#c #h #I #G #L #V1 #T1 #T #H #b elim (cpg_inv_bind1 … H) -H * +#c #h #I #G #L #V1 #T1 #T #H #p elim (cpg_inv_bind1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct /3 width=4 by cpg_bind, ex2_2_intro/ | #c #T2 #_ #_ #H destruct ] 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 950b046a4..c8f0b394f 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 @@ -17,7 +17,7 @@ include "basic_2/s_computation/fqup_weight.ma". include "basic_2/s_computation/fqup_drops.ma". include "basic_2/rt_transition/cpg.ma". -(* CONTEXT-SENSITIVE GENERIC PARALLEL RT-TRANSITION FOR TERMS ***************) +(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) (* Advanced properties ******************************************************) @@ -61,6 +61,23 @@ lemma cpg_inv_lref1_drops: ∀c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ➡[c, h] T2 → ] qed-. +lemma cpg_inv_atom1_drops: ∀c,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[c, h] T2 → + ∨∨ T2 = ⓪{I} ∧ c = 𝟘𝟘 + | ∃∃s. T2 = ⋆(next h s) & I = Sort s & c = 𝟘𝟙 + | ∃∃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) + 𝟘𝟙. +#c #h * #n #G #L #T2 #H +[ elim (cpg_inv_sort1 … H) -H * + /3 width=3 by or4_intro0, or4_intro1, ex3_intro, conj/ +| elim (cpg_inv_lref1_drops … H) -H * + /3 width=10 by or4_intro0, or4_intro2, or4_intro3, ex5_5_intro, conj/ +| elim (cpg_inv_gref1 … H) -H + /3 width=1 by or4_intro0, conj/ +] +qed-. + (* Properties with generic slicing for local environments *******************) lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G). @@ -135,7 +152,7 @@ qed-. (* Inversion lemmas with generic slicing for local environments *************) -lemma cpg_inv_lift1: ∀c,h,G. d_deliftable2_sn (cpg h c G). +lemma cpg_inv_lifts1: ∀c,h,G. d_deliftable2_sn (cpg h c G). #c #h #G #L #U generalize in match c; -c @(fqup_wf_ind_eq … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * * [ #s #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct -IH 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 93d12c2ed..90f846e5a 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 @@ -15,7 +15,7 @@ include "basic_2/static/lsubr.ma". include "basic_2/rt_transition/cpg.ma". -(* CONTEXT-SENSITIVE GENERIC PARALLEL RT-TRANSITION FOR TERMS ***************) +(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) (* Properties with restricted refinement for local environments *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma index 53448a7bb..5dcf8ece0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg_simple.ma @@ -15,7 +15,7 @@ include "basic_2/grammar/term_simple.ma". include "basic_2/rt_transition/cpg.ma". -(* CONTEXT-SENSITIVE GENERIC PARALLEL RT-TRANSITION FOR TERMS ***************) +(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************) (* Properties with simple terms *********************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma index d5374513a..c05a2585d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma @@ -48,6 +48,11 @@ interpretation "context-sensitive parallel reduction (term)" (* Basic properties *********************************************************) +lemma cpr_cpx: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2. +#h #o #G #L #T1 #T2 #H elim H -L -T1 -T2 +/2 width=7 by cpx_delta, cpx_bind, cpx_flat, cpx_zeta, cpx_eps, cpx_beta, cpx_theta/ +qed. + lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr. #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 [ // 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 f7fd702e5..c40733142 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -12,293 +12,202 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/pred_6.ma". -include "basic_2/static/sd.ma". -include "basic_2/reduction/cpr.ma". - -(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) - -(* avtivate genv *) -inductive cpx (h) (o): relation4 genv lenv term term ≝ -| cpx_atom : ∀I,G,L. cpx h o G L (⓪{I}) (⓪{I}) -| cpx_st : ∀G,L,s,d. deg h o s (d+1) → cpx h o G L (⋆s) (⋆(next h s)) -| cpx_delta: ∀I,G,L,K,V,V2,W2,i. - ⬇[i] L ≡ K.ⓑ{I}V → cpx h o G K V V2 → - ⬆[0, i+1] V2 ≡ W2 → cpx h o G L (#i) W2 -| cpx_bind : ∀a,I,G,L,V1,V2,T1,T2. - cpx h o G L V1 V2 → cpx h o G (L.ⓑ{I}V1) T1 T2 → - cpx h o G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2) -| cpx_flat : ∀I,G,L,V1,V2,T1,T2. - cpx h o G L V1 V2 → cpx h o G L T1 T2 → - cpx h o G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2) -| cpx_zeta : ∀G,L,V,T1,T,T2. cpx h o G (L.ⓓV) T1 T → - ⬆[0, 1] T2 ≡ T → cpx h o G L (+ⓓV.T1) T2 -| cpx_eps : ∀G,L,V,T1,T2. cpx h o G L T1 T2 → cpx h o G L (ⓝV.T1) T2 -| cpx_ct : ∀G,L,V1,V2,T. cpx h o G L V1 V2 → cpx h o G L (ⓝV1.T) V2 -| cpx_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2. - cpx h o G L V1 V2 → cpx h o G L W1 W2 → cpx h o G (L.ⓛW1) T1 T2 → - cpx h o G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2) -| cpx_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. - cpx h o G L V1 V → ⬆[0, 1] V ≡ V2 → cpx h o G L W1 W2 → - cpx h o G (L.ⓓW1) T1 T2 → - cpx h o G L (ⓐV1.ⓓ{a}W1.T1) (ⓓ{a}W2.ⓐV2.T2) -. +include "basic_2/notation/relations/pred_5.ma". +include "basic_2/rt_transition/cpg.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS *****************) + +definition cpx (h): relation4 genv lenv term term ≝ + λG,L,T1,T2. ∃c. ⦃G, L⦄ ⊢ T1 ➡[c, h] T2. interpretation - "context-sensitive extended parallel reduction (term)" - 'PRed h o G L T1 T2 = (cpx h o G L T1 T2). + "uncounted context-sensitive parallel reduction (term)" + 'PRed h G L T1 T2 = (cpx h G L T1 T2). (* Basic properties *********************************************************) -lemma lsubr_cpx_trans: ∀h,o,G. lsub_trans … (cpx h o G) lsubr. -#h #o #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -[ // -| /2 width=2 by cpx_st/ -| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - elim (lsubr_fwd_drop2_pair … HL12 … HLK1) -HL12 -HLK1 * - /4 width=7 by cpx_delta, cpx_ct/ -|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_pair/ -|5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/ -|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsubr_pair/ -] -qed-. +lemma cpx_atom: ∀h,I,G,L. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] ⓪{I}. +/2 width=2 by cpg_atom, ex_intro/ qed. -(* Note: this is "∀h,g,L. reflexive … (cpx h g L)" *) -lemma cpx_refl: ∀h,o,G,T,L. ⦃G, L⦄ ⊢ T ➡[h, o] T. -#h #o #G #T elim T -T // * /2 width=1 by cpx_bind, cpx_flat/ +(* 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. + +lemma cpx_delta: ∀h,I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 → + ⬆*[1] V2 ≡ W2 → ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ➡[h] W2. +#h * #G #K #V1 #V2 #W2 * +/3 width=4 by cpg_delta, cpg_ell, ex_intro/ qed. -lemma cpr_cpx: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡[h, o] T2. -#h #o #G #L #T1 #T2 #H elim H -L -T1 -T2 -/2 width=7 by cpx_delta, cpx_bind, cpx_flat, cpx_zeta, cpx_eps, cpx_beta, cpx_theta/ +lemma cpx_lref: ∀h,I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ➡[h] T → + ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ➡[h] U. +#h #I #G #K #V #T #U #i * +/3 width=4 by cpg_lref, ex_intro/ qed. -lemma cpx_pair_sn: ∀h,o,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 → - ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡[h, o] ②{I}V2.T. -#h #o * /2 width=1 by cpx_bind, cpx_flat/ +lemma cpx_bind: ∀h,p,I,G,L,V1,V2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h] T2 → + ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[h] ⓑ{p,I}V2.T2. +#h #p #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 * +/3 width=2 by cpg_bind, ex_intro/ qed. -lemma cpx_delift: ∀h,o,I,G,K,V,T1,L,l. ⬇[l] L ≡ (K.ⓑ{I}V) → - ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 & ⬆[l, 1] T ≡ T2. -#h #o #I #G #K #V #T1 elim T1 -T1 -[ * #i #L #l /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/ - elim (lt_or_eq_or_gt i l) #Hil [1,3: /4 width=4 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ylt_inj, yle_inj, ex2_2_intro/ ] - destruct - elim (lift_total V 0 (i+1)) #W #HVW - elim (lift_split … HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/ -| * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #l #HLK - elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2 - [ elim (IHU1 (L. ⓑ{I} W1) (l+1)) -IHU1 /3 width=9 by cpx_bind, drop_drop, lift_bind, ex2_2_intro/ - | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpx_flat, lift_flat, ex2_2_intro/ - ] -] -qed-. +lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 → + ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[h] ⓕ{I}V2.T2. +#h #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 * +/3 width=2 by cpg_flat, ex_intro/ +qed. -(* Basic inversion lemmas ***************************************************) +lemma cpx_zeta: ∀h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ➡[h] T → + ⬆*[1] T2 ≡ T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡[h] T2. +#h #G #L #V #T1 #T #T2 * +/3 width=4 by cpg_zeta, ex_intro/ +qed. -fact cpx_inv_atom1_aux: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → ∀J. T1 = ⓪{J} → - ∨∨ T2 = ⓪{J} - | ∃∃s,d. deg h o s (d+1) & T2 = ⋆(next h s) & J = Sort s - | ∃∃I,K,V,V2,i. ⬇[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, o] V2 & - ⬆[O, i+1] V2 ≡ T2 & J = LRef i. -#G #h #o #L #T1 #T2 * -L -T1 -T2 -[ #I #G #L #J #H destruct /2 width=1 by or3_intro0/ -| #G #L #s #d #Hkd #J #H destruct /3 width=5 by or3_intro1, ex3_2_intro/ -| #I #G #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9 by or3_intro2, ex4_5_intro/ -| #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 -| #G #L #V1 #V2 #T #_ #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 cpx_eps: ∀h,G,L,V,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → ⦃G, L⦄ ⊢ ⓝV.T1 ➡[h] T2. +#h #G #L #V #T1 #T2 * +/3 width=2 by cpg_eps, ex_intro/ +qed. + +(* Basic_2A1: was: cpx_ct *) +lemma cpx_ee: ∀h,G,L,V1,V2,T. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ ⓝV1.T ➡[h] V2. +#h #G #L #V1 #V2 #T * +/3 width=2 by cpg_ee, ex_intro/ +qed. -lemma cpx_inv_atom1: ∀h,o,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h, o] T2 → +lemma cpx_beta: ∀h,p,G,L,V1,V2,W1,W2,T1,T2. + ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ W1 ➡[h] W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h] T2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ➡[h] ⓓ{p}ⓝW2.V2.T2. +#h #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 * #cV #HV12 * #cW #HW12 * +/3 width=2 by cpg_beta, ex_intro/ +qed. + +lemma cpx_theta: ∀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 ➡[h] T2 → + ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡[h] ⓓ{p}W2.ⓐV2.T2. +#h #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 * #cV #HV1 #HV2 * #cW #HW12 * +/3 width=4 by cpg_theta, ex_intro/ +qed. + +lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L). +/2 width=2 by ex_intro/ qed. + +lemma cpx_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=2 by cpg_pair_sn, ex_intro/ +qed. + +(* Basic inversion lemmas ***************************************************) + +lemma cpx_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h] T2 → ∨∨ T2 = ⓪{J} - | ∃∃s,d. deg h o s (d+1) & T2 = ⋆(next h s) & J = Sort s - | ∃∃I,K,V,V2,i. ⬇[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, o] V2 & - ⬆[O, i+1] V2 ≡ T2 & J = LRef i. -/2 width=3 by cpx_inv_atom1_aux/ qed-. - -lemma cpx_inv_sort1: ∀h,o,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[h, o] T2 → T2 = ⋆s ∨ - ∃∃d. deg h o s (d+1) & T2 = ⋆(next h s). -#h #o #G #L #T2 #s #H -elim (cpx_inv_atom1 … H) -H /2 width=1 by or_introl/ * -[ #s0 #d0 #Hkd0 #H1 #H2 destruct /3 width=4 by ex2_intro, or_intror/ -| #I #K #V #V2 #i #_ #_ #_ #H destruct -] + | ∃∃s. T2 = ⋆(next h s) & J = Sort s + | ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓑ{I}V1 & J = LRef 0 + | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[h] T & ⬆*[1] T ≡ T2 & + L = K.ⓑ{I}V & J = LRef (⫯i). +#h #J #G #L #T2 * #c #H elim (cpg_inv_atom1 … H) -H * +/4 width=9 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex4_5_intro, ex4_4_intro, ex2_intro, ex_intro/ qed-. -lemma cpx_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, o] T2 → - T2 = #i ∨ - ∃∃I,K,V,V2. ⬇[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, o] V2 & - ⬆[O, i+1] V2 ≡ T2. -#h #o #G #L #T2 #i #H -elim (cpx_inv_atom1 … H) -H /2 width=1 by or_introl/ * -[ #s #d #_ #_ #H destruct -| #I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7 by ex3_4_intro, or_intror/ -] +lemma cpx_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[h] T2 → + T2 = ⋆s ∨ T2 = ⋆(next h s). +#h #G #L #T2 #s * #c #H elim (cpg_inv_sort1 … H) -H * +/2 width=1 by or_introl, or_intror/ qed-. -lemma cpx_inv_lref1_ge: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, o] T2 → |L| ≤ i → T2 = #i. -#h #o #G #L #T2 #i #H elim (cpx_inv_lref1 … H) -H // * -#I #K #V1 #V2 #HLK #_ #_ #HL -h -G -V2 lapply (drop_fwd_length_lt2 … HLK) -K -I -V1 -#H elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ +lemma cpx_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[h] T2 → + T2 = #0 ∨ + ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓑ{I}V1. +#h #G #L #T2 * #c #H elim (cpg_inv_zero1 … H) -H * +/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/ qed-. -lemma cpx_inv_gref1: ∀h,o,G,L,T2,p. ⦃G, L⦄ ⊢ §p ➡[h, o] T2 → T2 = §p. -#h #o #G #L #T2 #p #H -elim (cpx_inv_atom1 … H) -H // * -[ #s #d #_ #_ #H destruct -| #I #K #V #V2 #i #_ #_ #_ #H destruct -] +lemma cpx_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ➡[h] T2 → + T2 = #(⫯i) ∨ + ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ➡[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V. +#h #G #L #T2 #i * #c #H elim (cpg_inv_lref1 … H) -H * +/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/ qed-. -fact cpx_inv_bind1_aux: ∀h,o,G,L,U1,U2. ⦃G, L⦄ ⊢ U1 ➡[h, o] U2 → - ∀a,J,V1,T1. U1 = ⓑ{a,J}V1.T1 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ T1 ➡[h, o] T2 & - U2 = ⓑ{a,J}V2.T2 - ) ∨ - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[h, o] T & ⬆[0, 1] U2 ≡ T & - a = true & J = Abbr. -#h #o #G #L #U1 #U2 * -L -U1 -U2 -[ #I #G #L #b #J #W #U1 #H destruct -| #G #L #s #d #_ #b #J #W #U1 #H destruct -| #I #G #L #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 by ex3_2_intro, or_introl/ -| #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 by ex4_intro, or_intror/ -| #G #L #V #T1 #T2 #_ #b #J #W #U1 #H destruct -| #G #L #V1 #V2 #T #_ #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 -] +lemma cpx_inv_gref1: ∀h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ➡[h] T2 → T2 = §l. +#h #G #L #T2 #l * #c #H elim (cpg_inv_gref1 … H) -H // qed-. -lemma cpx_inv_bind1: ∀h,o,a,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡[h, o] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h, o] T2 & - U2 = ⓑ{a,I} V2. T2 +lemma cpx_inv_bind1: ∀h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[h] U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[h] T2 & + U2 = ⓑ{p,I}V2.T2 ) ∨ - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[h, o] T & ⬆[0, 1] U2 ≡ T & - a = true & I = Abbr. -/2 width=3 by cpx_inv_bind1_aux/ qed-. - -lemma cpx_inv_abbr1: ∀h,o,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡[h, o] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[h, o] T2 & - U2 = ⓓ{a} V2. T2 - ) ∨ - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[h, o] T & ⬆[0, 1] U2 ≡ T & a = true. -#h #o #a #G #L #V1 #T1 #U2 #H -elim (cpx_inv_bind1 … H) -H * /3 width=5 by ex3_2_intro, ex3_intro, or_introl, or_intror/ + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[h] T & ⬆*[1] U2 ≡ T & + p = true & I = Abbr. +#h #p #I #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_bind1 … H) -H * +/4 width=5 by ex4_intro, ex3_2_intro, ex_intro, or_introl, or_intror/ qed-. -lemma cpx_inv_abst1: ∀h,o,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 ➡[h, o] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡[h, o] T2 & - U2 = ⓛ{a} V2. T2. -#h #o #a #G #L #V1 #T1 #U2 #H -elim (cpx_inv_bind1 … H) -H * -[ /3 width=5 by ex3_2_intro/ -| #T #_ #_ #_ #H destruct -] +lemma cpx_inv_abbr1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[h] U2 → ( + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[h] T2 & + U2 = ⓓ{p}V2.T2 + ) ∨ + ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[h] T & ⬆*[1] U2 ≡ T & p = true. +#h #p #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_abbr1 … H) -H * +/4 width=5 by ex3_2_intro, ex3_intro, ex_intro, or_introl, or_intror/ qed-. -fact cpx_inv_flat1_aux: ∀h,o,G,L,U,U2. ⦃G, L⦄ ⊢ U ➡[h, o] U2 → - ∀J,V1,U1. U = ⓕ{J}V1.U1 → - ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ U1 ➡[h, o] T2 & - U2 = ⓕ{J}V2.T2 - | (⦃G, L⦄ ⊢ U1 ➡[h, o] U2 ∧ J = Cast) - | (⦃G, L⦄ ⊢ V1 ➡[h, o] U2 ∧ J = Cast) - | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & - ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h, o] T2 & - U1 = ⓛ{a}W1.T1 & - U2 = ⓓ{a}ⓝW2.V2.T2 & J = Appl - | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V & ⬆[0,1] V ≡ V2 & - ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h, o] T2 & - U1 = ⓓ{a}W1.T1 & - U2 = ⓓ{a}W2.ⓐV2.T2 & J = Appl. -#h #o #G #L #U #U2 * -L -U -U2 -[ #I #G #L #J #W #U1 #H destruct -| #G #L #s #d #_ #J #W #U1 #H destruct -| #I #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 by or5_intro0, ex3_2_intro/ -| #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 by or5_intro1, conj/ -| #G #L #V1 #V2 #T #HV12 #J #W #U1 #H destruct /3 width=1 by or5_intro2, conj/ -| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=11 by or5_intro3, ex6_6_intro/ -| #a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=13 by or5_intro4, ex7_7_intro/ -] +lemma cpx_inv_abst1: ∀h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡[h] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡[h] T2 & + U2 = ⓛ{p}V2.T2. +#h #p #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_abst1 … H) -H +/3 width=5 by ex3_2_intro, ex_intro/ qed-. -lemma cpx_inv_flat1: ∀h,o,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[h, o] U2 → - ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ U1 ➡[h, o] T2 & - U2 = ⓕ{I} V2. T2 - | (⦃G, L⦄ ⊢ U1 ➡[h, o] U2 ∧ I = Cast) - | (⦃G, L⦄ ⊢ V1 ➡[h, o] U2 ∧ I = Cast) - | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & - ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h, o] T2 & - U1 = ⓛ{a}W1.T1 & - U2 = ⓓ{a}ⓝW2.V2.T2 & I = Appl - | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V & ⬆[0,1] V ≡ V2 & - ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h, o] T2 & - U1 = ⓓ{a}W1.T1 & - U2 = ⓓ{a}W2.ⓐV2.T2 & I = Appl. -/2 width=3 by cpx_inv_flat1_aux/ qed-. - -lemma cpx_inv_appl1: ∀h,o,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[h, o] U2 → - ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ U1 ➡[h, o] T2 & - U2 = ⓐ V2. T2 - | ∃∃a,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & - ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[h, o] T2 & - U1 = ⓛ{a}W1.T1 & U2 = ⓓ{a}ⓝW2.V2.T2 - | ∃∃a,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V & ⬆[0,1] V ≡ V2 & - ⦃G, L⦄ ⊢ W1 ➡[h, o] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h, o] T2 & - U1 = ⓓ{a}W1.T1 & U2 = ⓓ{a}W2. ⓐV2. T2. -#h #o #G #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H * -[ /3 width=5 by or3_intro0, ex3_2_intro/ -|2,3: #_ #H destruct -| /3 width=11 by or3_intro1, ex5_6_intro/ -| /3 width=13 by or3_intro2, ex6_7_intro/ -] +lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 & + U2 = ⓕ{I}V2.T2 + | (⦃G, L⦄ ⊢ U1 ➡[h] U2 ∧ I = Cast) + | (⦃G, L⦄ ⊢ V1 ➡[h] U2 ∧ I = Cast) + | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ W1 ➡[h] W2 & + ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[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 ➡[h] T2 & + U1 = ⓓ{p}W1.T1 & + U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl. +#h #I #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_flat1 … H) -H * +/4 width=14 by or5_intro0, or5_intro1, or5_intro2, or5_intro3, or5_intro4, ex7_7_intro, ex6_6_intro, ex3_2_intro, ex_intro, conj/ qed-. -(* Note: the main property of simple terms *) -lemma cpx_inv_appl1_simple: ∀h,o,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡[h, o] U → 𝐒⦃T1⦄ → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 & - U = ⓐV2.T2. -#h #o #G #L #V1 #T1 #U #H #HT1 -elim (cpx_inv_appl1 … H) -H * -[ /2 width=5 by ex3_2_intro/ -| #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct - elim (simple_inv_bind … HT1) -| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct - elim (simple_inv_bind … HT1) -] +lemma cpx_inv_appl1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[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 ➡[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 ➡[h] T2 & + U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2. +#h #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_appl1 … H) -H * +/4 width=13 by or3_intro0, or3_intro1, or3_intro2, ex6_7_intro, ex5_6_intro, ex3_2_intro, ex_intro/ qed-. -lemma cpx_inv_cast1: ∀h,o,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[h, o] U2 → - ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h, o] V2 & ⦃G, L⦄ ⊢ U1 ➡[h, o] T2 & - U2 = ⓝ V2. T2 - | ⦃G, L⦄ ⊢ U1 ➡[h, o] U2 - | ⦃G, L⦄ ⊢ V1 ➡[h, o] U2. -#h #o #G #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H * -[ /3 width=5 by or3_intro0, ex3_2_intro/ -|2,3: /2 width=1 by or3_intro1, or3_intro2/ -| #a #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #H destruct -| #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct -] +lemma cpx_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 & + U2 = ⓝV2.T2 + | ⦃G, L⦄ ⊢ U1 ➡[h] U2 + | ⦃G, L⦄ ⊢ V1 ➡[h] U2. +#h #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_cast1 … H) -H * +/4 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex_intro/ qed-. (* Basic forward lemmas *****************************************************) -lemma cpx_fwd_bind1_minus: ∀h,o,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[h, o] T → ∀b. - ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{b,I}V1.T1 ➡[h, o] ⓑ{b,I}V2.T2 & +lemma cpx_fwd_bind1_minus: ∀h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[h] T → ∀p. + ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[h] ⓑ{p,I}V2.T2 & T = -ⓑ{I}V2.T2. -#h #o #I #G #L #V1 #T1 #T #H #b -elim (cpx_inv_bind1 … H) -H * -[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4 by cpx_bind, ex2_2_intro/ -| #T2 #_ #_ #H destruct -] +#h #I #G #L #V1 #T1 #T * #c #H #p elim (cpg_fwd_bind1_minus … H p) -H +/3 width=4 by ex2_2_intro, ex_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_cix.ma deleted file mode 100644 index 9bb51aebc..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_cix.ma +++ /dev/null @@ -1,52 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/reduction/cix.ma". -include "basic_2/reduction/cpx.ma". - -(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) - -(* Advanced forward lemmas on irreducibility ********************************) - -lemma cpx_fwd_cix: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, o] T2 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐈⦃T1⦄ → T2 = T1. -#h #o #G #L #T1 #T2 #H elim H -G -L -T1 -T2 -[ // -| #G #L #s #d #Hkd #H elim (cix_inv_sort … Hkd H) -| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H - elim (cix_inv_delta … HLK) // -| #a * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H - [ elim (cix_inv_bind … H) -H #HV1 #HT1 * #H destruct - lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct - lapply (IHT1 … HT1) -IHT1 #H destruct // - | elim (cix_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/ - ] -| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H - [ elim (cix_inv_appl … H) -H #HV1 #HT1 #_ - >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // - | elim (cix_inv_ri2 … H) /2 width=1 by/ - ] -| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H - elim (cix_inv_ri2 … H) /2 width=1 by or_introl/ -| #G #L #V1 #T1 #T2 #_ #_ #H - elim (cix_inv_ri2 … H) /2 width=1 by/ -| #G #L #V1 #V2 #T #_ #_ #H - elim (cix_inv_ri2 … H) /2 width=1 by/ -| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H - elim (cix_inv_appl … H) -H #_ #_ #H - elim (simple_inv_bind … 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/rt_transition/cpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma new file mode 100644 index 000000000..6caaa1d76 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma @@ -0,0 +1,67 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/cpg_drops.ma". +include "basic_2/rt_transition/cpx.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS *****************) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was: cpx_delta *) +lemma cpx_delta_drops: ∀h,I,G,L,K,V,V2,W2,i. + ⬇*[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ➡[h] V2 → + ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[h] W2. +#h * #G #L #K #V #V2 #W2 #i #HLK * +/3 width=7 by cpg_ell_drops, cpg_delta_drops, ex_intro/ +qed. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_2A1: was: cpx_inv_atom1 *) +lemma cpx_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 → + ∨∨ T2 = ⓪{I} + | ∃∃s. T2 = ⋆(next h s) & I = Sort s + | ∃∃J,K,V,V2,i. ⬇*[i] L ≡ K.ⓑ{J}V & ⦃G, K⦄ ⊢ V ➡[h] V2 & + ⬆*[⫯i] V2 ≡ T2 & I = LRef i. +#h #I #G #L #T2 * #c #H elim (cpg_inv_atom1_drops … H) -H * +/4 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex2_intro, ex_intro/ +qed-. + +(* Basic_2A1: was: cpx_inv_lref1 *) +lemma cpx_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 → + T2 = #i ∨ + ∃∃J,K,V,V2. ⬇*[i] L ≡ K. ⓑ{J}V & ⦃G, K⦄ ⊢ V ➡[h] V2 & + ⬆*[⫯i] V2 ≡ T2. +#h #G #L #T1 #i * #c #H elim (cpg_inv_lref1_drops … H) -H * +/4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/ +qed-. + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: includes: cpx_lift *) +lemma cpx_lifts: ∀h,G. d_liftable2 (cpx h G). +#h #G #K #T1 #T2 * #cT #HT12 #b #f #L #HLK #U1 #HTU1 +elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1 +/3 width=4 by ex2_intro, ex_intro/ +qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: includes: cpx_inv_lift1 *) +lemma cpx_inv_lift1: ∀h,G. d_deliftable2_sn (cpx h G). +#h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1 +elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1 +/3 width=4 by ex2_intro, ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma new file mode 100644 index 000000000..645f59987 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -0,0 +1,120 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* Properties on supclosure *************************************************) + +lemma fqu_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/ +[ #I #G #L #V2 #U2 #HVU2 + elim (lift_total U2 0 1) + /4 width=7 by fqu_drop, cpx_delta, drop_pair, drop_drop, ex2_intro/ +| #G #L #K #T1 #U1 #k #HLK1 #HTU1 #T2 #HTU2 + elim (lift_total T2 0 (k+1)) + /3 width=11 by cpx_lift, fqu_drop, ex2_intro/ +] +qed-. + +lemma fquq_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H +[ #HT12 elim (fqu_cpx_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma fqup_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpx_trans … H12 … HTU2) -T2 + /3 width=3 by fqu_fqup, ex2_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 + elim (fqu_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2 + elim (IHT1 … HT2) -T /3 width=7 by fqup_strap1, ex2_intro/ +] +qed-. + +lemma fqus_cpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fqus_inv_gen … H) -H +[ #HT12 elim (fqup_cpx_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/ +| * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma fqu_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) + #U2 #HVU2 @(ex3_intro … U2) + [1,3: /3 width=7 by fqu_drop, cpx_delta, drop_pair, drop_drop/ + | #H destruct + lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 // + ] +| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) + [1,3: /2 width=4 by fqu_pair_sn, cpx_pair_sn/ + | #H0 destruct /2 width=1 by/ + ] +| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2)) + [1,3: /2 width=4 by fqu_bind_dx, cpx_bind/ + | #H0 destruct /2 width=1 by/ + ] +| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2)) + [1,3: /2 width=4 by fqu_flat_dx, cpx_flat/ + | #H0 destruct /2 width=1 by/ + ] +| #G #L #K #T1 #U1 #k #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (k+1)) + #U2 #HTU2 @(ex3_intro … U2) + [1,3: /2 width=10 by cpx_lift, fqu_drop/ + | #H0 destruct /3 width=5 by lift_inj/ +] +qed-. + +lemma fquq_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12 +[ #H12 elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. + +lemma fqup_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 + #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_neq … H1 … HTU1 H) -T1 + /3 width=8 by fqup_strap2, ex3_intro/ +] +qed-. + +lemma fqus_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, o] U2 → (T2 = U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12 +[ #H12 elim (fqup_cpx_trans_neq … H12 … HTU2 H) -T2 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /3 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lift.ma deleted file mode 100644 index 98f4a46be..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lift.ma +++ /dev/null @@ -1,267 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground_2/ynat/ynat_max.ma". -include "basic_2/substitution/drop_drop.ma". -include "basic_2/multiple/fqus_alt.ma". -include "basic_2/static/da.ma". -include "basic_2/reduction/cpx.ma". - -(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) - -(* Advanced properties ******************************************************) - -fact sta_cpx_aux: ∀h,o,G,L,T1,T2,d2,d1. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → d2 = 1 → - ⦃G, L⦄ ⊢ T1 ▪[h, o] d1+1 → ⦃G, L⦄ ⊢ T1 ➡[h, o] T2. -#h #o #G #L #T1 #T2 #d2 #d1 #H elim H -G -L -T1 -T2 -d2 -[ #G #L #d2 #s #H0 destruct normalize - /3 width=4 by cpx_st, da_inv_sort/ -| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #_ #HVW2 #IHV12 #H0 #H destruct - elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 - lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/ -| #G #L #K #V1 #V2 #i #_ #_ #_ #H destruct -| #G #L #K #V1 #V2 #W2 #i #d2 #HLK #HV12 #HVW2 #_ #H0 #H - lapply (discr_plus_xy_y … H0) -H0 #H0 destruct - elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 - lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct - /4 width=7 by cpx_delta, cpr_cpx, lstas_cpr/ -| /4 width=2 by cpx_bind, da_inv_bind/ -| /4 width=3 by cpx_flat, da_inv_flat/ -| /4 width=3 by cpx_eps, da_inv_flat/ -] -qed-. - -lemma sta_cpx: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 → - ⦃G, L⦄ ⊢ T1 ▪[h, o] d+1 → ⦃G, L⦄ ⊢ T1 ➡[h, o] T2. -/2 width=3 by sta_cpx_aux/ qed. - -(* Relocation properties ****************************************************) - -lemma cpx_lift: ∀h,o,G. d_liftable (cpx h o G). -#h #o #G #K #T1 #T2 #H elim H -G -K -T1 -T2 -[ #I #G #K #L #b #l #k #_ #U1 #H1 #U2 #H2 - >(lift_mono … H1 … H2) -H1 -H2 // -| #G #K #s #d #Hkd #L #b #l #k #_ #U1 #H1 #U2 #H2 - >(lift_inv_sort1 … H1) -U1 - >(lift_inv_sort1 … H2) -U2 /2 width=2 by cpx_st/ -| #I #G #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #b #l #k #HLK #U1 #H #U2 #HWU2 - elim (lift_inv_lref1 … H) * #Hil #H destruct - [ elim (lift_trans_ge … HVW2 … HWU2) -W2 /2 width=1 by ylt_fwd_le_succ1/ #W2 #HVW2 #HWU2 - elim (drop_trans_le … HLK … HKV) -K /2 width=2 by ylt_fwd_le/ #X #HLK #H - elim (drop_inv_skip2 … H) -H /2 width=1 by ylt_to_minus/ -Hil - #K #Y #HKV #HVY #H destruct /3 width=10 by cpx_delta/ - | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 /2 width=1 by yle_succ_dx/ >plus_plus_comm_23 #HVU2 - lapply (drop_trans_ge_comm … HLK … HKV ?) -K /3 width=7 by cpx_delta, drop_inv_gen/ - ] -| #a #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #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=6 by cpx_bind, drop_skip/ -| #I #G #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #b #l #k #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 by cpx_flat/ -| #G #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #b #l #k #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=6 by cpx_zeta, drop_skip/ -| #G #K #V #T1 #T2 #_ #IHT12 #L #b #l #k #HLK #U1 #H #U2 #HTU2 - elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_eps/ -| #G #K #V1 #V2 #T #_ #IHV12 #L #b #l #k #HLK #U1 #H #U2 #HVU2 - elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=6 by cpx_ct/ -| #a #G #K #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L #b #l #k #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=6 by cpx_beta, drop_skip/ -| #a #G #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #b #l #k #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 - elim (lift_inv_flat1 … HX) -HX #V3 #T3 #HV3 #HT23 #HX destruct - elim (lift_trans_ge … HV2 … HV3) -V2 /4 width=6 by cpx_theta, drop_skip/ -] -qed. - -lemma cpx_inv_lift1: ∀h,o,G. d_deliftable_sn (cpx h o G). -#h #o #G #L #U1 #U2 #H elim H -G -L -U1 -U2 -[ * #i #G #L #K #b #l #k #_ #T1 #H - [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_sort, ex2_intro/ - | elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=3 by cpx_atom, lift_lref_ge_minus, lift_lref_lt, ex2_intro/ - | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3 by cpx_atom, lift_gref, ex2_intro/ - ] -| #G #L #s #d #Hkd #K #b #l #k #_ #T1 #H - lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3 by cpx_st, lift_sort, ex2_intro/ -| #I #G #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #b #l #k #HLK #T1 #H - elim (lift_inv_lref2 … H) -H * #Hil #H destruct - [ elim (drop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV - elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2 - elim (lift_trans_le … HUV2 … HVW2) -V2 // yplus_SO2 >ymax_pre_sn /3 width=9 by cpx_delta, ylt_fwd_le_succ1, ex2_intro/ - | elim (yle_inv_plus_inj2 … Hil) #Hlim #Hmi - lapply (yle_inv_inj … Hmi) -Hmi #Hmi - lapply (drop_conf_ge … HLK … HLV ?) -L // #HKLV - elim (lift_split … HVW2 l (i - k + 1)) -HVW2 /3 width=1 by yle_succ, yle_pred_sn, le_S_S/ -Hil -Hlim - #V1 #HV1 >plus_minus //