(* *)
(**************************************************************************)
-include "basic_2/reduction/lpr_aaa.ma".
+include "basic_2/reduction/lpx_aaa.ma".
include "basic_2/computation/cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* *)
(**************************************************************************)
-include "basic_2/reduction/lpr_aaa.ma".
+include "basic_2/reduction/lpx_aaa.ma".
include "basic_2/computation/lprs.ma".
(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
-notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
- non associative with precedence 45
- for @{ 'PRedSn $L1 $L2 }.
-
notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )"
non associative with precedence 45
for @{ 'PRed $h $g $L $T1 $T2 }.
-notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ ➡ break [ term 46 g ] break term 46 T2 )"
+notation "hvbox( L1 ⊢ ➡ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'PRedSn $L1 $L2 }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 g ] break term 46 L2 )"
non associative with precedence 45
- for @{ 'PRedAlt $h $g $L $T1 $T2 }.
+ for @{ 'PRedSn $h $g $L1 $L2 }.
(* Computation **************************************************************)
non associative with precedence 45
for @{ 'PEval $L $T1 $T2 }.
-notation "hvbox( ⬊ * term 46 T )"
- non associative with precedence 45
- for @{ 'SN $T }.
-
notation "hvbox( L ⊢ ⬊ * break term 46 T )"
non associative with precedence 45
for @{ 'SN $L $T }.
non associative with precedence 45
for @{ 'SNAlt $L $T }.
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 g ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedStar $h $g $L $T1 $T2 }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 g ] break term 46 T )"
+ non associative with precedence 45
+ for @{ 'SN $h $g $L $T }.
+
+notation "hvbox( ⦃ term 46 h, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 46 g ] break term 46 T )"
+ non associative with precedence 45
+ for @{ 'SNAlt $h $g $L $T }.
+
notation "hvbox( ⦃ term 46 L, break term 46 T ⦄ ϵ break [ term 46 R ] break 〚term 46 A 〛 )"
non associative with precedence 45
for @{ 'InEInt $R $L $T $A }.
(* Basic_1: was: pr2_head_1 *)
lemma cpr_pair_sn: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 →
- ∀T. L⊢ ②{I}V1.T ➡ ②{I}V2.T.
+ ∀T. L ⊢ ②{I}V1.T ➡ ②{I}V2.T.
* /2 width=1/ qed.
lemma cpr_delift: ∀L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
inductive cpx (h) (g): lenv → relation term ≝
-| cpx_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → cpx h g L (⓪{I}) U2
-| cpx_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → cpx h g L (⓪{I}) U2
-| cpx_bind: ∀a,I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g (L.ⓑ{I}V1) T1 T2 →
- L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → cpx h g L (ⓑ{a,I}V1.T1) U2
-| cpx_flat: ∀I,L,V1,V2,T1,T2,U2. cpx h g L V1 V2 → cpx h g L T1 T2 →
- L ⊢ ⓕ{I}V2.T2 ➡ U2 → cpx h g L (ⓕ{I}V1.T1) U2
+| cpx_atom : ∀I,L. cpx h g L (⓪{I}) (⓪{I})
+| cpx_sort : ∀L,k,l. deg h g k (l+1) → cpx h g L (⋆k) (⋆(next h k))
+| cpx_delta: ∀I,L,K,V,V2,W2,i.
+ ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g K V V2 →
+ ⇧[0, i + 1] V2 ≡ W2 → cpx h g L (#i) W2
+| cpx_bind : ∀a,I,L,V1,V2,T1,T2.
+ cpx h g L V1 V2 → cpx h g (L. ⓑ{I} V1) T1 T2 →
+ cpx h g L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+| cpx_flat : ∀I,L,V1,V2,T1,T2.
+ cpx h g L V1 V2 → cpx h g L T1 T2 →
+ cpx h g L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+| cpx_zeta : ∀L,V,T1,T,T2. cpx h g (L.ⓓV) T1 T →
+ ⇧[0, 1] T2 ≡ T → cpx h g L (+ⓓV. T1) T2
+| cpx_tau : ∀L,V,T1,T2. cpx h g L T1 T2 → cpx h g L (ⓝV. T1) T2
+| cpx_beta : ∀a,L,V1,V2,W,T1,T2.
+ cpx h g L V1 V2 → cpx h g (L.ⓛW) T1 T2 →
+ cpx h g L (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2)
+| cpx_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2.
+ cpx h g L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g L W1 W2 → cpx h g (L.ⓓW1) T1 T2 →
+ cpx h g L (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV2. T2)
.
interpretation
(* Note: this is "∀h,g,L. reflexive … (cpx h g L)" *)
lemma cpx_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
-#h #g #T elim T -T /2 width=1/ * /2 width=5/
+#h #g #T elim T -T // * /2 width=1/
qed.
-lemma cpr_cpx: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
-#h #g #T1 elim T1 -T1 /2 width=1/ * /2 width=5/
+lemma cpr_cpx: ∀h,g,L,T1,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #L #T1 #T2 #H elim H -L -T1 -T2 // /2 width=1/ /2 width=3/ /2 width=7/
qed.
-lemma ssta_cpx: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
-#h #g #T1 elim T1 -T1 /2 width=2/ * [|*]
-[ #a #I #V1 #T1 #_ #IHT1 #L #X #l #H
- elim (ssta_inv_bind1 … H) -H #T2 #HT12 #H destruct /3 width=5/
-| #V1 #T1 #_ #IHT1 #L #X #l #H
- elim (ssta_inv_appl1 … H) -H #T2 #HT12 #H destruct /3 width=5/
-| #V1 #T1 #_ #IHT1 #L #X #l #H
- lapply (ssta_inv_cast1 … H) -H /3 width=5/
-]
+fact ssta_cpx_aux: ∀h,g,L,T1,T2,l0. ⦃h, L⦄ ⊢ T1 •[g] ⦃l0, T2⦄ →
+ ∀l. l0 = l+1 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+#h #g #L #T1 #T2 #l0 #H elim H -L -T1 -T2 -l0 /2 width=2/ /2 width=7/ /3 width=2/ /3 width=7/
+qed-.
+
+lemma ssta_cpx: ∀h,g,L,T1,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
+/2 width=4 by ssta_cpx_aux/ qed.
+
+lemma cpx_pair_sn: ∀h,g,I,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+ ∀T. ⦃h, L⦄ ⊢ ②{I}V1.T ➡[g] ②{I}V2.T.
+#h #g * /2 width=1/ qed.
+
+lemma cpx_delift: ∀h,g,L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
+ ∃∃T2,T. ⦃h, L⦄ ⊢ T1 ➡[g] T2 & ⇧[d, 1] T ≡ T2.
+#h #g #L #K #V #T1 #d #HLK
+elim (cpr_delift … HLK) -HLK /3 width=4/
+qed-.
+
+lemma cpx_append: ∀h,g. l_appendable_sn … (cpx h g).
+#h #g #K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/ /2 width=3/
+#I #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_ldrop2_length … HK0) #H
+@(cpx_delta … I … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpx_inv_atom1_aux: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ∀J. T1 = ⓪{J} →
+ ∨∨ T2 = ⓪{J}
+ | ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
+ | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ➡[g] V2 &
+ ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+#h #g #L #T1 #T2 * -L -T1 -T2
+[ #I #L #J #H destruct /2 width=1/
+| #L #k #l #Hkl #J #H destruct /3 width=5/
+| #I #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=9/
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T2 #_ #J #H destruct
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #J #H destruct
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #J #H destruct
+]
+qed-.
+
+lemma cpx_inv_atom1: ∀h,g,J,L,T2. ⦃h, L⦄ ⊢ ⓪{J} ➡[g] T2 →
+ ∨∨ T2 = ⓪{J}
+ | ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
+ | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃h, K⦄ ⊢ V ➡[g] V2 &
+ ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+/2 width=3 by cpx_inv_atom1_aux/ qed-.
+
+lemma cpx_inv_sort1: ∀h,g,L,T2,k. ⦃h, L⦄ ⊢ ⋆k ➡[g] T2 → T2 = ⋆k ∨
+ ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k).
+#h #g #L #T2 #k #H
+elim (cpx_inv_atom1 … H) -H /2 width=1/ *
+[ #k0 #l #Hkl #H1 #H2 destruct /3 width=4/
+| #I #K #V #V2 #i #_ #_ #_ #H destruct
+]
+qed-.
+
+lemma cpx_inv_lref1: ∀h,g,L,T2,i. ⦃h, L⦄ ⊢ #i ➡[g] T2 →
+ T2 = #i ∨
+ ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃h, K⦄ ⊢ V ➡[g] V2 &
+ ⇧[O, i + 1] V2 ≡ T2.
+#h #g #L #T2 #i #H
+elim (cpx_inv_atom1 … H) -H /2 width=1/ *
+[ #k #l #_ #_ #H destruct
+| #I #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=7/
+]
+qed-.
+
+lemma cpx_inv_gref1: ∀h,g,L,T2,p. ⦃h, L⦄ ⊢ §p ➡[g] T2 → T2 = §p.
+#h #g #L #T2 #p #H
+elim (cpx_inv_atom1 … H) -H // *
+[ #k #l #_ #_ #H destruct
+| #I #K #V #V2 #i #_ #_ #_ #H destruct
+]
+qed-.
+
+fact cpx_inv_bind1_aux: ∀h,g,L,U1,U2. ⦃h, L⦄ ⊢ U1 ➡[g] U2 →
+ ∀a,J,V1,T1. U1 = ⓑ{a,J} V1. T1 → (
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{J}V1⦄ ⊢ T1 ➡[g] T2 &
+ U2 = ⓑ{a,J} V2. T2
+ ) ∨
+ ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T &
+ a = true & J = Abbr.
+#h #g #L #U1 #U2 * -L -U1 -U2
+[ #I #L #b #J #W1 #U1 #H destruct
+| #L #k #l #_ #b #J #W1 #U1 #H destruct
+| #I #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #W1 #U1 #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #b #J #W1 #U1 #H destruct /3 width=5/
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
+| #L #V #T1 #T #T2 #HT1 #HT2 #b #J #W1 #U1 #H destruct /3 width=3/
+| #L #V #T1 #T2 #_ #b #J #W1 #U1 #H destruct
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #b #J #W1 #U1 #H destruct
+]
+qed-.
+
+lemma cpx_inv_bind1: ∀h,g,a,I,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡[g] U2 → (
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓑ{I}V1⦄ ⊢ T1 ➡[g] T2 &
+ U2 = ⓑ{a,I} V2. T2
+ ) ∨
+ ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T &
+ a = true & I = Abbr.
+/2 width=3 by cpx_inv_bind1_aux/ qed-.
+
+lemma cpx_inv_abbr1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓓ{a}V1.T1 ➡[g] U2 → (
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓓ V1⦄ ⊢ T1 ➡[g] T2 &
+ U2 = ⓓ{a} V2. T2
+ ) ∨
+ ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 ➡[g] T & ⇧[0, 1] U2 ≡ T & a = true.
+#h #g #a #L #V1 #T1 #U2 #H
+elim (cpx_inv_bind1 … H) -H * /3 width=3/ /3 width=5/
+qed-.
+
+lemma cpx_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1.T1 ➡[g] U2 →
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛ V1⦄ ⊢ T1 ➡[g] T2 &
+ U2 = ⓛ{a} V2. T2.
+#h #g #a #L #V1 #T1 #U2 #H
+elim (cpx_inv_bind1 … H) -H *
+[ /3 width=5/
+| #T #_ #_ #_ #H destruct
+]
+qed-.
+
+fact cpx_inv_flat1_aux: ∀h,g,L,U,U2. ⦃h, L⦄ ⊢ U ➡[g] U2 →
+ ∀J,V1,U1. U = ⓕ{J} V1. U1 →
+ ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+ U2 = ⓕ{J} V2. T2
+ | (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ J = Cast)
+ | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓛ{a}W. T1 &
+ U2 = ⓓ{a}V2. T2 & J = Appl
+ | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
+ ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓓ{a}W1. T1 &
+ U2 = ⓓ{a}W2. ⓐV2. T2 & J = Appl.
+#h #g #L #U #U2 * -L -U -U2
+[ #I #L #J #W1 #U1 #H destruct
+| #L #k #l #_ #J #W1 #U1 #H destruct
+| #I #L #K #V #V2 #W2 #i #_ #_ #_ #J #W1 #U1 #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #W1 #U1 #H destruct
+| #I #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=5/
+| #L #V #T1 #T #T2 #_ #_ #J #W1 #U1 #H destruct
+| #L #V #T1 #T2 #HT12 #J #W1 #U1 #H destruct /3 width=1/
+| #a #L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #W1 #U1 #H destruct /3 width=9/
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W1 #U1 #H destruct /3 width=13/
+]
+qed-.
+
+lemma cpx_inv_flat1: ∀h,g,I,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓕ{I}V1.U1 ➡[g] U2 →
+ ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+ U2 = ⓕ{I} V2. T2
+ | (⦃h, L⦄ ⊢ U1 ➡[g] U2 ∧ I = Cast)
+ | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓛ{a}W. T1 &
+ U2 = ⓓ{a}V2. T2 & I = Appl
+ | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
+ ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] 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,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓐ V1.U1 ➡[g] U2 →
+ ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+ U2 = ⓐ V2. T2
+ | ∃∃a,V2,W,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L.ⓛW⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓛ{a}W. T1 & U2 = ⓓ{a}V2. T2
+ | ∃∃a,V,V2,W1,W2,T1,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V & ⇧[0,1] V ≡ V2 &
+ ⦃h, L⦄ ⊢ W1 ➡[g] W2 & ⦃h, L.ⓓW1⦄ ⊢ T1 ➡[g] T2 &
+ U1 = ⓓ{a}W1. T1 & U2 = ⓓ{a}W2. ⓐV2. T2.
+#h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H *
+[ /3 width=5/
+| #_ #H destruct
+| /3 width=9/
+| /3 width=13/
+]
+qed-.
+
+(* Note: the main property of simple terms *)
+lemma cpx_inv_appl1_simple: ∀h,g,L,V1,T1,U. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡[g] U → 𝐒⦃T1⦄ →
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ T1 ➡[g] T2 &
+ U = ⓐV2. T2.
+#h #g #L #V1 #T1 #U #H #HT1
+elim (cpx_inv_appl1 … H) -H *
+[ /2 width=5/
+| #a #V2 #W #U1 #U2 #_ #_ #H #_ destruct
+ elim (simple_inv_bind … HT1)
+| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
+ elim (simple_inv_bind … HT1)
+]
+qed-.
+
+lemma cpx_inv_cast1: ∀h,g,L,V1,U1,U2. ⦃h, L⦄ ⊢ ⓝ V1.U1 ➡[g] U2 → (
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 & ⦃h, L⦄ ⊢ U1 ➡[g] T2 &
+ U2 = ⓝ V2. T2
+ ) ∨ ⦃h, L⦄ ⊢ U1 ➡[g] U2.
+#h #g #L #V1 #U1 #U2 #H elim (cpx_inv_flat1 … H) -H *
+[ /3 width=5/
+| /2 width=1/
+| #a #V2 #W #T1 #T2 #_ #_ #_ #_ #H destruct
+| #a #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpx_fwd_bind1_minus: ∀h,g,I,L,V1,T1,T. ⦃h, L⦄ ⊢ -ⓑ{I}V1.T1 ➡[g] T → ∀b.
+ ∃∃V2,T2. ⦃h, L⦄ ⊢ ⓑ{b,I}V1.T1 ➡[g] ⓑ{b,I}V2.T2 &
+ T = -ⓑ{I}V2.T2.
+#h #g #I #L #V1 #T1 #T #H #b
+elim (cpx_inv_bind1 … H) -H *
+[ #V2 #T2 #HV12 #HT12 #H destruct /3 width=4/
+| #T2 #_ #_ #H destruct
+]
+qed-.
+
+lemma cpx_fwd_shift1: ∀h,g,L1,L,T1,T. ⦃h, L⦄ ⊢ L1 @@ T1 ➡[g] T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#h #g #L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #L #T1 #T #HT1
+ @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #L #T1 #X
+ >shift_append_assoc normalize #H
+ elim (cpx_inv_bind1 … H) -H *
+ [ #V0 #T0 #_ #HT10 #H destruct
+ elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
+ >append_length >HL12 -HL12
+ @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
+ | #T #_ #_ #H destruct
+ ]
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/cpx.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
-
-include "basic_2/substitution/lpss_ldrop.ma".
-include "basic_2/substitution/fsups.ma".
-
-lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 →
- ∃∃U1. L1 ⊢ T1 ▶* U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄.
-#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ]
-[ * #L1
- [ #V2 #U2 #HVU2
- elim (lift_total U2 0 1) #W2 #HUW2
- @(ex2_intro … W2) /2 width=7/
- @(fsup_ldrop … L1 … HUW2) /2 width=1/
- | #W #U2 #H
- @(ex2_intro … (#0)) /2 width=7/
-
-| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
- elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2
- elim (lift_total T d e) #U #HTU
- lapply (cpss_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
-]
-qed-.
-
-
-
-(*
-include "basic_2/relocation/lift_lift.ma".
-include "basic_2/substitution/fsups.ma".
-*)
-(*
-lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
- ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
- ∃∃L,U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
-
-*)
-lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
- ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃ ⦃L2, U2⦄.
-#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
-[ * #L1 #V1 #U2 #l #H
- elim (lift_total U2 0 1) #W2 #HUW2
-(*
- [ @(ex2_intro … W2) [ @(cpx_ssta … l) @(ssta_ldef … H) //
- | @(fsups_ldrop … L1 … HUW2) /2 width=1/
-*)
-|
-| #a #I #L1 #V1 #T1 #U2 #l #HT1
- @(ex2_intro … (ⓑ{a,I}V1.U2)) /2 width=1/
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/relocation/ldrop_ldrop.ma".
+include "basic_2/relocation/fsupq.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpx_lift: ∀h,g. l_liftable (cpx h g).
+#h #g #K #T1 #T2 #H elim H -K -T1 -T2
+[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2
+ >(lift_mono … H1 … H2) -H1 -H2 //
+| #K #k #l #Hkl #L #d #e #_ #U1 #H1 #U2 #H2
+ >(lift_inv_sort1 … H1) -U1
+ >(lift_inv_sort1 … H2) -U2 /2 width=2/
+| #I #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
+ elim (lift_inv_lref1 … H) * #Hid #H destruct
+ [ elim (lift_trans_ge … HVW2 … HWU2) -W2 // <minus_plus #W2 #HVW2 #HWU2
+ elim (ldrop_trans_le … HLK … HKV) -K /2 width=2/ #X #HLK #H
+ elim (ldrop_inv_skip2 … H) -H /2 width=1/ -Hid #K #Y #HKV #HVY #H destruct /3 width=9/
+ | lapply (lift_trans_be … HVW2 … HWU2 ? ?) -W2 // /2 width=1/ >plus_plus_comm_23 #HVU2
+ lapply (ldrop_trans_ge_comm … HLK … HKV ?) -K // -Hid /3 width=7/
+ ]
+| #a #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_bind1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+ elim (lift_inv_bind1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /4 width=5/
+| #I #K #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+ elim (lift_inv_flat1 … H1) -H1 #VV1 #TT1 #HVV1 #HTT1 #H1 destruct
+ elim (lift_inv_flat1 … H2) -H2 #VV2 #TT2 #HVV2 #HTT2 #H2 destruct /3 width=6/
+| #K #V #T1 #T #T2 #_ #HT2 #IHT1 #L #d #e #HLK #U1 #H #U2 #HTU2
+ elim (lift_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
+ elim (lift_conf_O1 … HTU2 … HT2) -T2 /4 width=5/
+| #K #V #T1 #T2 #_ #IHT12 #L #d #e #HLK #U1 #H #U2 #HTU2
+ elim (lift_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct /3 width=5/
+| #a #K #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+ elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct
+ elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct
+ elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct /4 width=5/
+| #a #K #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L #d #e #HLK #X1 #HX1 #X2 #HX2
+ 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=5/
+]
+qed.
+
+lemma cpx_inv_lift1: ∀h,g. l_deliftable_sn (cpx h g).
+#h #g #L #U1 #U2 #H elim H -L -U1 -U2
+[ * #L #i #K #d #e #_ #T1 #H
+ [ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
+ | elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
+ | lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
+ ]
+| #L #k #l #Hkl #K #d #e #_ #T1 #H
+ lapply (lift_inv_sort2 … H) -H #H destruct /3 width=3/
+| #I #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
+ elim (lift_inv_lref2 … H) -H * #Hid #H destruct
+ [ elim (ldrop_conf_lt … HLK … HLV) -L // #L #U #HKL #HLV #HUV
+ elim (IHV2 … HLV … HUV) -V #U2 #HUV2 #HU2
+ elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m // -Hid /3 width=9/
+ | elim (le_inv_plus_l … Hid) #Hdie #Hei
+ lapply (ldrop_conf_ge … HLK … HLV ?) -L // #HKLV
+ elim (lift_split … HVW2 d (i - e + 1)) -HVW2 [4: // |3: /2 width=1/ |2: /3 width=1/ ] -Hid -Hdie
+ #V1 #HV1 >plus_minus // <minus_minus // /2 width=1/ <minus_n_n <plus_n_O /3 width=9/
+ ]
+| #a #I #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHV12 … HLK … HWV1) -IHV12 #W2 #HW12 #HWV2
+ elim (IHU12 … HTU1) -IHU12 -HTU1 /3 width=5/
+| #I #L #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHV12 … HLK … HWV1) -V1
+ elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5/
+| #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #X #H
+ elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHU1 (K.ⓓW1) … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+ elim (lift_div_le … HU2 … HTU) -U // /3 width=5/
+| #L #V #U1 #U2 #_ #IHU12 #K #d #e #HLK #X #H
+ elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
+ elim (IHU12 … HLK … HTU1) -L -U1 /3 width=3/
+| #a #L #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #K #d #e #HLK #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+ elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+ elim (IHV12 … HLK … HV01) -V1
+ elim (IHT12 (K.ⓛW0) … HT01) -T1 /2 width=1/ /3 width=5/
+| #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #K #d #e #HLK #X #HX
+ elim (lift_inv_flat2 … HX) -HX #V0 #Y #HV01 #HY #HX destruct
+ elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct
+ elim (IHV1 … HLK … HV01) -V1 #V3 #HV3 #HV03
+ elim (IHT12 (K.ⓓW0) … HT01) -T1 /2 width=1/ #T3 #HT32 #HT03
+ elim (IHW12 … HLK … HW01) -W1 #W3 #HW32 #HW03
+ elim (lift_trans_le … HV3 … HV2 ?) -V // #V #HV3 #HV2
+ @ex2_intro [2: /3 width=2/ | skip |3: /2 width=3/ ] (**) (* /4 width=5/ is slow *)
+]
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+lemma fsup_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2,3,4,5: /3 width=5/ ]
+[ #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+ elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2
+ elim (lift_total T d e) #U #HTU
+ lapply (cpx_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+| #I #L1 #V2 #U2 #HVU2
+ elim (lift_total U2 0 1) /4 width=9/
+]
+qed-.
+
+lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+/3 width=4 by fsup_cpx_trans, ssta_cpx/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/static/aaa_lift.ma".
-include "basic_2/static/lsuba_aaa.ma".
-include "basic_2/reduction/lpr_ldrop.ma".
-
-(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
-
-(* Properties on atomic arity assignment for terms **************************)
-
-lemma aaa_cpr_lpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. L1 ⊢ T1 ➡ T2 →
- ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T2 ⁝ A.
-#L1 #T1 #A #H elim H -L1 -T1 -A
-[ #L1 #k #X #H
- >(cpr_inv_sort1 … H) -H //
-| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
- elim (cpr_inv_lref1 … H) -H
- [ #H destruct
- elim (lpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
- elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
- | * #Y #Z #V2 #H #HV12 #HV2
- lapply (ldrop_mono … H … HLK1) -H #H destruct
- elim (lpr_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
- elim (lpr_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/
- ]
-| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpr_inv_abbr1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/
- | #T2 #HT12 #HT2 #H destruct -IHV1
- @(aaa_inv_lift (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/
- ]
-| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpr_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/
-| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpr_inv_appl1 … H) -H *
- [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/
- | #b #V2 #W1 #U1 #U2 #HV12 #HU12 #H1 #H2 destruct
- lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
- lapply (IHT1 (ⓛ{b}W1.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
- elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
- lapply (lsuba_aaa_trans … HU2 (L2.ⓓV2) ?) -HU2 /2 width=2/ /2 width=3/
- | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
- lapply (aaa_lift L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2
- lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
- elim (aaa_inv_abbr … H) -H /3 width=3/
- ]
-| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
- elim (cpr_inv_cast1 … H) -H
- [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/
- | -IHV1 /2 width=1/
- ]
-]
-qed-.
-
-lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A.
-/2 width=5 by aaa_cpr_lpr_conf/ qed-.
-
-lemma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A.
-/2 width=5 by aaa_cpr_lpr_conf/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/lpr.ma".
+include "basic_2/reduction/cpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+definition lpx: ∀h. sd h → relation lenv ≝ λh,g. lpx_sn (cpx h g).
+
+interpretation "extended parallel reduction (local environment, sn variant)"
+ 'PRedSn h g L1 L2 = (lpx h g L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpx_inv_atom1: ∀h,g,L2. ⦃h, ⋆⦄ ⊢ ➡[g] L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpx_inv_pair1: ∀h,g,I,K1,V1,L2. ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡[g] L2 →
+ ∃∃K2,V2. ⦃h, K1⦄ ⊢ ➡[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡[g] V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpx_inv_atom2: ∀h,g,L1. ⦃h, L1⦄ ⊢ ➡[g] ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpx_inv_pair2: ∀h,g,I,L1,K2,V2. ⦃h, L1⦄ ⊢ ➡[g] K2.ⓑ{I}V2 →
+ ∃∃K1,V1. ⦃h, K1⦄ ⊢ ➡[g] K2 & ⦃h, K1⦄ ⊢ V1 ➡[g] V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_refl: ∀h,g,L. ⦃h, L⦄ ⊢ ➡[g] L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpx_pair: ∀h,g,I,K1,K2,V1,V2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ⦃h, K1⦄ ⊢ V1 ➡[g] V2 →
+ ⦃h, K1.ⓑ{I}V1⦄ ⊢ ➡[g] K2.ⓑ{I}V2.
+/2 width=1/ qed.
+
+lemma lpx_append: ∀h,g,K1,K2. ⦃h, K1⦄ ⊢ ➡[g] K2 → ∀L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 →
+ ⦃h, L1 @@ K1⦄ ⊢ ➡[g] L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpx_append/ qed.
+
+lemma lpr_lpx: ∀h,g,L1,L2. L1 ⊢ ➡ L2 → ⦃h, L1⦄ ⊢ ➡[g] L2.
+#h #g #L1 #L2 #H elim H -L1 -L2 // /3 width=1/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_fwd_length: ∀h,g,L1,L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma lpx_fwd_append1: ∀h,g,K1,L1,L. ⦃h, K1 @@ L1⦄ ⊢ ➡[g] L →
+ ∃∃K2,L2. ⦃h, K1⦄ ⊢ ➡[g] K2 & L = K2 @@ L2.
+/2 width=2 by lpx_sn_fwd_append1/ qed-.
+
+lemma lpx_fwd_append2: ∀h,g,L,K2,L2. ⦃h, L⦄ ⊢ ➡[g] K2 @@ L2 →
+ ∃∃K1,L1. ⦃h, K1⦄ ⊢ ➡[g] K2 & L = K1 @@ L1.
+/2 width=2 by lpx_sn_fwd_append2/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/static/aaa_lift.ma".
+include "basic_2/static/lsuba_aaa.ma".
+include "basic_2/reduction/lpx_ldrop.ma".
+
+(* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
+
+(* Properties on atomic arity assignment for terms **************************)
+
+lemma aaa_cpx_lpx_conf: ∀h,g,L1,T1,A. L1 ⊢ T1 ⁝ A → ∀T2. ⦃h, L1⦄ ⊢ T1 ➡[g] T2 →
+ ∀L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → L2 ⊢ T2 ⁝ A.
+#h #g #L1 #T1 #A #H elim H -L1 -T1 -A
+[ #L1 #k #X #H
+ elim (cpx_inv_sort1 … H) -H // * //
+| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHV1 #X #H #L2 #HL12
+ elim (cpx_inv_lref1 … H) -H
+ [ #H destruct
+ elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
+ elim (lpx_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
+ | * #J #Y #Z #V2 #H #HV12 #HV2
+ lapply (ldrop_mono … H … HLK1) -H #H destruct
+ elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
+ elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/
+ ]
+| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_abbr1 … H) -H *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=2/
+ | #T2 #HT12 #HT2 #H destruct -IHV1
+ @(aaa_inv_lift (L2.ⓓV1) … HT2) -HT2 /2 width=1/ /3 width=1/
+ ]
+| #a #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct /4 width=1/
+| #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_appl1 … H) -H *
+ [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=3/
+ | #b #V2 #W1 #U1 #U2 #HV12 #HU12 #H1 #H2 destruct
+ lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2
+ lapply (IHT1 (ⓛ{b}W1.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
+ elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct
+ lapply (lsuba_aaa_trans … HU2 (L2.ⓓV2) ?) -HU2 /2 width=2/ /2 width=3/
+ | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct
+ lapply (aaa_lift L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=1/ #HV2
+ lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1/ -L1 #H
+ elim (aaa_inv_abbr … H) -H /3 width=3/
+ ]
+| #L1 #V1 #T1 #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
+ elim (cpx_inv_cast1 … H) -H
+ [ * #V2 #T2 #HV12 #HT12 #H destruct /3 width=1/
+ | -IHV1 /2 width=1/
+ ]
+]
+qed-.
+
+lemma aaa_cpx_conf: ∀h,g,L,T1,A. L ⊢ T1 ⁝ A → ∀T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → L ⊢ T2 ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
+lemma aaa_lpx_conf: ∀h,g,L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃h, L1⦄ ⊢ ➡[g] L2 → L2 ⊢ T ⁝ A.
+/2 width=7 by aaa_cpx_lpx_conf/ qed-.
+
+lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A.
+/3 width=5 by aaa_cpx_conf, cpr_cpx/ qed-.
+
+lemma aaa_lpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A.
+/3 width=5 by aaa_lpx_conf, lpr_lpx/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/relocation/ldrop_lpx_sn.ma".
+include "basic_2/reduction/cpx_lift.ma".
+include "basic_2/reduction/lpx.ma".
+
+(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpx_ldrop_conf: ∀h,g. dropable_sn (lpx h g).
+/3 width=5 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+
+lemma ldrop_lpx_trans: ∀h,g. dedropable_sn (lpx h g).
+/3 width=9 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+
+lemma lpx_ldrop_trans_O1: ∀h,g. dropable_dx (lpx h g).
+/2 width=3 by lpx_sn_dropable/ qed-.
(* SUPCLOSURE ***************************************************************)
inductive fsup: bi_relation lenv term ≝
-| fsup_lref : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
+| fsup_lref_O : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
| fsup_pair_sn: ∀I,L,V,T. fsup L (②{I}V.T) L V
| fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
| fsup_flat_dx: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T
@(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
qed-.
-fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|.
+fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀i. T1 = #i → |L2| < |L1|.
#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
[5: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
(* OPTIONAL SUPCLOSURE ******************************************************)
-definition fsupq: bi_relation lenv term ≝ bi_RC … fsup.
+inductive fsupq: bi_relation lenv term ≝
+| fsupq_refl : ∀L,T. fsupq L T L T
+| fsupq_lref_O : ∀I,L,V. fsupq (L.ⓑ{I}V) (#0) L V
+| fsupq_pair_sn: ∀I,L,V,T. fsupq L (②{I}V.T) L V
+| fsupq_bind_dx: ∀a,I,L,V,T. fsupq L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| fsupq_flat_dx: ∀I,L,V,T. fsupq L (ⓕ{I}V.T) L T
+| fsupq_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e.
+ ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
+ fsupq K1 T1 K2 T2 → fsupq L1 U1 K2 T2
+.
interpretation
"optional structural successor (closure)"
- 'SupTermOpt L1 T1 L2 T2 = (fsup L1 T1 L2 T2).
+ 'SupTermOpt L1 T1 L2 T2 = (fsupq L1 T1 L2 T2).
(* Basic properties *********************************************************)
-lemma fsupq_refl: bi_reflexive … fsupq.
-/2 width=1/ qed.
-
lemma fsup_fsupq: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄.
-/2 width=1/ qed.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=7/ qed.
+
+(* Basic properties *********************************************************)
+
+lemma fsupq_lref_S_lt: ∀I,L,K,V,T,i. 0 < i → ⦃L, #(i-1)⦄ ⊃⸮ ⦃K, T⦄ → ⦃L.ⓑ{I}V, #i⦄ ⊃⸮ ⦃K, T⦄.
+/3 width=7/ qed.
+
+lemma fsupq_lref: ∀I,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃L, #i⦄ ⊃⸮ ⦃K, V⦄.
+/3 width=2/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma fsupq_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ → ♯{L2, T2} ≤ ♯{L1, T1}.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // [1,2,3: /2 width=1/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
+lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
+lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
+@(transitive_le … IHT12) -IHT12 /2 width=1/
+qed-.
+
+fact fsupq_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
+ ∀i. T1 = #i → |L2| ≤ |L1|.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 //
+[ #a #I #L #V #T #j #H destruct
+| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
+ lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
+ @(transitive_le … HLK1) /2 width=2/
+]
+qed-.
+lemma fsupq_fwd_length_lref1: ∀L1,L2,T2,i. ⦃L1, #i⦄ ⊃⸮ ⦃L2, T2⦄ → |L2| ≤ |L1|.
+/2 width=5 by fsupq_fwd_length_lref1_aux/
+qed-.
next_lt: ∀k. k < next k (* strict monotonicity condition *)
}.
+definition sh_N: sh ≝ mk_sh S ….
+// qed.
+
(* Basic properties *********************************************************)
lemma nexts_le: ∀h,k,l. k ≤ (next h)^l k.
]
class "water"
[ { "reduction" * } {
+ [ { "context-sensitive extended reduction" * } {
+ [ "lpx ( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpx_ldrop" + "lpx_aaa" * ]
+ [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_lift" * ]
+ }
+ ]
[ { "context-sensitive normal forms" * } {
[ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_liftt" + "cnf_crf" + "cnf_cif" * ]
}
]
[ { "context-sensitive reduction" * } {
- [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpss" + "lpr_aaa" + "lpr_lpr" * ]
+ [ "lpr ( ? ⊢ ➡ ? )" "lpr_ldrop" + "lpr_lpss" + "lpr_lpr" * ]
[ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cif" * ]
}
]
class "orange"
[ { "relocation" * } {
[ { "structural successor for closures" * } {
- [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" * ]
+ [ "fsup ( ⦃?,?⦄ ⊃ ⦃?,?⦄ )" "fsupq ( ⦃?,?⦄ ⊃⸮ ⦃?,?⦄ )" * ]
}
]
[ { "global env. slicing" * } {
projects / helm.git / commitdiff