]
}
]
- class "orange"
+ class "yellow"
[ { "MLTT1" * } {
[ { "" * } {
[ "genv_primitive" "judgement" * ]
]
}
]
- class "red"
+ class "orange"
[ { "functional" * } {
[ { "reduction and type machine" * } {
[ "rtm" "rtm_step ( ? ⇨ ? )" * ]
}
]
}
+ ]
+ class "red"
+ [ { "examples" * } {
+ [ { "" * } {
+ [ "" * ]
+ }
+ ]
+ }
]
}
lapply (cpcs_inv_lift … HLK … HVW … HVW0 ?) // -W /3 width=4/
]
qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma snv_fsup_conf: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g].
+#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
+[ #I1 #L1 #V1 #H
+ elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
+ lapply (ldrop_inv_refl … H) -H #H destruct //
+|2,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
+|4,5: * #L1 #V1 #T1 #H
+ [1,3: elim (snv_inv_appl … H) -H //
+ |2,4: elim (snv_inv_cast … H) -H //
+ ]
+| /3 width=7 by snv_inv_lift/
+]
+qed-.
interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+definition l_appendable_sn: predicate (lenv→relation term) ≝ λR.
+ ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
+
(* Basic properties *********************************************************)
lemma append_atom_sn: ∀L. ⋆ @@ L = L.
--- /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/grammar/lenv_append.ma".
+
+(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********)
+
+inductive lpx_sn (R:lenv→relation term): relation lenv ≝
+| lpx_sn_stom: lpx_sn R (⋆) (⋆)
+| lpx_sn_pair: ∀I,K1,K2,V1,V2.
+ lpx_sn R K1 K2 → R K1 V1 V2 →
+ lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2)
+.
+
+definition lpx_sn_confluent: predicate (lenv→relation term) ≝ λR.
+ ∀L0,T0,T1. R L0 T0 T1 → ∀T2. R L0 T0 T2 →
+ ∀L1. lpx_sn R L0 L1 → ∀L2. lpx_sn R L0 L2 →
+ ∃∃T. R L1 T1 T & R L2 T2 T.
+
+definition lpx_sn_transitive: predicate (lenv→relation term) ≝ λR.
+ ∀L1,T1,T. R L1 T1 T → ∀L2. lpx_sn R L1 L2 →
+ ∀T2. R L2 T T2 → R L1 T1 T2.
+
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+#R #L1 #L2 * -L1 -L2
+[ #J #K1 #V1 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 →
+ ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆.
+#R #L1 #L2 * -L1 -L2
+[ //
+| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct
+]
+qed-.
+
+lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
+#R #L1 #L2 * -L1 -L2
+[ #J #K2 #V2 #H destruct
+| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5/
+]
+qed-.
+
+lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) →
+ ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|.
+#R #L1 #L2 #H elim H -L1 -L2 normalize //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R).
+#R #HR #L elim L -L // /2 width=1/
+qed-.
+
+lemma lpx_sn_append: ∀R. l_appendable_sn R →
+ ∀K1,K2. lpx_sn R K1 K2 → ∀L1,L2. lpx_sn R L1 L2 →
+ lpx_sn R (L1 @@ K1) (L2 @@ K2).
+#R #HR #K1 #K2 #H elim H -K1 -K2 // /3 width=1/
+qed-.
+
+lemma lpx_sn_trans: ∀R. lpx_sn_transitive R → Transitive … (lpx_sn R).
+#R #HR #L1 #L #H elim H -L1 -L //
+#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
+elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5/
+qed-.
+
+lemma lpx_sn_conf: ∀R. lpx_sn_confluent R → confluent … (lpx_sn R).
+#R #HR #L0 @(f_ind … length … L0) -L0 #n #IH *
+[ #_ #X1 #H1 #X2 #H2 -n
+ >(lpx_sn_inv_atom1 … H1) -X1
+ >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3/
+| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+ elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
+ elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
+ elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
+ elim (HR … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
+]
+qed-.
f: flat
l: abstraction
n: native type annotation
+
+NAMING CONVENTIONS FOR TRANSFORMATIONS
+
+- first letter
+
+f: context-freee for closures
+l: sn contex-sensitive for terms
+r: dx contex-sensitive for terms
+t: context-free for terms
+
+-second letter
+
+p: parallel
+s: sequential
+
+- third letter
+
+c: conversion
+d: decomposed extended reduction
+q: restricted reduction
+r: reduction
+s: substitution
+x: extended reduction
+
+- forth letter (if present)
+
+p: non-reflexive transitive closure
+s: reflexive transitive closure
non associative with precedence 45
for @{ 'Unwind $L1 $T $L2 }.
+(* Restricted ***************************************************************)
+
+notation "hvbox( L ⊢ break term 46 T1 ➤ * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRestStar $L $T1 $T2 }.
+
+notation "hvbox( T1 ⊢ ➤ * break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRestStarSn $T1 $T2 }.
+
(* Reducibility *************************************************************)
notation "hvbox( L ⊢ break 𝐑 ⦃ term 46 T ⦄ )"
--- /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/unfold/cpss.ma".
+
+(* CONTEXT-SENSITIVE RESTRICTED PARALLEL COMPUTATION FOR TERMS **************)
+
+inductive cpqs: lenv → relation term ≝
+| cpqs_atom : ∀I,L. cpqs L (⓪{I}) (⓪{I})
+| cpqs_delta: ∀L,K,V,V2,W2,i.
+ ⇩[0, i] L ≡ K. ⓓV → cpqs K V V2 →
+ ⇧[0, i + 1] V2 ≡ W2 → cpqs L (#i) W2
+| cpqs_bind : ∀a,I,L,V1,V2,T1,T2.
+ cpqs L V1 V2 → cpqs (L. ⓑ{I} V1) T1 T2 →
+ cpqs L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
+| cpqs_flat : ∀I,L,V1,V2,T1,T2.
+ cpqs L V1 V2 → cpqs L T1 T2 →
+ cpqs L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
+| cpqs_zeta : ∀L,V,T1,T,T2. cpqs (L.ⓓV) T1 T →
+ ⇧[0, 1] T2 ≡ T → cpqs L (+ⓓV. T1) T2
+| cpqs_tau : ∀L,V,T1,T2. cpqs L T1 T2 → cpqs L (ⓝV. T1) T2
+.
+
+interpretation "context-sensitive restricted parallel computation (term)"
+ 'PRestStar L T1 T2 = (cpqs L T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Note: it does not hold replacing |L1| with |L2| *)
+lemma cpqs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➤* T2 →
+ ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➤* T2.
+#L1 #T1 #T2 #H elim H -L1 -T1 -T2
+[ //
+| #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
+ lapply (ldrop_fwd_ldrop2_length … HLK1) #Hi
+ lapply (ldrop_fwd_O1_length … HLK1) #H2i
+ elim (ldrop_lsubr_ldrop2_abbr … HL12 … HLK1 ? ?) -HL12 -HLK1 // -Hi
+ <H2i -H2i <minus_plus_m_m /3 width=6/
+| /4 width=1/
+| /3 width=1/
+| /4 width=3/
+| /3 width=1/
+]
+qed-.
+
+lemma cpss_cpqs: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ T1 ➤* T2.
+#L #T1 #T2 #H elim H -L -T1 -T2 // /2 width=1/ /2 width=6/
+qed.
+
+lemma cpqs_refl: ∀T,L. L ⊢ T ➤* T.
+/2 width=1/ qed.
+
+lemma cpqs_delift: ∀L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
+ ∃∃T2,T. L ⊢ T1 ➤* T2 & ⇧[d, 1] T ≡ T2.
+#L #K #V #T1 #d #HLK
+elim (cpss_delift … T1 … HLK) -HLK /3 width=4/
+qed-.
+
+lemma cpqs_append: l_appendable_sn … cpqs.
+#K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/ /2 width=3/
+#K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
+lapply (ldrop_fwd_ldrop2_length … HK0) #H
+@(cpqs_delta … (L@@K0) V1 … HVW2) //
+@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact cpqs_inv_atom1_aux: ∀L,T1,T2. L ⊢ T1 ➤* T2 → ∀I. T1 = ⓪{I} →
+ T2 = ⓪{I} ∨
+ ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV &
+ K ⊢ V ➤* V2 &
+ ⇧[O, i + 1] V2 ≡ T2 &
+ I = LRef i.
+#L #T1 #T2 * -L -T1 -T2
+[ #I #L #J #H destruct /2 width=1/
+| #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #J #H destruct /3 width=8/
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T #T2 #_ #_ #J #H destruct
+| #L #V #T1 #T2 #_ #J #H destruct
+]
+qed-.
+
+lemma cpqs_inv_atom1: ∀I,L,T2. L ⊢ ⓪{I} ➤* T2 →
+ T2 = ⓪{I} ∨
+ ∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV &
+ K ⊢ V ➤* V2 &
+ ⇧[O, i + 1] V2 ≡ T2 &
+ I = LRef i.
+/2 width=3 by cpqs_inv_atom1_aux/ qed-.
+
+lemma cpqs_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ➤* T2 → T2 = ⋆k.
+#L #T2 #k #H
+elim (cpqs_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+lemma cpqs_inv_lref1: ∀L,T2,i. L ⊢ #i ➤* T2 →
+ T2 = #i ∨
+ ∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV &
+ K ⊢ V ➤* V2 &
+ ⇧[O, i + 1] V2 ≡ T2.
+#L #T2 #i #H
+elim (cpqs_inv_atom1 … H) -H /2 width=1/
+* #K #V #V2 #j #HLK #HV2 #HVT2 #H destruct /3 width=6/
+qed-.
+
+lemma cpqs_inv_gref1: ∀L,T2,p. L ⊢ §p ➤* T2 → T2 = §p.
+#L #T2 #p #H
+elim (cpqs_inv_atom1 … H) -H //
+* #K #V #V2 #i #_ #_ #_ #H destruct
+qed-.
+
+fact cpqs_inv_bind1_aux: ∀L,U1,U2. L ⊢ U1 ➤* U2 →
+ ∀a,I,V1,T1. U1 = ⓑ{a,I} V1. T1 → (
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+ L. ⓑ{I} V1 ⊢ T1 ➤* T2 &
+ U2 = ⓑ{a,I} V2. T2
+ ) ∨
+ ∃∃T. L.ⓓV1 ⊢ T1 ➤* T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr.
+#L #U1 #U2 * -L -U1 -U2
+[ #I #L #b #J #W1 #U1 #H destruct
+| #L #K #V #V2 #W2 #i #_ #_ #_ #b #J #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
+]
+qed-.
+
+lemma cpqs_inv_bind1: ∀a,I,L,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ➤* U2 → (
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+ L. ⓑ{I} V1 ⊢ T1 ➤* T2 &
+ U2 = ⓑ{a,I} V2. T2
+ ) ∨
+ ∃∃T. L.ⓓV1 ⊢ T1 ➤* T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr.
+/2 width=3 by cpqs_inv_bind1_aux/ qed-.
+
+lemma cpqs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a} V1. T1 ➤* U2 → (
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+ L. ⓓ V1 ⊢ T1 ➤* T2 &
+ U2 = ⓓ{a} V2. T2
+ ) ∨
+ ∃∃T. L.ⓓV1 ⊢ T1 ➤* T & ⇧[0, 1] U2 ≡ T & a = true.
+#a #L #V1 #T1 #U2 #H
+elim (cpqs_inv_bind1 … H) -H * /3 width=3/ /3 width=5/
+qed-.
+
+lemma cpqs_inv_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a} V1. T1 ➤* U2 →
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 &
+ L. ⓛ V1 ⊢ T1 ➤* T2 &
+ U2 = ⓛ{a} V2. T2.
+#a #L #V1 #T1 #U2 #H
+elim (cpqs_inv_bind1 … H) -H *
+[ /3 width=5/
+| #T #_ #_ #_ #H destruct
+]
+qed-.
+
+fact cpqs_inv_flat1_aux: ∀L,U1,U2. L ⊢ U1 ➤* U2 →
+ ∀I,V1,T1. U1 = ⓕ{I} V1. T1 → (
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+ U2 = ⓕ{I} V2. T2
+ ) ∨
+ (L ⊢ T1 ➤* U2 ∧ I = Cast).
+#L #U1 #U2 * -L -U1 -U2
+[ #I #L #J #W1 #U1 #H destruct
+| #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/
+]
+qed-.
+
+lemma cpqs_inv_flat1: ∀I,L,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ➤* U2 → (
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+ U2 = ⓕ{I} V2. T2
+ ) ∨
+ (L ⊢ T1 ➤* U2 ∧ I = Cast).
+/2 width=3 by cpqs_inv_flat1_aux/ qed-.
+
+lemma cpqs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐ V1. T1 ➤* U2 →
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+ U2 = ⓐ V2. T2.
+#L #V1 #T1 #U2 #H elim (cpqs_inv_flat1 … H) -H *
+[ /3 width=5/
+| #_ #H destruct
+]
+qed-.
+
+lemma cpqs_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓝ V1. T1 ➤* U2 → (
+ ∃∃V2,T2. L ⊢ V1 ➤* V2 & L ⊢ T1 ➤* T2 &
+ U2 = ⓝ V2. T2
+ ) ∨
+ L ⊢ T1 ➤* U2.
+#L #V1 #T1 #U2 #H elim (cpqs_inv_flat1 … H) -H * /2 width=1/ /3 width=5/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpqs_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ➤* T →
+ ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#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 (cpqs_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/substitution/ldrop_ldrop.ma".
+include "basic_2/restricted/cpqs.ma".
+
+(* CONTEXT-SENSITIVE RESTRICTED PARALLEL COMPUTATION FOR TERMS **************)
+
+(* Relocation properties ****************************************************)
+
+lemma cpqs_lift: l_liftable cpqs.
+#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 #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=8/
+ | 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=6/
+ ]
+| #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/
+]
+qed.
+
+lemma cpqs_inv_lift1: l_deliftable_sn cpqs.
+#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 #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=8/
+ | 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=8/
+ ]
+| #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/
+]
+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/unfold/lpss.ma".
+include "basic_2/restricted/cpqs.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************)
+
+definition lpqs: relation lenv ≝ lpx_sn cpqs.
+
+interpretation "restricted parallel computation (local environment, sn variant)"
+ 'PRestStarSn L1 L2 = (lpqs L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpqs_inv_atom1: ∀L2. ⋆ ⊢ ➤* L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpqs_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ➤* L2 →
+ ∃∃K2,V2. K1 ⊢ ➤* K2 & K1 ⊢ V1 ➤* V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpqs_inv_atom2: ∀L1. L1 ⊢ ➤* ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpqs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➤* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ➤* K2 & K1 ⊢ V1 ➤* V2 & L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was by definition: csubst1_refl *)
+lemma lpqs_refl: ∀L. L ⊢ ➤* L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpqs_append: ∀K1,K2. K1 ⊢ ➤* K2 → ∀L1,L2. L1 ⊢ ➤* L2 →
+ L1 @@ K1 ⊢ ➤* L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpqs_append/ qed.
+
+lemma lpss_lpqs: ∀L1,L2. L1 ⊢ ▶* L2 → L1 ⊢ ➤* L2.
+#L1 #L2 #H elim H -L1 -L2 // /3 width=1/
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpqs_fwd_length: ∀L1,L2. L1 ⊢ ➤* L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ 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/substitution/fsup.ma".
+include "basic_2/restricted/lpqs_ldrop.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************)
+
+(* Main properties on context-sensitive rest parallel computation for terms *)
+
+fact cpqs_conf_lpqs_atom_atom:
+ ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ➤* T & L2 ⊢ ⓪{I} ➤* T.
+/2 width=3/ qed-.
+
+fact cpqs_conf_lpqs_atom_delta:
+ ∀L0,i. (
+ ∀L,T.♯{L, T} < ♯{L0, #i} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+ ∀V2. K0 ⊢ V0 ➤* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ #i ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
+elim (lpqs_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lpqs_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
+elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+elim (lift_total V 0 (i+1)) #T #HVT
+lapply (cpqs_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
+qed-.
+
+fact cpqs_conf_lpqs_delta_delta:
+ ∀L0,i. (
+ ∀L,T.♯{L, T} < ♯{L0, #i} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+ ∀V1. K0 ⊢ V0 ➤* V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 →
+ ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX →
+ ∀V2. KX ⊢ VX ➤* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ T1 ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1
+#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
+lapply (ldrop_mono … H … HLK0) -H #H destruct
+elim (lpqs_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lpqs_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
+elim (lpqs_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lpqs_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+elim (lift_total V 0 (i+1)) #T #HVT
+lapply (cpqs_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
+lapply (cpqs_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_bind_bind:
+ ∀a,I,L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀V1. L0 ⊢ V0 ➤* V1 → ∀T1. L0.ⓑ{I}V0 ⊢ T0 ➤* T1 →
+ ∀V2. L0 ⊢ V0 ➤* V2 → ∀T2. L0.ⓑ{I}V0 ⊢ T0 ➤* T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ ⓑ{a,I}V1.T1 ➤* T & L2 ⊢ ⓑ{a,I}V2.T2 ➤* T.
+#a #I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HV01 … HV02 … HL01 … HL02) //
+elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/
+qed-.
+
+fact cpqs_conf_lpqs_bind_zeta:
+ ∀L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀V1. L0 ⊢ V0 ➤* V1 → ∀T1. L0.ⓓV0 ⊢ T0 ➤* T1 →
+ ∀T2. L0.ⓓV0 ⊢ T0 ➤* T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ +ⓓV1.T1 ➤* T & L2 ⊢ X2 ➤* T.
+#L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 // /2 width=1/ -L0 -V0 -T0 #T #HT1 #HT2
+elim (cpqs_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ /3 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_zeta_zeta:
+ ∀L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,+ⓓV0.T0} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀T1. L0.ⓓV0 ⊢ T0 ➤* T1 → ∀X1. ⇧[O, 1] X1 ≡ T1 →
+ ∀T2. L0.ⓓV0 ⊢ T0 ➤* T2 → ∀X2. ⇧[O, 1] X2 ≡ T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ X1 ➤* T & L2 ⊢ X2 ➤* T.
+#L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
+#T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 // /2 width=1/ -L0 -T0 #T #HT1 #HT2
+elim (cpqs_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1/ #T1 #HT1 #HXT1
+elim (cpqs_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ #T2 #HT2 #HXT2
+lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_flat_flat:
+ ∀I,L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀V1. L0 ⊢ V0 ➤* V1 → ∀T1. L0 ⊢ T0 ➤* T1 →
+ ∀V2. L0 ⊢ V0 ➤* V2 → ∀T2. L0 ⊢ T0 ➤* T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ ⓕ{I}V1.T1 ➤* T & L2 ⊢ ⓕ{I}V2.T2 ➤* T.
+#I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HV01 … HV02 … HL01 … HL02) //
+elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
+qed-.
+
+fact cpqs_conf_lpqs_flat_tau:
+ ∀L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀V1,T1. L0 ⊢ T0 ➤* T1 → ∀T2. L0 ⊢ T0 ➤* T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ ⓝV1.T1 ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #V0 #T0 #IH #V1 #T1 #HT01
+#T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /3 width=3/
+qed-.
+
+fact cpqs_conf_lpqs_tau_tau:
+ ∀L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,ⓝV0.T0} →
+ ∀T1. L ⊢ T ➤* T1 → ∀T2. L ⊢ T ➤* T2 →
+ ∀L1. L ⊢ ➤* L1 → ∀L2. L ⊢ ➤* L2 →
+ ∃∃T0. L1 ⊢ T1 ➤* T0 & L2 ⊢ T2 ➤* T0
+ ) →
+ ∀T1. L0 ⊢ T0 ➤* T1 → ∀T2. L0 ⊢ T0 ➤* T2 →
+ ∀L1. L0 ⊢ ➤* L1 → ∀L2. L0 ⊢ ➤* L2 →
+ ∃∃T. L1 ⊢ T1 ➤* T & L2 ⊢ T2 ➤* T.
+#L0 #V0 #T0 #IH #T1 #HT01
+#T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HT01 … HT02 … HL01 … HL02) // -L0 -V0 -T0 /2 width=3/
+qed-.
+
+theorem cpqs_conf_lpqs: lpx_sn_confluent cpqs.
+#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
+[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpqs_inv_atom1 … H1) -H1
+ elim (cpqs_inv_atom1 … H2) -H2
+ [ #H2 #H1 destruct
+ /2 width=1 by cpqs_conf_lpqs_atom_atom/
+ | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct
+ /3 width=10 by cpqs_conf_lpqs_atom_delta/
+ | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct
+ /4 width=10 by ex2_commute, cpqs_conf_lpqs_atom_delta/
+ | * #X #Y #V2 #z #H #HV02 #HVT2 #H2
+ * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
+ /3 width=17 by cpqs_conf_lpqs_delta_delta/
+ ]
+| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpqs_inv_bind1 … H1) -H1 *
+ [ #V1 #T1 #HV01 #HT01 #H1
+ | #T1 #HT01 #HXT1 #H11 #H12
+ ]
+ elim (cpqs_inv_bind1 … H2) -H2 *
+ [1,3: #V2 #T2 #HV02 #HT02 #H2
+ |2,4: #T2 #HT02 #HXT2 #H21 #H22
+ ] destruct
+ [ /3 width=10 by cpqs_conf_lpqs_bind_bind/
+ | /4 width=11 by ex2_commute, cpqs_conf_lpqs_bind_zeta/
+ | /3 width=11 by cpqs_conf_lpqs_bind_zeta/
+ | /3 width=12 by cpqs_conf_lpqs_zeta_zeta/
+ ]
+| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpqs_inv_flat1 … H1) -H1 *
+ [ #V1 #T1 #HV01 #HT01 #H1
+ | #HX1 #H1
+ ]
+ elim (cpqs_inv_flat1 … H2) -H2 *
+ [1,3: #V2 #T2 #HV02 #HT02 #H2
+ |2,4: #HX2 #H2
+ ] destruct
+ [ /3 width=10 by cpqs_conf_lpqs_flat_flat/
+ | /4 width=8 by ex2_commute, cpqs_conf_lpqs_flat_tau/
+ | /3 width=8 by cpqs_conf_lpqs_flat_tau/
+ | /3 width=7 by cpqs_conf_lpqs_tau_tau/
+ ]
+]
+qed-.
+
+theorem cpqs_conf: ∀L. confluent … (cpqs L).
+/2 width=6 by cpqs_conf_lpqs/ qed-.
+
+theorem cpqs_trans_lpqs: lpx_sn_transitive cpqs.
+#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
+[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
+ elim (cpqs_inv_atom1 … H1) -H1
+ [ #H destruct
+ elim (cpqs_inv_atom1 … HT2) -HT2
+ [ #H destruct //
+ | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
+ elim (lpqs_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lpqs_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+ ]
+ | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
+ elim (lpqs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpqs_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+ elim (cpqs_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+ ]
+| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpqs_inv_bind1 … H1) -H1 *
+ [ #V #T #HV1 #HT1 #H destruct
+ elim (cpqs_inv_bind1 … H2) -H2 *
+ [ #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
+ | #T2 #HT2 #HXT2 #H1 #H2 destruct /4 width=5/
+ ]
+ | #Y1 #HTY1 #HXY1 #H11 #H12 destruct
+ elim (lift_total X2 0 1) #Y2 #HXY2
+ lapply (cpqs_lift … H2 (L2.ⓓV1) … HXY1 … HXY2) /2 width=1/ -X1 /4 width=5/
+ ]
+| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpqs_inv_flat1 … H1) -H1 *
+ [ #V #T #HV1 #HT1 #H destruct
+ elim (cpqs_inv_flat1 … H2) -H2 *
+ [ #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+ | #HX2 #H destruct /3 width=5/
+ ]
+ | #HX1 #H destruct /3 width=5/
+]
+qed-.
+
+theorem cpqs_trans: ∀L. Transitive … (cpqs L).
+/2 width=5 by cpqs_trans_lpqs/ qed-.
+
+(* Properties on context-sensitive rest. parallel computation for terms *****)
+
+lemma lpqs_cpqs_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➤* T1 → ∀L1. L0 ⊢ ➤* L1 →
+ ∃∃T. L1 ⊢ T0 ➤* T & L1 ⊢ T1 ➤* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpqs_conf_lpqs … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/
+qed-.
+
+lemma lpqs_cpqs_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➤* T1 → ∀L1. L0 ⊢ ➤* L1 →
+ ∃∃T. L1 ⊢ T0 ➤* T & L0 ⊢ T1 ➤* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpqs_conf_lpqs … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/
+qed-.
+
+lemma lpqs_cpqs_trans: ∀L1,L2. L1 ⊢ ➤* L2 →
+ ∀T1,T2. L2 ⊢ T1 ➤* T2 → L1 ⊢ T1 ➤* T2.
+/2 width=5 by cpqs_trans_lpqs/ qed-.
+
+lemma fsup_cpqs_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➤* U2 →
+ ∃∃L,U1. L1 ⊢ ➤* L & L ⊢ T1 ➤* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_lpqs_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K
+lapply (cpqs_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+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/substitution/ldrop_lpx_sn.ma".
+include "basic_2/restricted/cpqs_lift.ma".
+include "basic_2/restricted/lpqs.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ****************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpqs_ldrop_conf: dropable_sn lpqs.
+/3 width=5 by lpx_sn_deliftable_dropable, cpqs_inv_lift1/ qed-.
+
+lemma ldrop_lpqs_trans: dedropable_sn lpqs.
+/3 width=9 by lpx_sn_liftable_dedropable, cpqs_lift/ qed-.
+
+lemma lpqs_ldrop_trans_O1: dropable_dx lpqs.
+/2 width=3 by lpx_sn_dropable/ 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/restricted/lpqs_cpqs.ma".
+
+(* SN RESTRICTED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *****************)
+
+(* Main properties **********************************************************)
+
+theorem lpqs_conf: confluent … lpqs.
+/3 width=6 by lpx_sn_conf, cpqs_conf_lpqs/
+qed-.
+
+theorem lpqs_trans: Transitive … lpqs.
+/3 width=5 by lpx_sn_trans, cpqs_trans_lpqs/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpqs_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ➤* T →
+ ∃∃L2,T2. L @@ L1 ⊢ ➤* L @@ L2 & L @@ L1 ⊢ T1 ➤* T2 &
+ T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #HT1
+ @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
+ elim (cpqs_inv_bind1 … H) -H *
+ [ #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
+ lapply (lpqs_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1/ #HL12
+ @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3/ | skip ] <append_assoc // (**) (* explicit constructor *)
+ | #T #_ #_ #H destruct
+ ]
+]
+qed-.
]
qed-.
-lemma ltpx_dropable: ∀R. dropable_dx (lpx R).
+lemma lpx_dropable: ∀R. dropable_dx (lpx R).
/2 width=5 by lpx_dropable_aux/ 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/grammar/lenv_px_sn.ma".
+include "basic_2/substitution/ldrop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Properties on sn pointwise extension *************************************)
+
+lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R).
+#R #HR #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -L1 /3 width=3/
+| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (HR … HV12 … HLK1 … HWV1) -V1
+ elim (IHLK1 … HL12) -L1 /3 width=5/
+]
+qed-.
+
+lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) →
+ l_liftable R → dedropable_sn (lpx_sn R).
+#R #H1R #H2R #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H >(lpx_sn_inv_atom1 … H) -H /2 width=3/
+| #K1 #I #V1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+ elim (IHLK1 … HK12) -K1 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
+ elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
+ elim (lift_total W2 d e) #V2 #HWV2
+ lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1
+ elim (IHLK1 … HK12) -K1 /3 width=5/
+]
+qed-.
+
+fact lpx_sn_dropable_aux: ∀R,L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 →
+ d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & lpx_sn R K1 K2.
+#R #L2 #K2 #d #e #H elim H -L2 -K2 -d -e
+[ #d #e #X #H >(lpx_sn_inv_atom2 … H) -H /2 width=3/
+| #K2 #I #V2 #X #H
+ elim (lpx_sn_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
+| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
+ elim (lpx_sn_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
+ elim (IHLK2 … HL12 ?) -L2 // /3 width=3/
+| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
+ >commutative_plus normalize #H destruct
+]
+qed-.
+
+lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R).
+/2 width=5 by lpx_sn_dropable_aux/ qed-.
(* CONTEXT-SENSITIVE PARALLEL UNFOLD FOR TERMS ******************************)
inductive cpss: lenv → relation term ≝
-| cpss_atom : ∀L,I. cpss L (⓪{I}) (⓪{I})
-| cpss_subst: ∀L,K,V,V2,W2,i.
+| cpss_atom : ∀I,L. cpss L (⓪{I}) (⓪{I})
+| cpss_delta: ∀L,K,V,V2,W2,i.
⇩[0, i] L ≡ K. ⓓV → cpss K V V2 →
⇧[0, i + 1] V2 ≡ W2 → cpss L (#i) W2
-| cpss_bind : ∀L,a,I,V1,V2,T1,T2.
+| cpss_bind : ∀a,I,L,V1,V2,T1,T2.
cpss L V1 V2 → cpss (L. ⓑ{I} V1) T1 T2 →
cpss L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
-| cpss_flat : ∀L,I,V1,V2,T1,T2.
+| cpss_flat : ∀I,L,V1,V2,T1,T2.
cpss L V1 V2 → cpss L T1 T2 →
cpss L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
.
]
qed-.
+(* Basic_1: was by definition: subst1_refl *)
lemma cpss_refl: ∀T,L. L ⊢ T ▶* T.
#T elim T -T //
#I elim I -I /2 width=1/
qed.
+(* Basic_1: was only: subst1_ex *)
lemma cpss_delift: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) →
∃∃T2,T. L ⊢ T1 ▶* T2 & ⇧[d, 1] T ≡ T2.
#K #V #T1 elim T1 -T1
]
qed-.
-lemma cpss_append: ∀K,T1,T2. K ⊢ T1 ▶* T2 → ∀L. L @@ K ⊢ T1 ▶* T2.
+lemma cpss_append: l_appendable_sn … cpss.
#K #T1 #T2 #H elim H -K -T1 -T2 // /2 width=1/
#K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
lapply (ldrop_fwd_ldrop2_length … HK0) #H
-@(cpss_subst … (L@@K0) V1 … HVW2) //
+@(cpss_delta … (L@@K0) V1 … HVW2) //
@(ldrop_O1_append_sn_le … HK0) /2 width=2/ (**) (* /3/ does not work *)
qed.
⇧[O, i + 1] V2 ≡ T2 &
I = LRef i.
#L #T1 #T2 * -L -T1 -T2
-[ #L #I #J #H destruct /2 width=1/
+[ #I #L #J #H destruct /2 width=1/
| #L #K #V #V2 #T2 #i #HLK #HV2 #HVT2 #I #H destruct /3 width=8/
-| #L #a #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
-| #L #I #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #a #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
]
qed-.
-lemma cpss_inv_atom1: ∀L,T2,I. L ⊢ ⓪{I} ▶* T2 →
+lemma cpss_inv_atom1: ∀I,L,T2. L ⊢ ⓪{I} ▶* T2 →
T2 = ⓪{I} ∨
∃∃K,V,V2,i. ⇩[O, i] L ≡ K. ⓓV &
K ⊢ V ▶* V2 &
I = LRef i.
/2 width=3 by cpss_inv_atom1_aux/ qed-.
+(* Basic_1: was only: subst1_gen_sort *)
lemma cpss_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ▶* T2 → T2 = ⋆k.
#L #T2 #k #H
elim (cpss_inv_atom1 … H) -H //
* #K #V #V2 #i #_ #_ #_ #H destruct
qed-.
+(* Basic_1: was only: subst1_gen_lref *)
lemma cpss_inv_lref1: ∀L,T2,i. L ⊢ #i ▶* T2 →
T2 = #i ∨
∃∃K,V,V2. ⇩[O, i] L ≡ K. ⓓV &
L. ⓑ{I} V1 ⊢ T1 ▶* T2 &
U2 = ⓑ{a,I} V2. T2.
#L #U1 #U2 * -L -U1 -U2
-[ #L #k #a #I #V1 #T1 #H destruct
-| #L #K #V #V2 #W2 #i #_ #_ #_ #a #I #V1 #T1 #H destruct
-| #L #b #J #V1 #V2 #T1 #T2 #HV12 #HT12 #a #I #V #T #H destruct /2 width=5/
-| #L #J #V1 #V2 #T1 #T2 #_ #_ #a #I #V #T #H destruct
+[ #I #L #b #J #W1 #U1 #H destruct
+| #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 /2 width=5/
+| #I #L #V1 #V2 #T1 #T2 #_ #_ #b #J #W1 #U1 #H destruct
]
qed-.
-lemma cpss_inv_bind1: ∀L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* U2 →
+lemma cpss_inv_bind1: ∀a,I,L,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* U2 →
∃∃V2,T2. L ⊢ V1 ▶* V2 &
L. ⓑ{I} V1 ⊢ T1 ▶* T2 &
U2 = ⓑ{a,I} V2. T2.
∃∃V2,T2. L ⊢ V1 ▶* V2 & L ⊢ T1 ▶* T2 &
U2 = ⓕ{I} V2. T2.
#L #U1 #U2 * -L -U1 -U2
-[ #L #k #I #V1 #T1 #H destruct
-| #L #K #V #V2 #W2 #i #_ #_ #_ #I #V1 #T1 #H destruct
-| #L #a #J #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
-| #L #J #V1 #V2 #T1 #T2 #HV12 #HT12 #I #V #T #H destruct /2 width=5/
+[ #I #L #J #W1 #U1 #H destruct
+| #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 /2 width=5/
]
qed-.
-lemma cpss_inv_flat1: ∀L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* U2 →
+lemma cpss_inv_flat1: ∀I,L,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 ▶* U2 →
∃∃V2,T2. L ⊢ V1 ▶* V2 & L ⊢ T1 ▶* T2 &
U2 = ⓕ{I} V2. T2.
/2 width=3 by cpss_inv_flat1_aux/ qed-.
lemma cpss_fwd_tw: ∀L,T1,T2. L ⊢ T1 ▶* T2 → ♯{T1} ≤ ♯{T2}.
#L #T1 #T2 #H elim H -L -T1 -T2 normalize
-/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
+/3 width=1 by monotonic_le_plus_l, le_plus/ (**) (* auto is too slow without trace *)
qed-.
lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T →
@(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
]
qed-.
+
+(* Basic_1: removed theorems 27:
+ subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
+ subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
+ subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
+ subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt
+ subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
+ subst0_confluence_lift subst0_tlt
+ subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift
+ subst1_gen_lift_eq subst1_confluence_neq
+*)
(* Relocation properties ****************************************************)
+(* Basic_1: was only: subst1_lift_lt subst1_lift_ge *)
lemma cpss_lift: l_liftable cpss.
#K #T1 #T2 #H elim H -K -T1 -T2
-[ #K #I #L #d #e #_ #U1 #H1 #U2 #H2
+[ #I #K #L #d #e #_ #U1 #H1 #U2 #H2
>(lift_mono … H1 … H2) -H1 -H2 //
| #K #KV #V #V2 #W2 #i #HKV #HV2 #HVW2 #IHV2 #L #d #e #HLK #U1 #H #U2 #HWU2
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=8/
+ [ 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=8/
| 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=6/
]
-| #K #a #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+| #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/
-| #K #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L #d #e #HLK #U1 #H1 #U2 #H2
+| #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/
]
qed.
+(* Basic_1: was only: subst1_gen_lift_lt subst1_gen_lift_ge *)
lemma cpss_inv_lift1: l_deliftable_sn cpss.
#L #U1 #U2 #H elim H -L -U1 -U2
-[ #L * #i #K #d #e #_ #T1 #H
+[ * #L #i #K #d #e #_ #T1 #H
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
| elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=3/
| lapply (lift_inv_gref2 … H) -H #H destruct /2 width=3/
]
| #L #LV #V #V2 #W2 #i #HLV #HV2 #HVW2 #IHV2 #K #d #e #HLK #T1 #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
- [ elim (ldrop_conf_lt … HLK … HLV ?) -L // #L #U #HKL #HLV #HUV
+ [ 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=8/
+ elim (lift_trans_le … HUV2 … HVW2) -V2 // >minus_plus <plus_minus_m_m // -Hid /3 width=8/
| 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
+ 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=8/
]
-| #L #a #I #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+| #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/
-| #L #I #V1 #V2 #U1 #U2 #_ #_ #IHV12 #IHU12 #K #d #e #HLK #X #H
+| #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/
+++ /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/unfold/cpss.ma".
-
-(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
-
-inductive lcpss: relation lenv ≝
-| lcpss_atom: lcpss (⋆) (⋆)
-| lcpss_pair: ∀I,L1,L2,V1,V2. lcpss L1 L2 → L1 ⊢ V1 ▶* V2 →
- lcpss (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
-.
-
-interpretation "parallel unfold (local environment, sn variant)"
- 'PSubstStarSn L1 L2 = (lcpss L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact lcpss_inv_atom1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lcpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆.
-/2 width=5 by lcpss_inv_atom1_aux/ qed-.
-
-fact lcpss_inv_pair1_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
-#L1 #L2 * -L1 -L2
-[ #I #K1 #V1 #H destruct
-| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K1 #W1 #H destruct /2 width=5/
-]
-qed-.
-
-lemma lcpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 →
- ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
-/2 width=5 by lcpss_inv_pair1_aux/ qed-.
-
-fact lcpss_inv_atom2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → L2 = ⋆ → L1 = ⋆.
-#L1 #L2 * -L1 -L2
-[ //
-| #I #L1 #L2 #V1 #V2 #_ #_ #H destruct
-]
-qed-.
-
-lemma lcpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆.
-/2 width=5 by lcpss_inv_atom2_aux/ qed-.
-
-fact lcpss_inv_pair2_aux: ∀L1,L2. L1 ⊢ ▶* L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
-#L1 #L2 * -L1 -L2
-[ #I #K1 #V1 #H destruct
-| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #J #K2 #W2 #H destruct /2 width=5/
-]
-qed-.
-
-lemma lcpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
-/2 width=5 by lcpss_inv_pair2_aux/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lcpss_refl: ∀L. L ⊢ ▶* L.
-#L elim L -L // /2 width=1/
-qed.
-
-lemma lcpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 →
- L1 @@ K1 ⊢ ▶* L2 @@ K2.
-#K1 #K2 #H elim H -K1 -K2 // /3 width=1/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma lcpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|.
-#L1 #L2 #H elim H -L1 -L2 normalize //
-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/substitution/fsup.ma".
-include "basic_2/unfold/lcpss_ldrop.ma".
-
-(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
-
-(* Main properties on context-sensitive parallel unfold for terms ***********)
-
-fact cpss_conf_lcpss_aux: ∀L0,i. (
- ∀L,T0.♯{L, T0} < ♯{L0, #i} →
- ∀T1. L ⊢ T0 ▶* T1 → ∀T2. L ⊢ T0 ▶* T2 →
- ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
- ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T
- ) →
- ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
- ∀V2. K0 ⊢ V0 ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
- ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
- ∃∃T. L1 ⊢ #i ▶* T & L2 ⊢ T2 ▶* T.
-#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
-elim (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
-elim (lcpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
-elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
-elim (lcpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
-lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
-lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
-elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (lift_total V 0 (i+1)) #T #HVT
-lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
-qed-.
-
-theorem cpss_conf_lcpss: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀T2. L0 ⊢ T0 ▶* T2 →
- ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
- ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T.
-#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
-[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
- elim (cpss_inv_atom1 … H1) -H1
- elim (cpss_inv_atom1 … H2) -H2
- [ #H2 #H1 destruct /2 width=3/
- | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct
- /3 width=10 by cpss_conf_lcpss_aux/
- | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct
- /4 width=10 by ex2_commute, cpss_conf_lcpss_aux/
- | * #X #Y #V2 #z #H #HV02 #HVT2 #H2
- * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
- lapply (ldrop_mono … H … HLK0) -H #H destruct
- elim (lcpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
- elim (lcpss_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
- elim (lcpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
- elim (lcpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
- lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
- elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
- elim (lift_total V 0 (i+1)) #T #HVT
- lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
- lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/
- ]
-| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
- elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
- elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
- elim (IH … HV01 … HV02 … HL01 … HL02) //
- elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/
-| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
- elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
- elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
- elim (IH … HV01 … HV02 … HL01 … HL02) //
- elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
-]
-qed-.
-
-theorem cpss_conf: ∀L. confluent … (cpss L).
-/2 width=6 by cpss_conf_lcpss/ qed-.
-
-theorem cpss_trans_lcpss: ∀L1,T1,T. L1 ⊢ T1 ▶* T → ∀L2. L1 ⊢ ▶* L2 →
- ∀T2. L2 ⊢ T ▶* T2 → L1 ⊢ T1 ▶* T2.
-#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
-[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
- elim (cpss_inv_atom1 … H1) -H1
- [ #H destruct
- elim (cpss_inv_atom1 … HT2) -HT2
- [ #H destruct //
- | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
- elim (lcpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
- elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
- ]
- | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
- elim (lcpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
- elim (lcpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
- elim (cpss_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
- ]
-| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
- elim (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
- elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
-| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
- elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
- elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
-]
-qed-.
-
-theorem cpss_trans: ∀L. Transitive … (cpss L).
-/2 width=5 by cpss_trans_lcpss/ qed-.
-
-(* Properties on context-sensitive parallel unfold for terms ****************)
-
-lemma lcpss_cpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 →
- ∃∃T. L1 ⊢ T0 ▶* T & L1 ⊢ T1 ▶* T.
-#L0 #T0 #T1 #HT01 #L1 #HL01
-elim (cpss_conf_lcpss … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/
-qed-.
-
-lemma lcpss_cpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 →
- ∃∃T. L1 ⊢ T0 ▶* T & L0 ⊢ T1 ▶* T.
-#L0 #T0 #T1 #HT01 #L1 #HL01
-elim (cpss_conf_lcpss … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/
-qed-.
-
-lemma lcpss_cpss_trans: ∀L1,L2. L1 ⊢ ▶* L2 →
- ∀T1,T2. L2 ⊢ T1 ▶* T2 → L1 ⊢ T1 ▶* T2.
-/2 width=5 by cpss_trans_lcpss/ qed-.
-
-lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 →
- ∃∃L,U1. L1 ⊢ ▶* L & L ⊢ T1 ▶* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
-#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
-#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
-elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
-elim (lift_total T d e) #U #HTU
-elim (ldrop_lcpss_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K
-lapply (cpss_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
-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/unfold/lcpss_cpss.ma".
-
-(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
-
-(* Main properties **********************************************************)
-
-theorem lcpss_conf: confluent … lcpss.
-#L0 @(f_ind … length … L0) -L0 #n #IH *
-[ #_ #X1 #H1 #X2 #H2 -n
- >(lcpss_inv_atom1 … H1) -X1
- >(lcpss_inv_atom1 … H2) -X2 /2 width=3/
-| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
- elim (lcpss_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
- elim (lcpss_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
- elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
- elim (cpss_conf_lcpss … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5/
-]
-qed-.
-
-theorem lcpss_trans: Transitive … lcpss.
-#L1 #L #H elim H -L1 -L //
-#I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H
-elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct
-lapply (cpss_trans_lcpss … HV1 … HL1 … HV2) -V -HL1 /3 width=1/
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T →
- ∃∃L2,T2. L @@ L1 ⊢ ▶* L @@ L2 & L @@ L1 ⊢ T1 ▶* T2 &
- T = L2 @@ T2.
-#L1 @(lenv_ind_dx … L1) -L1
-[ #L #T1 #T #HT1
- @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
-| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
- elim (cpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
- lapply (lcpss_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1/ #HL12
- @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3/ | skip ] <append_assoc // (**) (* explicit constructor *)
-]
-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/unfold/cpss_lift.ma".
-include "basic_2/unfold/lcpss.ma".
-
-(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
-
-(* Properies on local environment slicing ***********************************)
-
-lemma lcpss_ldrop_conf: dropable_sn lcpss.
-#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #e #X #H
- lapply (lcpss_inv_atom1 … H) -H #H destruct /2 width=3/
-| #L1 #I #V1 #X #H
- elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=3/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #X #H
- elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=3/
-| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
- elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (cpss_inv_lift1 … HV12 … HLK1 … HWV1) -HLK1 -V1
- elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=5/
-]
-qed-.
-
-lemma ldrop_lcpss_trans: dedropable_sn lcpss.
-#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ #d #e #X #H
- lapply (lcpss_inv_atom1 … H) -H #H destruct /2 width=3/
-| #L1 #I #V1 #X #H
- elim (lcpss_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=3/
-| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
- elim (IHLK1 … HK12) -IHLK1 -HK12 /3 width=5/
-| #L1 #K1 #I #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H
- elim (lcpss_inv_pair1 … H) -H #L2 #W2 #HL12 #HW12 #H destruct
- elim (lift_total W2 d e) #V2 #HWV2
- lapply (cpss_lift … HW12 … HLK1 … HWV1 … HWV2) -W1 -HLK1
- elim (IHLK1 … HL12) -IHLK1 -HL12 /3 width=5/
-]
-qed-.
-
-fact lcpss_ldrop_trans_O1_aux: ∀L2,K2,d,e. ⇩[d, e] L2 ≡ K2 → ∀L1. L1 ⊢ ▶* L2 →
- d = 0 → ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 ⊢ ▶* K2.
-#L2 #K2 #d #e #H elim H -L2 -K2 -d -e
-[ #d #e #X #H >(lcpss_inv_atom2 … H) -H /2 width=3/
-| #K2 #I #V2 #X #H
- elim (lcpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct /3 width=5/
-| #L2 #K2 #I #V2 #e #_ #IHLK2 #X #H #_
- elim (lcpss_inv_pair2 … H) -H #L1 #V1 #HL12 #HV12 #H destruct
- elim (IHLK2 … HL12 ?) -L2 // /3 width=3/
-| #L2 #K2 #I #V2 #W2 #d #e #_ #_ #_ #L1 #_
- >commutative_plus normalize #H destruct
-]
-qed-.
-
-lemma lcpss_ldrop_trans_O1: dropable_dx lcpss.
-/2 width=5 by lcpss_ldrop_trans_O1_aux/ 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/grammar/lenv_px_sn.ma".
+include "basic_2/unfold/cpss.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Basic_1: includes: csubst1_bind *)
+definition lpss: relation lenv ≝ lpx_sn cpss.
+
+interpretation "parallel unfold (local environment, sn variant)"
+ 'PSubstStarSn L1 L2 = (lpss L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lpss_inv_atom1: ∀L2. ⋆ ⊢ ▶* L2 → L2 = ⋆.
+/2 width=4 by lpx_sn_inv_atom1_aux/ qed-.
+
+lemma lpss_inv_pair1: ∀I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* L2 →
+ ∃∃K2,V2. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L2 = K2. ⓑ{I} V2.
+/2 width=3 by lpx_sn_inv_pair1_aux/ qed-.
+
+lemma lpss_inv_atom2: ∀L1. L1 ⊢ ▶* ⋆ → L1 = ⋆.
+/2 width=4 by lpx_sn_inv_atom2_aux/ qed-.
+
+lemma lpss_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ▶* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ▶* K2 & K1 ⊢ V1 ▶* V2 & L1 = K1. ⓑ{I} V1.
+/2 width=3 by lpx_sn_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was by definition: csubst1_refl *)
+lemma lpss_refl: ∀L. L ⊢ ▶* L.
+/2 width=1 by lpx_sn_refl/ qed.
+
+lemma lpss_append: ∀K1,K2. K1 ⊢ ▶* K2 → ∀L1,L2. L1 ⊢ ▶* L2 →
+ L1 @@ K1 ⊢ ▶* L2 @@ K2.
+/3 width=1 by lpx_sn_append, cpss_append/ qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lpss_fwd_length: ∀L1,L2. L1 ⊢ ▶* L2 → |L1| = |L2|.
+/2 width=2 by lpx_sn_fwd_length/ qed-.
+
+(* Basic_1: removed theorems 28:
+ csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
+ csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
+ csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
+ csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt
+ csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back
+ csubst0_snd_bind csubst0_fst_bind csubst0_both_bind
+ csubst1_head csubst1_flat csubst1_gen_head
+ csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1
+ fsubst0_gen_base
+*)
--- /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/substitution/fsup.ma".
+include "basic_2/unfold/lpss_ldrop.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Main properties on context-sensitive parallel unfold for terms ***********)
+
+fact cpss_conf_lpss_atom_atom:
+ ∀I,L1,L2. ∃∃T. L1 ⊢ ⓪{I} ▶* T & L2 ⊢ ⓪{I} ▶* T.
+/2 width=3/ qed-.
+
+fact cpss_conf_lpss_atom_delta:
+ ∀L0,i. (
+ ∀L,T.♯{L, T} < ♯{L0, #i} →
+ ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
+ ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
+ ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
+ ) →
+ ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+ ∀V2. K0 ⊢ V0 ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
+ ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
+ ∃∃T. L1 ⊢ #i ▶* T & L2 ⊢ T2 ▶* T.
+#L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
+elim (lpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lpss_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
+elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+elim (lift_total V 0 (i+1)) #T #HVT
+lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 /3 width=6/
+qed-.
+
+fact cpss_conf_lpss_delta_delta:
+ ∀L0,i. (
+ ∀L,T.♯{L, T} < ♯{L0, #i} →
+ ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
+ ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
+ ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
+ ) →
+ ∀K0,V0. ⇩[O, i] L0 ≡ K0.ⓓV0 →
+ ∀V1. K0 ⊢ V0 ▶* V1 → ∀T1. ⇧[O, i + 1] V1 ≡ T1 →
+ ∀KX,VX. ⇩[O, i] L0 ≡ KX.ⓓVX →
+ ∀V2. KX ⊢ VX ▶* V2 → ∀T2. ⇧[O, i + 1] V2 ≡ T2 →
+ ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
+ ∃∃T. L1 ⊢ T1 ▶* T & L2 ⊢ T2 ▶* T.
+#L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1
+#KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
+lapply (ldrop_mono … H … HLK0) -H #H destruct
+elim (lpss_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
+elim (lpss_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
+elim (lpss_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
+elim (lpss_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
+lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_pair2_fwd_fw … HLK0 (#i)) -HLK0 #HLK0
+elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
+elim (lift_total V 0 (i+1)) #T #HVT
+lapply (cpss_lift … HV1 … HLK1 … HVT1 … HVT) -K1 -V1
+lapply (cpss_lift … HV2 … HLK2 … HVT2 … HVT) -K2 -V2 -V /2 width=3/
+qed-.
+
+fact cpss_conf_lpss_bind_bind:
+ ∀a,I,L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,ⓑ{a,I}V0.T0} →
+ ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
+ ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
+ ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
+ ) →
+ ∀V1. L0 ⊢ V0 ▶* V1 → ∀T1. L0.ⓑ{I}V0 ⊢ T0 ▶* T1 →
+ ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0.ⓑ{I}V0 ⊢ T0 ▶* T2 →
+ ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
+ ∃∃T. L1 ⊢ ⓑ{a,I}V1.T1 ▶* T & L2 ⊢ ⓑ{a,I}V2.T2 ▶* T.
+#a #I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HV01 … HV02 … HL01 … HL02) //
+elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH // /2 width=1/ /3 width=5/
+qed-.
+
+fact cpss_conf_lpss_flat_flat:
+ ∀I,L0,V0,T0. (
+ ∀L,T.♯{L,T} < ♯{L0,ⓕ{I}V0.T0} →
+ ∀T1. L ⊢ T ▶* T1 → ∀T2. L ⊢ T ▶* T2 →
+ ∀L1. L ⊢ ▶* L1 → ∀L2. L ⊢ ▶* L2 →
+ ∃∃T0. L1 ⊢ T1 ▶* T0 & L2 ⊢ T2 ▶* T0
+ ) →
+ ∀V1. L0 ⊢ V0 ▶* V1 → ∀T1. L0 ⊢ T0 ▶* T1 →
+ ∀V2. L0 ⊢ V0 ▶* V2 → ∀T2. L0 ⊢ T0 ▶* T2 →
+ ∀L1. L0 ⊢ ▶* L1 → ∀L2. L0 ⊢ ▶* L2 →
+ ∃∃T. L1 ⊢ ⓕ{I}V1.T1 ▶* T & L2 ⊢ ⓕ{I}V2.T2 ▶* T.
+#I #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
+#V2 #HV02 #T2 #HT02 #L1 #HL01 #L2 #HL02
+elim (IH … HV01 … HV02 … HL01 … HL02) //
+elim (IH … HT01 … HT02 … HL01 … HL02) // /3 width=5/
+qed-.
+
+theorem cpss_conf_lpss: lpx_sn_confluent cpss.
+#L0 #T0 @(f2_ind … fw … L0 T0) -L0 -T0 #n #IH #L0 * [|*]
+[ #I0 #Hn #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpss_inv_atom1 … H1) -H1
+ elim (cpss_inv_atom1 … H2) -H2
+ [ #H2 #H1 destruct
+ /2 width=1 by cpss_conf_lpss_atom_atom/
+ | * #K0 #V0 #V2 #i2 #HLK0 #HV02 #HVT2 #H2 #H1 destruct
+ /3 width=10 by cpss_conf_lpss_atom_delta/
+ | #H2 * #K0 #V0 #V1 #i1 #HLK0 #HV01 #HVT1 #H1 destruct
+ /4 width=10 by ex2_commute, cpss_conf_lpss_atom_delta/
+ | * #X #Y #V2 #z #H #HV02 #HVT2 #H2
+ * #K0 #V0 #V1 #i #HLK0 #HV01 #HVT1 #H1 destruct
+ /3 width=17 by cpss_conf_lpss_delta_delta/
+ ]
+| #a #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpss_inv_bind1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
+ elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
+ /3 width=10 by cpss_conf_lpss_bind_bind/
+| #I #V0 #T0 #Hn #X1 #H1 #X2 #H2 #L1 #HL01 #L2 #HL02 destruct
+ elim (cpss_inv_flat1 … H1) -H1 #V1 #T1 #HV01 #HT01 #H destruct
+ elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV02 #HT02 #H destruct
+ /3 width=10 by cpss_conf_lpss_flat_flat/
+]
+qed-.
+
+(* Basic_1: was only: subst1_confluence_eq *)
+theorem cpss_conf: ∀L. confluent … (cpss L).
+/2 width=6 by cpss_conf_lpss/ qed-.
+
+theorem cpss_trans_lpss: lpx_sn_transitive cpss.
+#L1 #T1 @(f2_ind … fw … L1 T1) -L1 -T1 #n #IH #L1 * [|*]
+[ #I #Hn #T #H1 #L2 #HL12 #T2 #HT2 destruct
+ elim (cpss_inv_atom1 … H1) -H1
+ [ #H destruct
+ elim (cpss_inv_atom1 … HT2) -HT2
+ [ #H destruct //
+ | * #K2 #V #V2 #i #HLK2 #HV2 #HVT2 #H destruct
+ elim (lpss_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lpss_inv_pair2 … H) -H #K1 #V1 #HK12 #HV1 #H destruct
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+ ]
+ | * #K1 #V1 #V #i #HLK1 #HV1 #HVT #H destruct
+ elim (lpss_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+ elim (lpss_inv_pair1 … H) -H #K2 #W2 #HK12 #_ #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+ elim (cpss_inv_lift1 … HT2 … HLK2 … HVT) -L2 -T
+ lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) /3 width=9/
+ ]
+| #a #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpss_inv_bind1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+ elim (cpss_inv_bind1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
+| #I #V1 #T1 #Hn #X1 #H1 #L2 #HL12 #X2 #H2
+ elim (cpss_inv_flat1 … H1) -H1 #V #T #HV1 #HT1 #H destruct
+ elim (cpss_inv_flat1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+]
+qed-.
+
+(* Basic_1: was only: subst1_trans *)
+theorem cpss_trans: ∀L. Transitive … (cpss L).
+/2 width=5 by cpss_trans_lpss/ qed-.
+
+(* Properties on context-sensitive parallel unfold for terms ****************)
+
+(* Basic_1: was only: subst1_subst1_back *)
+lemma lpss_cpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 →
+ ∃∃T. L1 ⊢ T0 ▶* T & L1 ⊢ T1 ▶* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpss_conf_lpss … HT01 T0 … HL01 … HL01) // -L0 /2 width=3/
+qed-.
+
+lemma lpss_cpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ▶* T1 → ∀L1. L0 ⊢ ▶* L1 →
+ ∃∃T. L1 ⊢ T0 ▶* T & L0 ⊢ T1 ▶* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cpss_conf_lpss … HT01 T0 … L0 … HL01) // -HT01 -HL01 /2 width=3/
+qed-.
+
+(* Basic_1: was only: subst1_subst1 *)
+lemma lpss_cpss_trans: ∀L1,L2. L1 ⊢ ▶* L2 →
+ ∀T1,T2. L2 ⊢ T1 ▶* T2 → L1 ⊢ T1 ▶* T2.
+/2 width=5 by cpss_trans_lpss/ qed-.
+
+lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 →
+ ∃∃L,U1. L1 ⊢ ▶* L & L ⊢ T1 ▶* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
+elim (lift_total T d e) #U #HTU
+elim (ldrop_lpss_trans … HLK1 … HK1) -HLK1 -HK1 #L2 #HL12 #HL2K
+lapply (cpss_lift … HT1 … HL2K … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+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/substitution/ldrop_lpx_sn.ma".
+include "basic_2/unfold/cpss_lift.ma".
+include "basic_2/unfold/lpss.ma".
+
+(* SN PARALLEL UNFOLD FOR LOCAL ENVIRONMENTS ********************************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lpss_ldrop_conf: dropable_sn lpss.
+/3 width=5 by lpx_sn_deliftable_dropable, cpss_inv_lift1/ qed-.
+
+lemma ldrop_lpss_trans: dedropable_sn lpss.
+/3 width=9 by lpx_sn_liftable_dedropable, cpss_lift/ qed-.
+
+lemma lpss_ldrop_trans_O1: dropable_dx lpss.
+/2 width=3 by lpx_sn_dropable/ 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/unfold/lpss_cpss.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Main properties **********************************************************)
+
+theorem lpss_conf: confluent … lpss.
+/3 width=6 by lpx_sn_conf, cpss_conf_lpss/
+qed-.
+
+theorem lpss_trans: Transitive … lpss.
+/3 width=5 by lpx_sn_trans, cpss_trans_lpss/
+qed-.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpss_fwd_shift1: ∀L1,L,T1,T. L ⊢ L1 @@ T1 ▶* T →
+ ∃∃L2,T2. L @@ L1 ⊢ ▶* L @@ L2 & L @@ L1 ⊢ T1 ▶* T2 &
+ T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #HT1
+ @ex3_2_intro [3: // |4,5: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T >shift_append_assoc #H <append_assoc
+ elim (cpss_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IH … HT12) -IH -HT12 #L2 #T #HL12 #HT1 #H destruct
+ lapply (lpss_trans … HL12 (L.ⓑ{I}V2@@L2) ?) -HL12 /3 width=1/ #HL12
+ @(ex3_2_intro … (⋆.ⓑ{I}V2@@L2)) [4: /2 width=3/ | skip ] <append_assoc // (**) (* explicit constructor *)
+]
+qed-.
]
(*
class "wine"
- [ { "examples" * } {
- [ { "" * } {
- [ "" * ]
- }
- ]
- }
- ]
- class "magenta"
[ { "higher order dynamic typing" * } {
[ { "higher order native type assignment" * } {
[ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
}
]
*)
- class "prune"
+ class "magenta"
[ { "dynamic typing" * } {
(*
[ { "local env. ref. for native type assignment" * } {
]
}
]
- class "blue"
+ class "prune"
[ { "equivalence" * } {
[ { "focalized equivalence" * } {
[ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_fpcs" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
]
}
]
- class "sky"
+ class "blue"
[ { "conversion" * } {
[ { "focalized conversion" * } {
[ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
]
}
]
- class "cyan"
+ class "sky"
[ { "computation" * } {
[ { "focalized computation" * } {
[ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ]
]
}
]
- class "water"
+ class "cyan"
[ { "reducibility" * } {
[ { "context-sensitive focalized reduction" * } {
[ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
]
}
]
+ class "water"
+ [ { "restricted computation" * } {
+ [ { "restricted parallel computation" * } {
+ [ "lpqs ( ? ⊢ ➤* ? )" "lpqs_ldrop" + "lpqs_cpqs" + "lpqs_lpqs" * ]
+ [ "cpqs ( ? ⊢ ? ➤* ? )" "cpqs_lift" * ]
+ }
+ ]
+ }
+ ]
class "green"
[ { "unwind" * } {
[ { "iterated stratified static type assignment" * } {
[ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ]
}
]
- [ { "revised parallel substitution" * } {
- [ "lcpss ( ? ⊢ ▶* ? )" "lcpss_ldrop" + "lcpss_cpss" + "lcpss_lcpss" * ]
+ [ { "revised parallel substitution" * } {
+ [ "lpss ( ? ⊢ ▶* ? )" "lpss_ldrop" + "lpss_cpss" + "lpss_lpss" * ]
[ "cpss ( ? ⊢ ? ▶* ? )" "cpss_lift" * ]
}
]
- [ { "partial unfold" * } {
+ [ { "partial unfold" * } {
[ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ]
[ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ]
[ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
}
]
[ { "basic local env. slicing" * } {
- [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_lbotr" + "ldrop_ldrop" * ]
+ [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_lpx_sn" + "ldrop_lbotr" + "ldrop_ldrop" * ]
}
]
[ { "local env. ref. for substitution" * } {
]
[ { "internal syntax" * } {
[ "genv" * ]
- [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_bi" * ]
+ [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_sn" + "lenv_px_bi" * ]
[ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
[ "item" * ]
}
projects / helm.git / commitdiff