+++ /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/cofrees_lift.ma".
-include "basic_2/substitution/llpx_sn_alt1.ma".
-
-(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
-
-(* alternative definition of llpx_sn (not recursive) *)
-definition llpx_sn_alt2: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝
- λR,d,T,L1,L2. |L1| = |L2| ∧
- (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
- ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
- I1 = I2 ∧ R I1 K1 V1 V2
- ).
-
-(* Main properties **********************************************************)
-
-lemma cpy_inv_nlift2_be: ∀G,L,U1,U2,d. ⦃G, L⦄ ⊢ U1 ▶[d, ∞] U2 → ∀i. d ≤ yinj i →
- ∀K,s. ⇩[s, i, 1] L ≡ K →
- (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥).
-#G #L #U1 #U2 #d #HU12 #i #Hdi #K #s #HLK #HnU2 #T1 #HTU1
-elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=2 by/
-qed-.
-
-lemma cpy_inv_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 →
- ∀i. d ≤ yinj i → (* yinj i + yinj 1 ≤ d + e → *)
- (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) →
- ∃∃j. d ≤ yinj j & j ≤ i & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥).
-#G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e
-[ #I #G #L #d #e #i #Hdi (* #Hide *) #H @(ex3_intro … i) /2 width=2 by/
-| #I #G #L #K #V #W #j #d #e #Hdj #Hjde #HLK #HVW #i #Hdi (* #Hide *) #HnW
- elim (le_or_ge i j) #Hij [2: @(ex3_intro … j) /2 width=7 by lift_inv_lref2_be/ ]
- elim (lift_split … HVW i j) -HVW //
- #X #_ #H elim HnW -HnW //
-| #a #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_bind … H) -H
- [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
- #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=9 by nlift_bind_sn/
- | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
- #j #Hdj #Hji
- >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
- #HnW1 @(ex3_intro … (j-1)) /3 width=9 by nlift_bind_dx, yle_pred, monotonic_pred/
- ]
-| #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_flat … H) -H
- [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
- #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_sn/
- | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 //
- #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_dx/
- ]
-]
-qed-.
-
-axiom frees_fwd_nlift_ge: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → d ≤ yinj i →
- ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥).
-
-(*
-lemma frees_ind_nlift: ∀L,d. ∀R:relation2 term nat.
- (∀U1,i. d ≤ yinj i → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1 i) →
- (∀U1,U2,i,j. d ≤ yinj j → j ≤ i → ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → R U2 i → R U1 j) →
- ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i.
-#L #d #R #IH1 #IH2 #U1 #i #Hdi #H @(frees_ind … H) -U1 /3 width=4 by/
-#U1 #U2 #HU12 #HnU2 #HU2 @(IH2 … HU12 … HU2)
-
-qed-.
-*)(*
-lemma frees_fwd_nlift: ∀L,d. ∀R:relation2 term nat. (
- ∀U1,j. (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥) ∨
- (∃∃U2,i. d ≤ yinj j → j < i & (L ⊢ j ~ϵ 𝐅*[d]⦃U1⦄ → ⊥) & ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 & R U1 i
- ) →
- d ≤ yinj j → R U1 j
- ) →
- ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i.
-#L #d #R #IHR #U1 #j #Hdj #H elim (frees_inv_gen … H) -H
-#U2 #H generalize in match Hdj; -Hdj generalize in match j; -j @(cpys_ind … H) -U2
-[ #j #Hdj #HnU1 @IHR -IHR /3 width=2 by or_introl/
-| #U0 #U2 #HU10 #HU02 #IHU10 #j #Hdj #HnU2 elim (cpy_inv_nlift2_ge … HU02 … Hdj HnU2) -HU02 -HnU2
- #i #Hdi #Hij #HnU0 lapply (IHU10 … HnU0) // -IHU10
- #Hi @IHR -IHR // -Hdj @or_intror
-
-lemma frees_fwd_nlift: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
- ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥).
-#L #U1 #d #i #Hdi #H
-#U2 #H #HnU2 @(cpys_ind_dx … H) -U1 [ @(ex3_intro … i) /2 width=2 by/ ] -Hdi -HnU2
-#U1 #U0 #HU10 #_ * #j #Hdj #Hji #HnU0 elim (cpy_inv_nlift2_ge … HU10 … Hdj HnU0) -U0 -Hdj
-/3 width=5 by transitive_le, ex3_intro/
-qed-.
-*)
-
-theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2.
-#R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H
-#HL12 #IH @conj // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
-elim (frees_fwd_nlift_ge … H Hdi) -H -Hdi #j #Hdj #Hji #HnU1
-lapply (ldrop_fwd_length_lt2 … HLK1) #HL1
-lapply (ldrop_fwd_length_lt2 … HLK2) #HL2
-lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1
-lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2
-elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1
-elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2
-
-
-
-
-generalize in match V2; -V2 generalize in match V1; -V1
-generalize in match K2; -K2 generalize in match K1; -K1
-generalize in match I2; -I2 generalize in match I1; -I1
-generalize in match IH; -IH
-@(frees_ind_nlift … Hdi H) -U1 -i
-[ #U1 #i #Hdi #HnU1 #IH #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2 elim (IH … HnU1 HLK1 HLK2) -IH -HnU1 -HLK1 -HLK2 /2 width=1 by conj/
-| #U1 #U2 #i #j #Hdj #Hji #HU12 #HnU2 #IHU12 #IH #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
-(*
-*)
- @(IHU12) … HLK1 HLK2)
-
- @(IHU12 … HLK1 HLK2) -IHU02 -I1 -I2 -K1 -K2 -V1 -V2
- #I1 #I2 #K1 #K2 #V1 #V2 #j #Hdj #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH -HLK1 -HLK2 //
-
-
-
- elim (frees_fwd_nlift … HnU1) // -HnU1 -Hdi
-#j #Hdj #Hji #HnU1
-lapply (ldrop_fwd_length_lt2 … HLK1) #HL1
-lapply (ldrop_fwd_length_lt2 … HLK2) #HL2
-lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1
-lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2
-elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1
-elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2
-elim (IH … HnU1 HLY1 HLY2) // #H #HX12 #HY12 destruct
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2.
-#R #L1 #L2 #U1 #d #H @(llpx_sn_ind_alt1 … H) -L1 -L2 -U1 -d
-#L1 #L2 #U1 #d #HL12 #IH @conj // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
-#U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
-[ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
-| #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
- #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
- @(cpy_inv_nlift2_be … HU10) /2 width=3 by/
-
-theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T2,d. llpx_sn R d T2 L1 L2 →
- ∀T1. ⦃⋆, L1⦄ ⊢ T1 ▶*[d, ∞] T2 → llpx_sn_alt2 R d T1 L1 L2.
-#R #L1 #L2 #U2 #d #H elim (llpx_sn_inv_alt1 … H) -H
-#HL12 #IH #U1 #HU12 @conj // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
-#U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
-[ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
-| #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
- #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
- @(cpy_inv_nlift2_be … HU10) /2 width=3 by/
-
-
-theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2.
-#R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H
-#HL12 #IH @conj // -HL12
-#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
-#U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
-[ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
-| #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
- #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
- @(cpy_inv_nlift2_be … HU10) /2 width=3 by/
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/lift_neg.ma".
+include "basic_2/relocation/lift_lift.ma".
+include "basic_2/relocation/cpy.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
+
+(* Inversion lemmas on negated relocation ***********************************)
+
+lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 →
+ ∀i. d ≤ yinj i → (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) →
+ (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) ∨
+ ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W &
+ (∀V. ⇧[i-j-1, 1] V ≡ W → ⊥) & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥).
+#G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e
+[ /3 width=2 by or_introl/
+| #I #G #L #K #V #W #j #d #e #Hdj #Hjde #HLK #HVW #i #Hdi #HnW
+ elim (lt_or_ge j i) #Hij
+ [ @or_intror @(ex5_4_intro … HLK) // -HLK
+ [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V //
+ #Y #HXY >minus_plus <plus_minus_m_m /2 width=2 by/
+ | -HnW /2 width=7 by lift_inv_lref2_be/
+ ]
+ | elim (lift_split … HVW i j) -HVW //
+ #X #_ #H elim HnW -HnW //
+ ]
+| #a #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_bind … H) -H
+ [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
+ [ /4 width=9 by nlift_bind_sn, or_introl/
+ | * /5 width=9 by nlift_bind_sn, ex5_4_intro, or_intror/
+ ]
+ | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
+ [ /4 width=9 by nlift_bind_dx, or_introl/
+ | * #J #K #W #j #Hdj #Hji #HLK #HnW
+ elim (yle_inv_succ1 … Hdj) -Hdj #Hdj #Hj
+ lapply (ylt_O … Hj) -Hj #Hj
+ lapply (ldrop_inv_drop1_lt … HLK ?) // -HLK #HLK
+ >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
+ #HnU1 <minus_le_minus_minus_comm in HnW;
+ /5 width=9 by nlift_bind_dx, monotonic_lt_pred, lt_plus_to_minus_r, ex5_4_intro, or_intror/
+ ]
+ ]
+| #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_flat … H) -H
+ [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
+ [ /4 width=9 by nlift_flat_sn, or_introl/
+ | * /5 width=9 by nlift_flat_sn, ex5_4_intro, or_intror/
+ ]
+ | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 //
+ [ /4 width=9 by nlift_flat_dx, or_introl/
+ | * /5 width=9 by nlift_flat_dx, ex5_4_intro, or_intror/
+ ]
+]
+qed-.
]
qed-.
-lemma ldrop_fwd_rfw: â\88\80I,L,K,V,i. â\87©[i] L â\89¡ K.â\93\91{I}V â\86\92 â\99¯{K, V} < â\99¯{L, #i}.
+lemma ldrop_fwd_rfw: â\88\80I,L,K,V,i. â\87©[i] L â\89¡ K.â\93\91{I}V â\86\92 â\88\80T. â\99¯{K, V} < â\99¯{L, T}.
#I #L #K #V #i #HLK lapply (ldrop_fwd_lw … HLK) -HLK
-normalize in ⊢ (%→?%%); /2 width=1 by le_S_S/
+normalize in ⊢ (%→?→?%%); /3 width=3 by le_to_lt_to_lt/
qed-.
(* Advanced inversion lemmas ************************************************)
(* Inversion lemmas on negated basic relocation *****************************)
+lemma nlift_inv_lref_be_SO: ∀i,j. (∀X. ⇧[i, 1] X ≡ #j → ⊥) → j = i.
+#i #j elim (lt_or_eq_or_gt i j) // #Hij #H
+[ elim (H (#(j-1))) -H /2 width=1 by lift_lref_ge_minus/
+| elim (H (#j)) -H /2 width=1 by lift_lref_lt/
+]
+qed-.
+
lemma nlift_inv_bind: ∀a,I,W,U,d,e. (∀X. ⇧[d, e] X ≡ ⓑ{a,I}W.U → ⊥) →
(∀V. ⇧[d, e] V ≡ W → ⊥) ∨ (∀T. ⇧[d+1, e] T ≡ U → ⊥).
#a #I #W #U #d #e #H elim (is_lift_dec W d e)
"context-sensitive exclusion from free variables (term)"
'CoFreeStar L i d T = (cofrees d i L T).
+(* Basic forward lemmas *****************************************************)
+
+lemma cofrees_fwd_lift: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
+/2 width=1 by/ qed-.
+
+lemma cofrees_fwd_nlift: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
+#L #U #d #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/
+qed-.
+
+lemma cofrees_fwd_bind_sn: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
+#a #I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓑ{a,I}W2.U)) /2 width=1 by cpys_bind/ -W1
+#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_bind_dx: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
+ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
+#a #I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓑ{a,I}W.U2)) /2 width=1 by cpys_bind/ -U1
+#X #H elim (lift_inv_bind2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_sn: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄.
+#I #L #W1 #U #i #d #H #W2 #HW12 elim (H (ⓕ{I}W2.U)) /2 width=1 by cpys_flat/ -W1
+#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
+lemma cofrees_fwd_flat_dx: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+#I #L #W #U1 #i #d #H #U2 #HU12 elim (H (ⓕ{I}W.U2)) /2 width=1 by cpys_flat/ -U1
+#X #H elim (lift_inv_flat2 … H) -H /2 width=2 by ex_intro/
+qed-.
+
(* Basic inversion lemmas ***************************************************)
lemma cofrees_inv_gen: ∀L,U,U0,d,i. ⦃⋆, L⦄ ⊢ U ▶*[d, ∞] U0 → (∀T. ⇧[i, 1] T ≡ U0 → ⊥) →
#X #H elim (lift_inv_lref2_be … H) -H //
qed-.
-(* Basic forward lemmas *****************************************************)
-
-lemma cofrees_fwd_lift: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∃T. ⇧[i, 1] T ≡ U.
-/2 width=1 by/ qed-.
+lemma cofrees_inv_bind: ∀a,I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓑ{a,I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L.ⓑ{I}W ⊢ i+1 ~ϵ 𝐅*[⫯d]⦃U⦄.
+/3 width=8 by cofrees_fwd_bind_sn, cofrees_fwd_bind_dx, conj/ qed-.
-lemma cofrees_fwd_nlift: ∀L,U,d,i. (∀T. ⇧[i, 1] T ≡ U → ⊥) → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
-#L #U #d #i #HnTU #H elim (cofrees_fwd_lift … H) -H /2 width=2 by/
-qed-.
+lemma cofrees_inv_flat: ∀I,L,W,U,i,d. L ⊢ i ~ϵ 𝐅*[d]⦃ⓕ{I}W.U⦄ →
+ L ⊢ i ~ϵ 𝐅*[d]⦃W⦄ ∧ L ⊢ i ~ϵ 𝐅*[d]⦃U⦄.
+/3 width=7 by cofrees_fwd_flat_sn, cofrees_fwd_flat_dx, conj/ qed-.
(* Basic Properties *********************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/cpy_nlift.ma".
+include "basic_2/substitution/cofrees_lift.ma".
+
+(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+
+(* Alternative definition of frees_ge ***************************************)
+
+lemma frees_inv_ge: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
+ (∀T. ⇧[i, 1] T ≡ U → ⊥) ∨
+ ∃∃I,K,W,j. d ≤ yinj j & j < i & ⇩[j]L ≡ K.ⓑ{I}W &
+ (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) & (∀T. ⇧[j, 1] T ≡ U → ⊥).
+#L #U #d #i #Hdi #H @(frees_ind … H) -U /3 width=2 by or_introl/
+#U1 #U2 #HU12 #HU2 *
+[ #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /3 width=2 by or_introl/
+ * /5 width=9 by cofrees_fwd_nlift, ex5_4_intro, or_intror/
+| * #I2 #K2 #W2 #j2 #Hdj2 #Hj2i #HLK2 #HnW2 #HnU2 elim (cpy_fwd_nlift2_ge … HU12 … HnU2) -HU12 -HnU2 /4 width=9 by ex5_4_intro, or_intror/
+ * #I1 #K1 #W1 #j1 #Hdj1 #Hj12 #HLK1 #HnW1 #HnU1
+ lapply (ldrop_conf_ge … HLK1 … HLK2 ?) -HLK2 /2 width=1 by lt_to_le/
+ #HK12 lapply (ldrop_inv_drop1_lt … HK12 ?) /2 width=1 by lt_plus_to_minus_r/ -HK12
+ #HK12
+ @or_intror @(ex5_4_intro … HLK1 … HnU1) -HLK1 -HnU1 /2 width=3 by transitive_lt/
+ @(frees_be … HK12 … HnW1) /2 width=1 by arith_k_sn/ -HK12 -HnW1
+ >minus_plus in ⊢ (??(?(?%?)?)??→?); >minus_plus in ⊢ (??(?(??%)?)??→?); >arith_b1 /2 width=1 by/
+]
+qed-.
+
+lemma frees_ind_ge: ∀R:relation4 ynat nat lenv term.
+ (∀d,i,L,U. d ≤ yinj i → (∀T. ⇧[i, 1] T ≡ U → ⊥) → R d i L U) →
+ (∀d,i,j,I,L,K,W,U. d ≤ yinj j → j < i → ⇩[j]L ≡ K.ⓑ{I}W → (K ⊢ i-j-1 ~ϵ 𝐅*[0]⦃W⦄ → ⊥) → (∀T. ⇧[j, 1] T ≡ U → ⊥) → R 0 (i-j-1) K W → R d i L U) →
+ ∀d,i,L,U. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R d i L U.
+#R #IH1 #IH2 #d #i #L #U
+generalize in match d; -d generalize in match i; -i
+@(f2_ind … rfw … L U) -L -U
+#n #IHn #L #U #Hn #i #d #Hdi #H elim (frees_inv_ge … H) -H /3 width=2 by/
+-IH1 * #I #K #W #j #Hdj #Hji #HLK #HnW #HnU destruct /4 width=12 by ldrop_fwd_rfw/
+qed-.
(* CONTEXT-SENSITIVE EXCLUSION FROM FREE VARIABLES **************************)
+(* Advanced inversion lemmas ************************************************)
+
+lemma cofrees_inv_lref_be: ∀L,d,i,j. L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄ → d ≤ yinj j → j < i →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #d #i #j #Hj #Hdj #Hji #I #K #W1 #HLK #W2 #HW12 elim (lift_total W2 0 (j+1))
+#X2 #HWX2 elim (Hj X2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
+#Z2 #HZX2 elim (lift_div_le … HWX2 (i-j-1) 1 Z2) -HWX2 /2 width=2 by ex_intro/
+>minus_plus <plus_minus_m_m //
+qed-.
+
+lemma cofrees_inv_be: ∀L,U,d,i. L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ∀j. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ ∀I,K,W. ⇩[j]L ≡ K.ⓑ{I}W → d ≤ yinj j → j < i → K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄.
+#L #U @(f2_ind … rfw … L U) -L -U
+#n #IH #L * *
+[ -IH #k #_ #d #i #_ #j #H elim (H (⋆k)) -H //
+| -IH #j #_ #d #i #Hi0 #j0 #H <(nlift_inv_lref_be_SO … H) -j0
+ /2 width=9 by cofrees_inv_lref_be/
+| -IH #p #_ #d #i #_ #j #H elim (H (§p)) -H //
+| #a #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
+ elim (cofrees_inv_bind … H1) -H1 #HW #HU
+ elim (nlift_inv_bind … H2) -H2 [ -HU /3 width=9 by/ ]
+ -HW #HnU lapply (IH … HU … HnU I K V ? ? ?)
+ /2 width=1 by ldrop_drop, yle_succ, lt_minus_to_plus/ -a -I -J -L -W -U -d
+ >minus_plus_plus_l //
+| #J #W #U #Hn #d #i #H1 #j #H2 #I #K #V #HLK #Hdj #Hji destruct
+ elim (cofrees_inv_flat … H1) -H1 #HW #HU
+ elim (nlift_inv_flat … H2) -H2 [ /3 width=9 by/ ]
+ #HnU @(IH … HU … HnU … HLK) // (**) (* full auto fails *)
+]
+qed-.
+
(* Advanced properties ******************************************************)
lemma cofrees_lref_skip: ∀L,d,i,j. j < i → yinj j < d → L ⊢ i ~ϵ 𝐅*[d]⦃#j⦄.
[ -n #Hij elim H -H /2 width=5 by cofrees_lref_lt/
| -H -n #H destruct /3 width=7 by lift_inv_lref2_be, ex2_intro/
| #Hji elim (frees_inv_lref_gt … H) // -H
- #I #K #W1 #HLK #H #Hdj elim (IH … H) /2 width=2 by ldrop_fwd_rfw/ -H -n
+ #I #K #W1 #HLK #H #Hdj elim (IH … H) /2 width=3 by ldrop_fwd_rfw/ -H -n
#W2 #HW12 #HnW2 elim (lift_total W2 0 (j+1))
#U2 #HWU2 @(ex2_intro … U2) /2 width=7 by cpys_subst_Y2/ -I -L -K -W1 -d
#T2 #HTU2 elim (lift_div_le … HWU2 (i-j-1) 1 T2) /2 width=2 by/ -W2
#L #d #i #R #IH1 #IH2 #U1 #H elim (frees_inv_gen … H) -H
#U2 #H #HnU2 @(cpys_ind_dx … H) -U1 /4 width=8 by cofrees_inv_gen/
qed-.
+
+(* Advanced negated properties **********************************************)
+
+lemma frees_be: ∀I,L,K,W,j. ⇩[j]L ≡ K.ⓑ{I}W →
+ ∀i. j < i → (K ⊢ i-j-1 ~ϵ 𝐅*[yinj 0]⦃W⦄ → ⊥) →
+ ∀U. (∀T. ⇧[j, 1] T ≡ U → ⊥) →
+ ∀d. d ≤ yinj j → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥).
+/4 width=11 by cofrees_inv_be/ 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/cofrees_alt.ma".
+include "basic_2/substitution/llpx_sn_alt1.ma".
+
+(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+
+(* alternative definition of llpx_sn (not recursive) *)
+definition llpx_sn_alt2: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝
+ λR,d,T,L1,L2. |L1| = |L2| ∧
+ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
+ ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
+ I1 = I2 ∧ R I1 K1 V1 V2
+ ).
+
+(* Main properties **********************************************************)
+
+theorem llpx_sn_llpx_sn_alt2: ∀R,T,L1,L2,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2.
+#R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U
+#n #IHn #L1 #U #Hn #L2 #d #H elim (llpx_sn_inv_alt1 … H) -H
+#HL12 #IHU @conj //
+#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 elim (frees_inv_ge … H) -H //
+[ -n #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/
+| * #J1 #K10 #W10 #j #Hdj #Hji #HLK10 #HnW10 #HnU destruct
+ lapply (ldrop_fwd_drop2 … HLK10) #H
+ lapply (ldrop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK10
+ elim (ldrop_O1_lt (Ⓕ) L2 j) [2: <HL12 /2 width=5 by ldrop_fwd_length_lt2/ ] #J2 #K20 #W20 #HLK20
+ lapply (ldrop_fwd_drop2 … HLK20) #H
+ lapply (ldrop_conf_ge … H … HLK2 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK20
+ elim (IHn K10 W10 … K20 0) /3 width=6 by ldrop_fwd_rfw/ -IHn
+ elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 //
+]
+qed.
[ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
}
]
+ [ { "lazy pointwise extension of a relation" * } {
+ [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt2" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ]
+ }
+ ]
+ [ { "pointwise union for local environments" * } {
+ [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
+ }
+ ]
[ { "context-sensitive exclusion from free variables" * } {
- [ "cofrees ( ? ⊢ ? ~ϵ 𝐅*[?]⦃?⦄ )" "cofrees_lift" * ]
+ [ "cofrees ( ? ⊢ ? ~ϵ 𝐅*[?]⦃?⦄ )" "cofrees_alt" + "cofrees_lift" * ]
}
]
[ { "contxt-sensitive extended multiple substitution" * } {
}
]
[ { "global env. slicing" * } {
- [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ]
- }
- ]
- [ { "pointwise union for local environments" * } {
- [ "llor ( ? ⩖[?] ? ≡ ? )" * ]
- }
- ]
- [ { "pointwise extension of a relation" * } {
- [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ]
- [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_ldrop" + "lpx_sn_lpx_sn" * ]
+ [ "gget ( ⇩[?] ? ≡ ? )" "gget_gget" * ]
}
]
[ { "contxt-sensitive extended ordinary substitution" * } {
- [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_cpy" * ]
+ [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ]
}
]
[ { "local env. ref. for extended substitution" * } {
[ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
}
]
+ [ { "pointwise extension of a relation" * } {
+ [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_ldrop" + "lpx_sn_lpx_sn" * ]
+ }
+ ]
[ { "basic local env. slicing" * } {
[ "ldrop ( ⇩[?,?,?] ? ≡ ? )" "ldrop_leq" + "ldrop_ldrop" * ]
}
--- /dev/null
+lemma eq_repl4: ∀A,B,C,D.∀R:relation4 A B C D.
+∀x1,x2:A.∀y1,y2:B. ∀z1,z2:C. ∀w1,w2:D. x1=x2 → y1=y2 → z1=z2 → w1=w2 → R x2 y2 z2 w2 → R x1 y1 z1 w1.
+// qed-.
projects / helm.git / commitdiff