STT_$(1) := $(1).stats
STTS += $$(STT_$(1))
- $$(STT_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt)
+ $$(STT_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt)
$$(STT_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt)
$$(STT_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l)
$$(STT_$(1)): P1 = $$(shell grep "^theorem " $$(MAS_$(1)) | wc -l)
SUM_$(1) := $(1)/web/$(1)_sum.tbl
SUMS += $$(SUM_$(1))
- $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt)
+ $$(SUM_$(1)): S0 = $$(shell cat $(1)/$(1)_probe.txt)
$$(SUM_$(1)): S1 = $$(shell cat $(1)/$(1)_mac.txt)
- $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l)
+ $$(SUM_$(1)): S4 = $$(shell ls $$(MAS_$(1)) | wc -l)
$$(SUM_$(1)): C1 = $$(shell grep "^inductive \|^record " $$(MAS_$(1)) | wc -l)
$$(SUM_$(1)): C2 = $$(shell grep "^definition \|^let rec " $$(MAS_$(1)) | wc -l)
$$(SUM_$(1)): C3 = $$(shell grep "^inductive \|^record \|^definition \|^let rec " $$(MAS_$(1)) | wc -l)
"context-sensitive free variables (term)"
'FreeStar L i d U = (frees d L U i).
+definition frees_trans: predicate (relation3 lenv term term) ≝
+ λR. ∀L,U1,U2,i. R L U1 U2 → L ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L ⊢ i ϵ 𝐅*[0]⦃U1⦄.
+
(* Basic inversion lemmas ***************************************************)
lemma frees_inv: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
--- /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_leq.ma".
+include "basic_2/multiple/frees.ma".
+
+(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
+
+(* Properties on equivalence for local environments *************************)
+
+lemma leq_frees_trans: ∀L2,U,d,i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ ∀L1. L1 ≃[d, ∞] L2 → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+#L2 #U #d #i #H elim H -L2 -U -d -i /3 width=2 by frees_eq/
+#I2 #L2 #K2 #U #W2 #d #i #j #Hdj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12
+elim (leq_ldrop_trans_be … HL12 … HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1
+lapply (leq_inv_O_Y … HK12) -HK12 #H destruct /3 width=9 by frees_be/
+qed-.
+
+lemma frees_leq_conf: ∀L1,U,d,i. L1 ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ ∀L2. L1 ≃[d, ∞] L2 → L2 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+/3 width=3 by leq_sym, leq_frees_trans/ qed-.
#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
qed.
+
+(* Properties on relocation *************************************************)
+
+lemma frees_lift_ge: ∀K,T,d,i. K ⊢ i ϵ𝐅*[d]⦃T⦄ →
+ ∀L,s,d0,e0. ⇩[s, d0, e0] L ≡ K →
+ ∀U. ⇧[d0, e0] T ≡ U → d0 ≤ i →
+ L ⊢ i+e0 ϵ 𝐅*[d]⦃U⦄.
+#K #T #d #i #H elim H -K -T -d -i
+[ #K #T #d #i #HnT #L #s #d0 #e0 #_ #U #HTU #Hd0i -K -s
+ @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
+| #I #K #K0 #T #V #d #i #j #Hdj #Hji #HnT #HK0 #HV #IHV #L #s #d0 #e0 #HLK #U #HTU #Hd0i
+ elim (lt_or_ge j d0) #H1
+ [ elim (ldrop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 #HLK0 #HVW
+ @(frees_be … HL0) -HL0 -HV
+ /3 width=3 by lt_plus_to_minus_r, lt_to_le_to_lt/
+ [ #X #HXU >(plus_minus_m_m d0 1) in HTU; /2 width=2 by ltn_to_ltO/ #HTU
+ elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by monotonic_pred/
+ | >minus_plus <plus_minus // <minus_plus
+ /3 width=5 by monotonic_le_minus_l2/
+ ]
+ | lapply (ldrop_trans_ge … HLK … HK0 ?) // -K #HLK0
+ lapply (ldrop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
+ @(frees_be … HLK0) -HLK0 -IHV
+ /2 width=1 by yle_plus_dx1_trans, lt_minus_to_plus/
+ #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
+ ]
+]
+qed.
+
+(* Inversion lemmas on relocation *******************************************)
+
+lemma frees_inv_lift_be: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ ∀K,s,d0,e0. ⇩[s, d0, e0+1] L ≡ K →
+ ∀T. ⇧[d0, e0+1] T ≡ U → d0 ≤ i → i ≤ d0 + e0 → ⊥.
+#L #U #d #i #H elim H -L -U -d -i
+[ #L #U #d #i #HnU #K #s #d0 #e0 #_ #T #HTU #Hd0i #Hide0
+ elim (lift_split … HTU i e0) -HTU /2 width=2 by/
+| #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hd0i #Hide0
+ elim (lt_or_ge j d0) #H1
+ [ elim (ldrop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+ @(IHW … HKL0 … HVW)
+ [ /2 width=1 by monotonic_le_minus_l2/
+ | >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
+ ]
+ | elim (lift_split … HTU j e0) -HTU /3 width=3 by lt_to_le_to_lt, lt_to_le/
+ ]
+]
+qed-.
+
+lemma frees_inv_lift_ge: ∀L,U,d,i. L ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ ∀K,s,d0,e0. ⇩[s, d0, e0] L ≡ K →
+ ∀T. ⇧[d0, e0] T ≡ U → d0 + e0 ≤ i →
+ K ⊢ i-e0 ϵ𝐅*[d-yinj e0]⦃T⦄.
+#L #U #d #i #H elim H -L -U -d -i
+[ #L #U #d #i #HnU #K #s #d0 #e0 #HLK #T #HTU #Hde0i -L -s
+ elim (le_inv_plus_l … Hde0i) -Hde0i #Hd0ie0 #He0i @frees_eq #X #HXT -K
+ elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
+| #I #L #K0 #U #W #d #i #j #Hdi #Hij #HnU #HLK0 #_ #IHW #K #s #d0 #e0 #HLK #T #HTU #Hde0i
+ elim (lt_or_ge j d0) #H1
+ [ elim (ldrop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
+ elim (le_inv_plus_l … Hde0i) #H0 #He0i
+ @(frees_be … H) -H
+ [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
+ | /2 width=3 by lt_to_le_to_lt/
+ | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by/
+ | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
+ >minus_plus >minus_plus >plus_minus /2 width=1 by monotonic_le_minus_l/
+ ]
+ | elim (lt_or_ge j (d0+e0)) [ >commutative_plus |] #H2
+ [ -L -I -W lapply (lt_plus_to_minus ???? H2) // -H2 #H2
+ elim (lift_split … HTU j (e0-1)) -HTU //
+ [ >minus_minus_associative /2 width=2 by ltn_to_ltO/ <minus_n_n
+ #X #_ #H elim (HnU … H)
+ | >commutative_plus /3 width=1 by le_minus_to_plus, monotonic_pred/
+ ]
+ | lapply (ldrop_conf_ge … HLK … HLK0 ?) // -L #HK0
+ elim (le_inv_plus_l … H2) -H2 #H2 #He0j
+ @(frees_be … HK0)
+ [ /2 width=1 by monotonic_yle_minus_dx/
+ | /2 width=1 by monotonic_lt_minus_l/
+ | #X #HXT elim (lift_trans_le … HXT … HTU) -T // <plus_minus_m_m /2 width=2 by/
+ | >arith_b1 /2 width=5 by/
+ ]
+ ]
+ ]
+]
+qed-.
(**************************************************************************)
include "basic_2/multiple/llor.ma".
+include "basic_2/multiple/llpx_sn_frees.ma".
include "basic_2/multiple/lleq_alt.ma".
(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
(* Properties on poinwise union for local environments **********************)
-lemma llpx_sn_llor_dx: ∀R,L1,L2.
- (∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄) →
- ∀T. llpx_sn R 0 T L1 L2 → ∀L. L1 ⩖[T] L2 ≡ L → L2 ≡[T, 0] L.
-#R #L1 #L2 #HR #T #H1 #L #H2
+lemma llpx_sn_llor_dx: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) →
+ ∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L2 ≡[T, d] L.
+#R #H1R #H2R #L1 #L2 #T #d #H1 #L #H2
+lapply (llpx_sn_frees_trans … H1R H2R … H1) -H1R -H2R #HR
elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
elim H2 -H2 #_ #HL1 #IH2
@lleq_intro_alt // #I2 #I #K2 #K #V2 #V #i #Hi #HnT #HLK2 #HLK
elim (ldrop_O1_lt (Ⓕ) L1 i) // -HiL #I1 #K1 #V1 #HLK1
elim (IH1 … HLK1 HLK2) -IH1 /2 width=1 by/ #H #_ destruct
elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H
-elim H -H /2 width=1 by/
+[ elim (ylt_yle_false … H) -H //
+| elim H -H /2 width=1 by/
+]
qed.
+
+lemma llpx_sn_llor_dx_sym: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) →
+ ∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L ≡[T, d] L2.
+/3 width=6 by llpx_sn_llor_dx, lleq_sym/ qed.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyor_4.ma".
+include "basic_2/notation/relations/lazyor_5.ma".
include "basic_2/multiple/frees.ma".
(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************)
-definition llor: relation4 term lenv lenv lenv ≝ λT,L2,L1,L.
+definition llor: ynat → relation4 term lenv lenv lenv ≝ λd,T,L2,L1,L.
∧∧ |L1| ≤ |L2| & |L1| = |L|
& (∀I1,I2,I,K1,K2,K,V1,V2,V,i.
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V →
- (∧∧ (L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) & I1 = I & V1 = V) ∨
- (∧∧ L1 ⊢ i ϵ 𝐅*[yinj 0]⦃T⦄ & I1 = I & V2 = V)
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → ⇩[i] L ≡ K.ⓑ{I}V → ∨∨
+ (∧∧ yinj i < d & I1 = I & V1 = V) |
+ (∧∧ (L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ → ⊥) & I1 = I & V1 = V) |
+ (∧∧ d ≤ yinj i & L1 ⊢ i ϵ 𝐅*[d]⦃T⦄ & I1 = I & V2 = V)
).
interpretation
"lazy union (local environment)"
- 'LazyOr L1 T L2 L = (llor T L2 L1 L).
+ 'LazyOr L1 T d L2 L = (llor d T L2 L1 L).
(* Basic properties *********************************************************)
-lemma llor_atom: ∀T,L2. ⋆ ⩖[T] L2 ≡ ⋆.
-#T #L2 @and3_intro //
+lemma llor_atom: ∀L2,T,d. ⋆ ⩖[T, d] L2 ≡ ⋆.
+#L2 #T #d @and3_intro //
#I1 #I2 #I #K1 #K2 #K #V1 #V2 #V #i #HLK1
elim (ldrop_inv_atom1 … HLK1) -HLK1 #H destruct
qed.
(* Advanced properties ******************************************************)
-axiom llor_total: ∀L1,L2,T. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L.
+axiom llor_total: ∀L1,L2,T,d. |L1| ≤ |L2| → ∃L. L1 ⩖[T, d] L2 ≡ 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/multiple/frees.ma".
+include "basic_2/multiple/llpx_sn_alt_rec.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* Properties on context-sensitive free variables ***************************)
+
+fact llpx_sn_frees_trans_aux: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) →
+ ∀L2,U,d,i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ →
+ ∀L1. llpx_sn R d U L1 L2 → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+#R #H1R #H2R #L2 #U #d #i #H elim H -L2 -U -d -i /3 width=2 by frees_eq/
+#I2 #L2 #K2 #U #W2 #d #i #j #Hdj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12
+elim (llpx_sn_inv_alt_r … HL12) -HL12 #HL12 #IH
+lapply (ldrop_fwd_length_lt2 … HLK2) #Hj
+elim (ldrop_O1_lt (Ⓕ) L1 j) // -Hj -HL12 #I1 #K1 #W1 #HLK1
+elim (IH … HnU HLK1 HLK2) // -IH -HLK2 /5 width=11 by frees_be/
+qed-.
+
+lemma llpx_sn_frees_trans: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) →
+ ∀L1,L2,U,d. llpx_sn R d U L1 L2 →
+ ∀i. L2 ⊢ i ϵ 𝐅*[d]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[d]⦃U⦄.
+/2 width=6 by llpx_sn_frees_trans_aux/ qed-.
(* Inversion lemmas on poinwise union for local environments ****************)
lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) →
- ∀L1,L2,T. llpx_sn R 0 T L1 L2 →
- ∀L. L1 ⩖[T] L2 ≡ L → lpx_sn R L1 L.
-#R #HR #L1 #L2 #T #H1 #L #H2
+ ∀L1,L2,T,d. llpx_sn R d T L1 L2 →
+ ∀L. L1 ⩖[T, d] L2 ≡ L → lpx_sn R L1 L.
+#R #HR #L1 #L2 #T #d #H1 #L #H2
elim (llpx_sn_llpx_sn_alt … H1) -H1 #HL12 #IH1
elim H2 -H2 #_ #HL1 #IH2
@lpx_sn_intro_alt // #I1 #I #K1 #K #V1 #V #i #HLK1 #HLK
lapply (ldrop_fwd_length_lt2 … HLK) #HiL
elim (ldrop_O1_lt (Ⓕ) L2 i) // -HiL -HL1 -HL12 #I2 #K2 #V2 #HLK2
-elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * [ /2 width=1 by conj/ ]
+elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK * /2 width=1 by conj/
#HnT #H1 #H2 elim (IH1 … HnT … HLK1 HLK2) -IH1 -HnT -HLK1 -HLK2 /2 width=1 by conj/
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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L1 ⩖ break [ term 46 T ] break term 46 L2 ≡ break term 46 L )"
- non associative with precedence 45
- for @{ 'LazyOr $L1 $T $L2 $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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( L1 ⩖ break [ term 46 T , break term 46 d ] break term 46 L2 ≡ break term 46 L )"
+ non associative with precedence 45
+ for @{ 'LazyOr $L1 $T $d $L2 $L }.
(* *)
(**************************************************************************)
-include "basic_2/multiple/fqup.ma".
+include "basic_2/multiple/frees_leq.ma".
include "basic_2/multiple/frees_lift.ma".
include "basic_2/reduction/lpx_ldrop.ma".
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-(*
-lemma cofrees_lsuby_conf: ∀L1,U,i. L1 ⊢ i ~ϵ 𝐅*⦃U⦄ →
- ∀L2. lsuby L1 L2 → L2 ⊢ i ~ϵ 𝐅*⦃U⦄.
-/3 width=3 by lsuby_cpys_trans/ qed-.
-lemma lpx_cpx_cofrees_conf: ∀h,g,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
- ∀i. L1 ⊢ i ~ϵ 𝐅*⦃U1⦄ → L2 ⊢ i ~ϵ 𝐅*⦃U2⦄.
+(* Properties on context-sensitive free variables ***************************)
+
+lemma lpx_cpx_frees_trans: ∀h,g,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, g] U2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀i. L2 ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U1⦄.
#h #g #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1
#G0 #L0 #U0 #IH #G #L1 * *
-[ -IH #k #HG #HL #HU #U2 #H elim (cpx_inv_sort1 … H) -H
- [| * #l #_ ] #H destruct //
-| #j #HG #HL #HU #U2 #H #L2 #HL12 #i #Hi elim (cpx_inv_lref1 … H) -H
- [ #H destruct elim (lt_or_eq_or_gt i j) #Hji
- [ -IH -HL12 /2 width=4 by cofrees_lref_gt/
- | -IH -HL12 destruct elim (cofrees_inv_lref_eq … Hi)
- | elim (lt_or_ge j (|L2|)) /2 width=5 by cofrees_lref_free/ #Hj
- elim (ldrop_O1_lt (Ⓕ) L1 j) [2: >(lpx_fwd_length … HL12) // ] #I #K1 #W1 #HLK1
- elim (lpx_ldrop_conf … HLK1 … HL12) -HL12 #Y #H #HLK2
- elim (lpx_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
- lapply (cofrees_inv_lref_lt … Hi … HLK1) -Hi // #HW1
- lapply (IH … HW12 … HK12 … HW1) /2 width=2 by fqup_lref/ -L1 -K1 -W1 #HW2
- /2 width=9 by cofrees_lref_lt/ (**) (* full auto too slow *)
- ]
- | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2 elim (lt_or_ge j i) #Hji
- [ lapply (ldrop_fwd_drop2 … HLK1) #H0
- elim (lpx_ldrop_conf … H0 … HL12) #K2 #HK12 #HLK2
- @(cofrees_lift_ge … HLK2 … HW0U2) //
- @(IH … HW10) /2 width=2 by fqup_lref/ -L2 -K2 -W0 -U2 -IH
- <minus_plus /2 width=7 by cofrees_inv_lref_lt/
- | -IH lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
- elim (lpx_ldrop_conf … HLK1 … HL12) -I -L1 -W1
- /2 width=12 by cofrees_lift_be/
+[ -IH #k #HG #HL #HU #U2 #H1 #L2 #_ #i #H2 elim (cpx_inv_sort1 … H1) -H1
+ [| * #l #_ ] #H destruct elim (frees_inv_sort … H2)
+| #j #HG #HL #HU #U2 #H1 #L2 #HL12 #i #H2 elim (cpx_inv_lref1 … H1) -H1
+ [ #H destruct elim (frees_inv_lref … H2) -H2 //
+ * #I #K2 #W2 #Hj #Hji #HLK2 #HW2
+ elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -HL12 #Y #HLK1 #H
+ elim (lpx_inv_pair2 … H) -H #K1 #W1 #HK12 #HW12 #H destruct
+ /4 width=11 by frees_lref_be, fqup_lref/
+ | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2
+ lapply (ldrop_fwd_drop2 … HLK1) #H0
+ elim (lpx_ldrop_conf … H0 … HL12) -H0 -HL12 #K2 #HK12 #HLK2
+ elim (lt_or_ge i (j+1)) #Hji
+ [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by monotonic_pred/
+ | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // <minus_plus destruct
+ /4 width=11 by frees_lref_be, fqup_lref/
]
]
-| -IH #p #HG #HL #HU #U2 #H lapply (cpx_inv_gref1 … H) -H
- #H destruct //
+| -IH #p #HG #HL #HU #U2 #H1 >(cpx_inv_gref1 … H1) -H1 destruct
+ #L2 #_ #i #H2 elim (frees_inv_gref … H2)
| #a #I #W1 #U1 #HG #HL #HU #X #HX #L2 #HL12 #i #Hi destruct
- elim (cofrees_inv_bind … Hi) -Hi #HW1 #HU1
- elim (cpx_inv_bind1 … HX) -HX
- [ * #W2 #U2 #HW12 #HU12 #H destruct /4 width=8 by cofrees_bind, lpx_pair/
- |
+ elim (cpx_inv_bind1 … HX) -HX *
+ [ #W2 #U2 #HW12 #HU12 #H destruct
+ elim (frees_inv_bind_O … Hi) -Hi
+ /4 width=7 by frees_bind_dx_O, frees_bind_sn, lpx_pair/
+ | #U2 #HU12 #HXU2 #H1 #H2 destruct
+ lapply (frees_lift_ge … Hi (L2.ⓓW1) (Ⓕ) … HXU2 ?)
+ /4 width=7 by frees_bind_dx_O, lpx_pair, ldrop_drop/
]
| #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct
- elim (cofrees_inv_flat … Hi) -Hi #HW1 #HX1
elim (cpx_inv_flat1 … HX2) -HX2 *
- [ #W2 #U2 #HW12 #HU12 #H destruct /3 width=7 by cofrees_flat/
- | #HU12 #H destruct /2 width=7 by/
- | #HW12 #H destruct /2 width=7 by/
+ [ #W2 #U2 #HW12 #HU12 #H destruct
+ elim (frees_inv_flat … Hi) -Hi /3 width=7 by frees_flat_dx, frees_flat_sn/
+ | #HU12 #H destruct /3 width=7 by frees_flat_dx/
+ | #HW12 #H destruct /3 width=7 by frees_flat_sn/
| #b #W2 #V1 #V2 #U1 #U2 #HW12 #HV12 #HU12 #H1 #H2 #H3 destruct
- elim (cofrees_inv_bind … HX1) -HX1 #HV1 #HU1
- @cofrees_bind [ /3 width=7 by cofrees_flat/ ]
- @(cofrees_lsuby_conf (L2.ⓛV2)) /3 width=7 by lpx_pair, lsuby_succ/
- |
-
-
-*)
+ elim (frees_inv_bind … Hi) -Hi #Hi
+ [ elim (frees_inv_flat … Hi) -Hi
+ /4 width=7 by frees_flat_dx, frees_flat_sn, frees_bind_sn/
+ | lapply (leq_frees_trans … Hi (L2.ⓛV2) ?) /2 width=1 by leq_succ/ -Hi #HU2
+ lapply (frees_weak … HU2 0 ?) -HU2
+ /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
+ ]
+ | #b #W2 #W0 #V1 #V2 #U1 #U2 #HW12 #HW20 #HV12 #HU12 #H1 #H2 #H3 destruct
+ elim (frees_inv_bind_O … Hi) -Hi #Hi
+ [ /4 width=7 by frees_flat_dx, frees_bind_sn/
+ | elim (frees_inv_flat … Hi) -Hi
+ [ #HW0 lapply (frees_inv_lift_ge … HW0 L2 (Ⓕ) … HW20 ?) -W0
+ /3 width=7 by frees_flat_sn, ldrop_drop/
+ | /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
+ ]
+ ]
+ ]
+]
+qed-.
+
+lemma cpx_frees_trans: ∀h,g,G. frees_trans (cpx h g G).
+/2 width=8 by lpx_cpx_frees_trans/ qed-.
+
+lemma lpx_frees_trans: ∀h,g,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, g] L2 →
+ ∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄.
+/2 width=8 by lpx_cpx_frees_trans/ qed-.
(* *)
(**************************************************************************)
+include "basic_2/multiple/llor_ldrop.ma".
+include "basic_2/multiple/llpx_sn_llor.ma".
+include "basic_2/multiple/llpx_sn_lpx_sn.ma".
include "basic_2/multiple/lleq_leq.ma".
-include "basic_2/multiple/lleq_ldrop.ma".
+include "basic_2/multiple/lleq_llor.ma".
include "basic_2/reduction/cpx_leq.ma".
-include "basic_2/reduction/lpx_ldrop.ma".
+include "basic_2/reduction/cpx_lleq.ma".
+include "basic_2/reduction/lpx_frees.ma".
(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
(* Properties on lazy equivalence for local environments ********************)
-axiom lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 →
+(* Note: contains a proof of llpx_cpx_conf *)
+lemma lleq_lpx_trans: ∀h,g,G,L2,K2. ⦃G, L2⦄ ⊢ ➡[h, g] K2 →
∀L1,T,d. L1 ≡[T, d] L2 →
∃∃K1. ⦃G, L1⦄ ⊢ ➡[h, g] K1 & K1 ≡[T, d] K2.
+#h #g #G #L2 #K2 #HLK2 #L1 #T #d #HL12
+lapply (lpx_fwd_length … HLK2) #H1
+lapply (lleq_fwd_length … HL12) #H2
+lapply (lpx_sn_llpx_sn … T … d HLK2) // -HLK2 #H
+lapply (lleq_llpx_sn_trans … HL12 … H) /2 width=3 by lleq_cpx_trans/ -HL12 -H #H
+elim (llor_total L1 K2 T d) // -H1 -H2 #K1 #HLK1
+lapply (llpx_sn_llor_dx_sym … H … HLK1)
+[ /2 width=6 by cpx_frees_trans/
+| /3 width=10 by cpx_llpx_sn_conf, cpx_inv_lift1, cpx_lift/
+| /3 width=5 by llpx_sn_llor_fwd_sn, ex2_intro/
+]
+qed-.
lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ≡[T1, 0] L1 →
class "magenta"
[ { "higher order dynamic typing" * } {
[ { "higher order native type assignment" * } {
- [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]
+ [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ]basic_2/multiple/frees_leq.ma
}
]
}
]
[ { "degree assignment" * } {
[ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_da" * ]
- }
+ }basic_2/multiple/frees_leq.ma
]
[ { "parameters" * } {
[ "sh" "sd" * ]
}
]
[ { "lazy pointwise extension of a relation" * } {
- [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" + "llpx_sn_llor" * ]
+ [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ]
}
]
[ { "pointwise union for local environments" * } {
- [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_ldrop" * ]
+ [ "llor ( ? ⩖[?,?] ? ≡ ? )" "llor_ldrop" * ]
}
]
[ { "context-sensitive exclusion from free variables" * } {
- [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_lift" * ]
+ [ "frees ( ? ⊢ ? ϵ 𝐅*[?]⦃?⦄ )" "frees_leq" + "frees_lift" * ]
}
]
[ { "contxt-sensitive extended multiple substitution" * } {
[ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_ldrop" + "lpx_sn_lpx_sn" * ]
}
]
- [ { "basic local env. slicing" * } {
+ [ { "basic local env. slicing" * } {
[ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_leq" + "ldrop_ldrop" * ]
}
]
projects / helm.git / commitdiff