(**************************************************************************)
include "basic_2/relocation/lex_tc.ma".
-include "basic_2/static/lfxs_fsle.ma".
include "basic_2/static/lfeq_fqup.ma".
-include "basic_2/static/lfeq_lfeq.ma".
+include "basic_2/static/lfeq_fsle.ma".
include "basic_2/i_static/tc_lfxs_fqup.ma".
(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
(* Note: s_rs_transitive_lex_inv_isid could be invoked in the last auto but makes it too slow *)
lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
- lfxs_fsle_compatible R →
+ lfxs_fsge_compatible R →
s_rs_transitive … R (λ_.lex R) →
lfeq_transitive R →
∀L1,L2,T. L1 ⪤**[R, T] L2 →
(* Advanced properties ******************************************************)
-lemma tc_lfxs_sym: ∀R. lfxs_fsle_compatible R →
+lemma tc_lfxs_sym: ∀R. lfxs_fsge_compatible R →
(∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
∀T. symmetric … (tc_lfxs R T).
#R #H1R #H2R #T #L1 #L2 #H elim H -L2
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 lenv bind bind → relation3 lenv bind bind →
relation3 rtmap lenv bind ≝
- λR1,R2,RN1,RP1,RN2,RP2,f,L0,T0.
- ∀T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+ λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
+ ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
∀L1. L0 ⪤*[RN1, RP1, f] L1 → ∀L2. L0 ⪤*[RN2, RP2, f] L2 →
- ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
-
-definition lexs_transitive: relation5 (relation3 lenv bind bind)
- (relation3 lenv bind bind) … ≝
- λR1,R2,R3,RN,RP.
- ∀f,L1,T1,T. R1 L1 T1 T → ∀L2. L1 ⪤*[RN, RP, f] L2 →
- ∀T2. R2 L2 T T2 → R3 L1 T1 T2.
+ ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
+
+definition lexs_transitive: relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,R3,RN,RP,f,L1,I1.
+ ∀I. R1 L1 I1 I → ∀L2. L1 ⪤*[RN, RP, f] L2 →
+ ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
(* Basic inversion lemmas ***************************************************)
(* Main properties **********************************************************)
-theorem lexs_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP) (f):
- lexs_transitive RN1 RN2 RN RN1 RP1 →
- lexs_transitive RP1 RP2 RP RN1 RP1 →
- ∀L1,L0. L1 ⪤*[RN1, RP1, f] L0 →
+theorem lexs_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP):
+ ∀L1,f.
+ (∀g,I,K,n. ⬇*[n] L1 ≡ K.ⓘ{I} → ⫯g = ⫱*[n] f → lexs_transitive RN1 RN2 RN RN1 RP1 g K I) →
+ (∀g,I,K,n. ⬇*[n] L1 ≡ K.ⓘ{I} → ↑g = ⫱*[n] f → lexs_transitive RP1 RP2 RP RN1 RP1 g K I) →
+ ∀L0. L1 ⪤*[RN1, RP1, f] L0 →
∀L2. L0 ⪤*[RN2, RP2, f] L2 →
L1 ⪤*[RN, RP, f] L2.
-#RN1 #RP1 #RN2 #RP2 #RN #RP #f #HN #HP #L1 #L0 #H elim H -f -L1 -L0
-[ #f #L2 #H >(lexs_inv_atom1 … H) -L2 //
-| #f #I1 #I #K1 #K #HK1 #HI1 #IH #L2 #H elim (lexs_inv_next1 … H) -H
- #I2 #K2 #HK2 #HI2 #H destruct /4 width=6 by lexs_next/
-| #f #I1 #I #K1 #K #HK1 #HI1 #IH #L2 #H elim (lexs_inv_push1 … H) -H
- #I2 #K2 #HK2 #HI2 #H destruct /4 width=6 by lexs_push/
+#RN1 #RP1 #RN2 #RP2 #RN #RP #L1 elim L1 -L1
+[ #f #_ #_ #L0 #H1 #L2 #H2
+ lapply (lexs_inv_atom1 … H1) -H1 #H destruct
+ lapply (lexs_inv_atom1 … H2) -H2 #H destruct
+ /2 width=1 by lexs_atom/
+| #K1 #I1 #IH #f elim (pn_split f) * #g #H destruct
+ #HN #HP #L0 #H1 #L2 #H2
+ [ elim (lexs_inv_push1 … H1) -H1 #I0 #K0 #HK10 #HI10 #H destruct
+ elim (lexs_inv_push1 … H2) -H2 #I2 #K2 #HK02 #HI02 #H destruct
+ lapply (HP … 0 … HI10 … HK10 … HI02) -HI10 -HI02 /2 width=2 by drops_refl/ #HI12
+ lapply (IH … HK10 … HK02) -IH -K0 /3 width=3 by lexs_push, drops_drop/
+ | elim (lexs_inv_next1 … H1) -H1 #I0 #K0 #HK10 #HI10 #H destruct
+ elim (lexs_inv_next1 … H2) -H2 #I2 #K2 #HK02 #HI02 #H destruct
+ lapply (HN … 0 … HI10 … HK10 … HI02) -HI10 -HI02 /2 width=2 by drops_refl/ #HI12
+ lapply (IH … HK10 … HK02) -IH -K0 /3 width=3 by lexs_next, drops_drop/
+ ]
]
qed-.
(* Basic_2A1: includes: lpx_sn_trans *)
-theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RN RP →
- lexs_transitive RP RP RP RN RP →
+theorem lexs_trans (RN) (RP) (f): (∀g,I,K. lexs_transitive RN RN RN RN RP g K I) →
+ (∀g,I,K. lexs_transitive RP RP RP RN RP g K I) →
Transitive … (lexs RN RP f).
/2 width=9 by lexs_trans_gen/ qed-.
lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2.
-/3 width=5 by lfpx_fsle_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.
+/3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-.
(* v GNU General Public License Version 2 *)
(* *)
(**************************************************************************)
-
+(*
include "basic_2/rt_computation/csx_cpxs.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
+include "basic_2/rt_computation/lfsx_lpxs.ma".
+*)
include "basic_2/rt_computation/lsubsx_lfsx.ma".
(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****)
+(*
+axiom lpxs_trans: ∀h,G. Transitive … (lpxs h G).
+*)
(* Advanced properties ******************************************************)
(* Basic_2A1: uses: lsx_lref_be_lpxs *)
-lemma lfsx_pair_lfpxs: ∀h,o,G,K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
- ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h, V] K2 →
- ∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄.
+lemma lfsx_pair_lpxs: ∀h,o,G,K1,V. ⦃G, K1⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
+ ∀K2. G ⊢ ⬈*[h, o, V] 𝐒⦃K2⦄ → ⦃G, K1⦄ ⊢ ⬈*[h] K2 →
+ ∀I. G ⊢ ⬈*[h, o, #0] 𝐒⦃K2.ⓑ{I}V⦄.
#h #o #G #K1 #V #H
@(csx_ind_cpxs … H) -V #V0 #_ #IHV0 #K2 #H
-@(lfsx_ind … H) -K2 #K0 #HK0 #IHK0 #HK10 #I
-@lfsx_intro #Y #HY #HnY
-elim (lfpx_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
+@(lfsx_ind_lpxs … H) -K2 #K0 #HK0 #IHK0 #HK10 #I
+@lfsx_intro_lpxs #Y #HY #HnY
+elim (lpxs_inv_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
elim (tdeq_dec h o V0 V2) #HnV02 destruct [ -IHV0 -HV02 -HK0 | -IHK0 -HnY ]
-[ /5 width=5 by lfsx_lfdeq_trans, lfpxs_step_dx, lfdeq_pair/
-| @lfsx_lfpx_trans
- [2: @(IHV0 … HnV02 K0 … I) -IHV0 -HnV02
- [ /2 width=3 by lfpxs_cpx_trans/
- | /2 width=3 by lfsx_cpx_trans/
- |
- ]
- |1: skip
- |3: @lfpx_pair /2 width=3 by lfpx_cpx_conf/
+[ /5 width=5 by lfsx_lfdeq_trans, lpxs_trans, lfdeq_pair/
+| @(IHV0 … HnV02) -IHV0 -HnV02
+ [
+ | /3 width=3 by lfsx_lpxs_trans, lfsx_cpxs_trans/
+ | /2 width=3 by lpxs_trans/
]
-]
-qed.
+
+(*
+ @(lfsx_lpxs_trans … (K0.ⓑ{I}V2))
+ [ @(IHV0 … HnV02 … HK10) -IHV0 -HnV02
+ [
+ | /2 width=3 by lfsx_cpxs_trans/
+ ]
+ |
+ ]
+*)
(* Basic_2A1: uses: lsx_lref_be *)
lemma lfsx_lref_pair: ∀h,o,G,K,V. ⦃G, K⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃K⦄ →
(* Forward lemmas with free variables inclusion for restricted closures *****)
-lemma cpm_fsle_comp: ∀n,h,G. R_fsle_compatible (cpm n h G).
-/3 width=6 by cpm_fwd_cpx, cpx_fsle_comp/ qed-.
+lemma cpm_fsge_comp: ∀n,h,G. R_fsge_compatible (cpm n h G).
+/3 width=6 by cpm_fwd_cpx, cpx_fsge_comp/ qed-.
-lemma lfpr_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpm 0 h G).
-/4 width=5 by cpm_fwd_cpx, lfpx_fsle_comp, lfxs_co/ qed-.
+lemma lfpr_fsge_comp: ∀h,G. lfxs_fsge_compatible (cpm 0 h G).
+/4 width=5 by cpm_fwd_cpx, lfpx_fsge_comp, lfxs_co/ qed-.
(* Properties with generic extension on referred entries ********************)
(* Main properties **********************************************************)
theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T).
-/3 width=6 by cpr_conf_lfpr, lfpr_fsle_comp, lfxs_conf/ qed-.
+/3 width=6 by cpr_conf_lfpr, lfpr_fsge_comp, lfxs_conf/ qed-.
theorem lfpr_bind: ∀h,G,L1,L2,V1. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 →
∀I,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, T] L2.ⓑ{I}V2 →
(* Note: This invalidates lfpxs_cpx_conf: "∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G)" *)
(* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *)
(* Basic_2A1: uses: lpx_cpx_frees_trans *)
-lemma lfpx_cpx_conf_fsle: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
+lemma lfpx_cpx_conf_fsge: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄.
#h #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G0 L0 T0) -G0 -L0 -T0
#G #L #T #IH #G0 #L0 * *
qed.
(* Basic_2A1: uses: cpx_frees_trans *)
-lemma cpx_fsle_comp: ∀h,G. R_fsle_compatible (cpx h G).
-/2 width=4 by lfpx_cpx_conf_fsle/ qed-.
+lemma cpx_fsge_comp: ∀h,G. R_fsge_compatible (cpx h G).
+/2 width=4 by lfpx_cpx_conf_fsge/ qed-.
(* Basic_2A1: uses: lpx_frees_trans *)
-lemma lfpx_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpx h G).
-/2 width=4 by lfpx_cpx_conf_fsle/ qed-.
+lemma lfpx_fsge_comp: ∀h,G. lfxs_fsge_compatible (cpx h G).
+/2 width=4 by lfpx_cpx_conf_fsge/ qed-.
(* Properties with generic extension on referred entries ********************)
(* Note: lemma 1000 *)
(* Basic_2A1: uses: cpx_llpx_sn_conf *)
lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R).
-/3 width=3 by fsle_lfxs_trans, cpx_fsle_comp/ qed-.
+/3 width=3 by fsge_lfxs_trans, cpx_fsge_comp/ qed-.
(* Advanced properties ******************************************************)
lemma lfpx_pair_sn_split: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → ∀o,I,T.
∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L & L ≛[h, o, V] L2.
-/3 width=5 by lfpx_fsle_comp, lfxs_pair_sn_split/ qed-.
+/3 width=5 by lfpx_fsge_comp, lfxs_pair_sn_split/ qed-.
lemma lfpx_flat_dx_split: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ∀o,I,V.
∃∃L. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L & L ≛[h, o, T] L2.
-/3 width=5 by lfpx_fsle_comp, lfxs_flat_dx_split/ qed-.
+/3 width=5 by lfpx_fsge_comp, lfxs_flat_dx_split/ qed-.
lemma lfpx_bind_dx_split: ∀h,I,G,L1,L2,V1,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2 → ∀o,p.
∃∃L,V. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ≛[h, o, T] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V.
-/3 width=5 by lfpx_fsle_comp, lfxs_bind_dx_split/ qed-.
+/3 width=5 by lfpx_fsge_comp, lfxs_bind_dx_split/ qed-.
lemma lfpx_bind_dx_split_void: ∀h,G,K1,L2,T. ⦃G, K1.ⓧ⦄ ⊢ ⬈[h, T] L2 → ∀o,p,I,V.
∃∃K2. ⦃G, K1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] K2 & K2.ⓧ ≛[h, o, T] L2.
-/3 width=5 by lfpx_fsle_comp, lfxs_bind_dx_split_void/ qed-.
+/3 width=5 by lfpx_fsge_comp, lfxs_bind_dx_split_void/ qed-.
lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) (cpx h G) (cdeq h o).
#h #o #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/
qed-.
lemma lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T).
-/3 width=6 by lfpx_fsle_comp, lfdeq_fsle_comp, cpx_tdeq_conf_lexs, lfxs_conf/ qed-.
+/3 width=6 by lfpx_fsge_comp, lfdeq_fsge_comp, cpx_tdeq_conf_lexs, lfxs_conf/ qed-.
(* Basic_2A1: uses: lleq_lpx_trans *)
lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 →
/2 width=3 by ex2_intro/
qed-.
+lemma fsle_inv_frees_eq: ∀L1,L2. |L1| = |L2| →
+ ∀T1,T2. ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄ →
+ ∀f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 →
+ f1 ⊆ f2.
+#L1 #L2 #H1L #T1 #T2 #H2L #f1 #Hf1 #f2 #Hf2
+elim (fsle_frees_trans_eq … H2L … Hf2) // -L2 -T2
+/3 width=6 by frees_mono, sle_eq_repl_back1/
+qed-.
+
(* Main properties **********************************************************)
theorem fsle_trans_sn: ∀L1,L2,T1,T. ⦃L1, T1⦄ ⊆ ⦃L2, T⦄ →
(* Advanved properties with free variables inclusion ************************)
-lemma lfdeq_fsle_comp: ∀h,o. lfxs_fsle_compatible (cdeq h o).
+lemma lfdeq_fsge_comp: ∀h,o. lfxs_fsge_compatible (cdeq h o).
#h #o #L1 #L2 #T * #f1 #Hf1 #HL12
lapply (frees_lfdeq_conf h o … Hf1 … HL12)
lapply (lexs_fwd_length … HL12)
(* Basic_2A1: uses: lleq_sym *)
lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T).
-/3 width=3 by lfdeq_fsle_comp, lfxs_sym, tdeq_sym/ qed-.
+/3 width=3 by lfdeq_fsge_comp, lfxs_sym, tdeq_sym/ qed-.
(* Basic_2A1: uses: lleq_dec *)
lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≛[h, o, T] L2).
"syntactic equivalence on referred entries (local environment)"
'LazyEqSn T L1 L2 = (lfeq T L1 L2).
+(* Note: "lfeq_transitive R" is equivalent to "lfxs_transitive ceq R R" *)
(* Basic_2A1: uses: lleq_transitive *)
definition lfeq_transitive: predicate (relation3 lenv term term) ≝
λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2.
(* Basic inversion lemmas ***************************************************)
-lemma lfeq_transitive_inv_lfxs: ∀R. lfeq_transitive R → lfxs_transitive ceq R R.
-/2 width=3 by/ qed-.
-
lemma lfeq_inv_bind: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ{p,I}V.T] L2 →
∧∧ L1 ≡[V] L2 & L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V.
/2 width=2 by lfxs_inv_bind/ qed-.
(* Basic_properties *********************************************************)
-lemma lfxs_transitive_lfeq: ∀R. lfxs_transitive ceq R R → lfeq_transitive R.
-/2 width=5 by/ qed.
-
lemma frees_lfeq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f →
∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f.
#f #L1 #T #H elim H -f -L1 -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/static/lfxs_length.ma".
+include "basic_2/static/lfxs_fsle.ma".
+include "basic_2/static/lfeq.ma".
+
+(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
+
+(* Properties with free variables inclusion for restricted closures *********)
+
+lemma lfeq_fsle_comp: lfxs_fsle_compatible ceq.
+#L1 #L2 #T #HL12
+elim (frees_total L1 T)
+/4 width=8 by frees_lfeq_conf, lfxs_fwd_length, lveq_length_eq, sle_refl, ex4_4_intro/
+qed.
+
+(* Forward lemmas with free variables inclusion for restricted closures *****)
+
+lemma lfeq_lfxs_trans: ∀R. lfeq_transitive R →
+ ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
+/4 width=16 by lfeq_fsle_comp, lfxs_trans_fsle, lfxs_trans_next/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/static/lfxs_lfxs.ma".
-include "basic_2/static/lfeq.ma".
-
-(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********)
-
-(* Advanced forward lemmas **************************************************)
-
-(* Note: the proof should may invoke lfeq_transitive_inv_lfxs *)
-lemma lfeq_lfxs_trans: ∀R. c_reflexive … R → lfeq_transitive R →
- ∀L1,L,T. L1 ≡[T] L →
- ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2.
-/3 width=9 by lfxs_trans_gen/ qed-.
∀K1,K,V1. K1 ⪤*[R1, V1] K → ∀V. R1 K1 V1 V →
∀K2. K ⪤*[R2, V] K2 → K ⪤*[R2, V1] K2.
-definition lfxs_transitive: relation3 ? (relation3 ?? term) ? ≝
+definition lfxs_transitive: relation3 ? (relation3 ?? term) … ≝
λR1,R2,R3.
∀K1,K,V1. K1 ⪤*[R1, V1] K →
∀V. R1 K1 V1 V → ∀V2. R2 K V V2 → R3 K1 V1 V2.
∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ → ∀T. ⬆*[f] T ≡ U →
∃∃K1. ⬇*[b, f] L1 ≡ K1 & K1 ⪤*[R, T] K2.
+definition lfxs_transitive_next: relation3 … ≝ λR1,R2,R3.
+ ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f →
+ ∀g,I,K,n. ⬇*[n] L ≡ K.ⓘ{I} → ⫯g = ⫱*[n] f →
+ lexs_transitive (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
+
(* Properties with generic slicing for local environments *******************)
lemma lfxs_liftable_dedropable_sn: ∀R. (∀L. reflexive ? (R L)) →
/3 width=6 by cext2_d_liftable2_sn, cfull_lift_sn, ext2_refl, ex3_intro, ex2_intro/
qed-.
+lemma lfxs_trans_next: ∀R1,R2,R3. lfxs_transitive R1 R2 R3 → lfxs_transitive_next R1 R2 R3.
+#R1 #R2 #R3 #HR #f #L1 #T #Hf #g #I1 #K1 #n #HLK #Hgf #I #H
+generalize in match HLK; -HLK elim H -I1 -I
+[ #I #_ #L2 #_ #I2 #H
+ lapply (ext2_inv_unit_sn … H) -H #H destruct
+ /2 width=1 by ext2_unit/
+| #I #V1 #V #HV1 #HLK1 #L2 #HL12 #I2 #H
+ elim (ext2_inv_pair_sn … H) -H #V2 #HV2 #H destruct
+ elim (frees_inv_drops_next … Hf … HLK1 … Hgf) -f -HLK1 #f #Hf #Hfg
+ /5 width=5 by ext2_pair, sle_lexs_trans, ex2_intro/
+]
+qed.
+
(* Inversion lemmas with generic slicing for local environments *************)
(* Basic_2A1: uses: llpx_sn_inv_lift_le llpx_sn_inv_lift_be llpx_sn_inv_lift_ge *)
(**************************************************************************)
include "basic_2/relocation/lexs_length.ma".
-include "basic_2/static/frees_drops.ma".
include "basic_2/static/fsle_fsle.ma".
+include "basic_2/static/lfxs_drops.ma".
include "basic_2/static/lfxs_lfxs.ma".
(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-definition R_fsle_compatible: predicate (relation3 …) ≝ λRN.
+definition R_fsge_compatible: predicate (relation3 …) ≝ λRN.
∀L,T1,T2. RN L T1 T2 → ⦃L, T2⦄ ⊆ ⦃L, T1⦄.
-definition lfxs_fsle_compatible: predicate (relation3 …) ≝ λRN.
+definition lfxs_fsge_compatible: predicate (relation3 …) ≝ λRN.
∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L2, T⦄ ⊆ ⦃L1, T⦄.
+definition lfxs_fsle_compatible: predicate (relation3 …) ≝ λRN.
+ ∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L1, T⦄ ⊆ ⦃L2, T⦄.
+
(* Basic inversions with free variables inclusion for restricted closures ***)
-lemma frees_lexs_conf: ∀R. lfxs_fsle_compatible R →
+lemma frees_lexs_conf: ∀R. lfxs_fsge_compatible R →
∀L1,T,f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
∀L2. L1 ⪤*[cext2 R, cfull, f1] L2 →
∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
(* Properties with free variables inclusion for restricted closures *********)
(* Note: we just need lveq_inv_refl: ∀L,n1,n2. L ≋ⓧ*[n1, n2] L → ∧∧ 0 = n1 & 0 = n2 *)
-lemma fsle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ →
+lemma fsge_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ →
∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2.
#R #L1 #T1 #T2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #Hn #Hf #L2 #HL12
elim (lveq_inj_length … Hn ?) // #H1 #H2 destruct
/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/
qed-.
-lemma lfxs_sym: ∀R. lfxs_fsle_compatible R →
+lemma lfxs_sym: ∀R. lfxs_fsge_compatible R →
(∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) →
∀T. symmetric … (lfxs R T).
#R #H1R #H2R #T #L1 #L2
qed-.
lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
+ lfxs_fsge_compatible R1 →
∀L1,L2,V. L1 ⪤*[R1, V] L2 → ∀I,T.
∃∃L. L1 ⪤*[R1, ②{I}V.T] L & L ⪤*[R2, V] L2.
#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T
qed-.
lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
+ lfxs_fsge_compatible R1 →
∀L1,L2,T. L1 ⪤*[R1, T] L2 → ∀I,V.
∃∃L. L1 ⪤*[R1, ⓕ{I}V.T] L & L ⪤*[R2, T] L2.
#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V
qed-.
lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
+ lfxs_fsge_compatible R1 →
∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤*[R1, T] L2 → ∀p.
∃∃L,V. L1 ⪤*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤*[R2, T] L2 & R1 L1 V1 V.
#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p
qed-.
lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) →
- lfxs_fsle_compatible R1 →
+ lfxs_fsge_compatible R1 →
∀L1,L2,T. L1.ⓧ ⪤*[R1, T] L2 → ∀p,I,V.
∃∃L. L1 ⪤*[R1, ⓑ{p,I}V.T] L & L.ⓧ ⪤*[R2, T] L2.
#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #p #I #V
(* Main properties with free variables inclusion for restricted closures ****)
theorem lfxs_conf: ∀R1,R2.
- lfxs_fsle_compatible R1 →
- lfxs_fsle_compatible R2 →
+ lfxs_fsge_compatible R1 →
+ lfxs_fsge_compatible R2 →
R_confluent2_lfxs R1 R2 R1 R2 →
∀T. confluent2 … (lfxs R1 T) (lfxs R2 T).
#R1 #R2 #HR1 #HR2 #HR12 #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
]
]
qed-.
+
+theorem lfxs_trans_fsle: ∀R1,R2,R3.
+ lfxs_fsle_compatible R1 → lfxs_transitive_next R1 R2 R3 →
+ ∀L1,L,T. L1 ⪤*[R1, T] L →
+ ∀L2. L ⪤*[R2, T] L2 → L1 ⪤*[R3, T] L2.
+#R1 #R2 #R3 #H1R #H2R #L1 #L #T #H
+lapply (H1R … H) -H1R #H0
+cases H -H #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2
+lapply (fsle_inv_frees_eq … H0 … Hf1 … Hf2) -H0 -Hf2
+/4 width=14 by lexs_trans_gen, lexs_fwd_length, sle_lexs_trans, ex2_intro/
+qed-.
/3 width=7 by frees_fwd_isfin, frees_bind_void, lexs_join, isfin_tl, ex2_intro/
qed.
-theorem lfxs_trans_gen: ∀R1,R2,R3.
- c_reflexive … R1 → c_reflexive … R2 →
- lfxs_confluent R1 R2 → lfxs_transitive R1 R2 R3 →
- ∀L1,T,L. L1 ⪤*[R1, T] L →
- ∀L2. L ⪤*[R2, T] L2 → L1 ⪤*[R3, T] L2.
-#R1 #R2 #R3 #H1R #H2R #H3R #H4R #L1 #T @(fqup_wf_ind_eq (Ⓣ) … (⋆) L1 T) -L1 -T
-#G0 #L0 #T0 #IH #G #L1 * *
-[ #s #HG #HL #HT #L #H1 #L2 #H2 destruct
- elim (lfxs_inv_sort … H1) -H1 *
- [ #H1 #H0 destruct
- >(lfxs_inv_atom_sn … H2) -L2 //
- | #I1 #I #K1 #K #HK1 #H1 #H0 destruct
- elim (lfxs_inv_sort_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct
- /4 width=3 by lfxs_sort, fqu_fqup/
- ]
-| * [ | #i ] #HG #HL #HT #L #H1 #L2 #H2 destruct
- [ elim (lfxs_inv_zero … H1) -H1 *
- [ #H1 #H0 destruct
- >(lfxs_inv_atom_sn … H2) -L2 //
- | #I #K1 #K #V1 #V #HK1 #H1 #H0 #H destruct
- elim (lfxs_inv_zero_pair_sn … H2) -H2 #K2 #V2 #HK2 #HV2 #H destruct
- /4 width=7 by lfxs_pair, fqu_fqup, fqu_lref_O/
- | #f1 #I #K1 #K #Hf1 #HK1 #H1 #H0 destruct
- elim (lfxs_inv_zero_unit_sn … H2) -H2 #f2 #K2 #Hf2 #HK2 #H destruct
- /5 width=8 by lfxs_unit, lexs_trans_id_cfull, lexs_eq_repl_back, isid_inv_eq_repl/
- ]
- | elim (lfxs_inv_lref … H1) -H1 *
- [ #H1 #H0 destruct
- >(lfxs_inv_atom_sn … H2) -L2 //
- | #I1 #I #K1 #K #HK1 #H1 #H0 destruct
- elim (lfxs_inv_lref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct
- /4 width=3 by lfxs_lref, fqu_fqup/
- ]
- ]
-| #l #HG #HL #HT #L #H1 #L2 #H2 destruct
- elim (lfxs_inv_gref … H1) -H1 *
- [ #H1 #H0 destruct
- >(lfxs_inv_atom_sn … H2) -L2 //
- | #I1 #I #K1 #K #HK1 #H1 #H0 destruct
- elim (lfxs_inv_gref_bind_sn … H2) -H2 #I2 #K2 #HK2 #H destruct
- /4 width=3 by lfxs_gref, fqu_fqup/
- ]
-| #p #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct
- elim (lfxs_inv_bind … V1 V1 … H1) -H1 // #H1V #H1T
- elim (lfxs_inv_bind … V1 V1 … H2) -H2 // #H2V #H2T
- /3 width=4 by lfxs_bind/
-| #I #V1 #T1 #HG #HL #HT #L #H1 #L2 #H2 destruct
- elim (lfxs_inv_flat … H1) -H1 #H1V #H1T
- elim (lfxs_inv_flat … H2) -H2 #H2V #H2T
- /3 width=3 by lfxs_flat/
-]
-qed-.
-
(* Negated inversion lemmas *************************************************)
(* Basic_2A1: uses: nllpx_sn_inv_bind nllpx_sn_inv_bind_O *)
}
]
[ { "syntactic equivalence" * } {
- [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ]
+ [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ]
}
]
[ { "generic extension of a context-sensitive relation" * } {
projects / helm.git / commitdiff