(* Basic properties *********************************************************)
+lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆.
+#f @drops_atom #H destruct
+qed.
+
lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⬇*[b, f] L1 ≡ L2).
#b #L1 #L2 #f1 #H elim H -f1 -L1 -L2
[ /4 width=3 by drops_atom, isid_eq_repl_back/
| #f2 #I #L1 #L2 #V #_ #IHL #J #K #W #H elim (IHL … H) -IHL
/3 width=7 by after_next, ex3_2_intro, drops_drop/
| #f2 #I #L1 #L2 #V1 #V2 #HL #_ #_ #J #K #W #H destruct
- lapply (isid_after_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
+ lapply (after_isid_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
]
qed-.
[ #H elim (isid_inv_next … H) -H //
| /2 width=5 by ex2_3_intro/
]
-qed-.
+qed-.
+
+(* Properties with uniform relocations **************************************)
+
+lemma drops_uni_ex: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∨ ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V.
+#L elim L -L /2 width=1 by or_introl/
+#L #I #V #IH * /4 width=4 by drops_refl, ex1_3_intro, or_intror/
+#i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/
+* /4 width=4 by drops_drop, ex1_3_intro, or_intror/
+qed-.
(* Basic_2A1: removed theorems 12:
drops_inv_nil drops_inv_cons d1_liftable_liftables
(* Basic_2A1: includes: drop_mono *)
lemma drops_mono: ∀b1,f,L,L1. ⬇*[b1, f] L ≡ L1 →
∀b2,L2. ⬇*[b2, f] L ≡ L2 → L1 = L2.
-#b1 #f #L #L1 lapply (isid_after_dx 𝐈𝐝 … f)
+#b1 #f #L #L1 lapply (after_isid_dx 𝐈𝐝 … f)
/3 width=8 by drops_conf, drops_fwd_isid/
qed-.
lapply (drops_mono … H0 … Hf2) -L #H
destruct /2 width=1 by and3_intro/
qed-.
+
+lemma drops_inv_uni: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → ∀I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V → ⊥.
+#L #i #H1 #I #K #V #H2
+lapply (drops_F … H2) -H2 #H2
+lapply (drops_mono … H2 … H1) -L -i #H destruct
+qed-.
(* Basic forward lemmas *****************************************************)
+lemma lifts_fwd_atom2: ∀f,I,X. ⬆*[f] X ≡ ⓪{I} → ∃J. X = ⓪{J}.
+#f * #n #X #H
+[ lapply (lifts_inv_sort2 … H)
+| elim (lifts_inv_lref2 … H)
+| lapply (lifts_inv_gref2 … H)
+] -H /2 width=2 by ex_intro/
+qed-.
+
(* Basic_2A1: includes: lift_inv_O2 *)
lemma lifts_fwd_isid: ∀f,T1,T2. ⬆*[f] T1 ≡ T2 → 𝐈⦃f⦄ → T1 = T2.
#f #T1 #T2 #H elim H -f -T1 -T2
(* Basic_2A1: includes: lift_inj *)
lemma lifts_inj: ∀f,T1,U. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2.
-#f #T1 #U #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝 … f)
+#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝 … f)
/3 width=6 by lifts_div3, lifts_fwd_isid/
qed-.
(* Basic_2A1: includes: lift_mono *)
lemma lifts_mono: ∀f,T,U1. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
-#f #T #U1 #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝 … f)
+#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝 … f)
/3 width=6 by lifts_conf, lifts_fwd_isid/
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/lpx_sn_drop.ma".
+include "basic_2/rt_transition/cpx_drops.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+
+(* Properties on local environment slicing ***********************************)
+
+lemma lpx_drop_conf: ∀h,o,G. dropable_sn (lpx h o G).
+/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+
+lemma drop_lpx_trans: ∀h,o,G. dedropable_sn (lpx h o G).
+/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+
+lemma lpx_drop_trans_O1: ∀h,o,G. dropable_dx (lpx h o G).
+/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/multiple/frees_lreq.ma".
+include "basic_2/multiple/frees_lift.ma".
+*)
+include "basic_2/s_computation/fqup_weight.ma".
+include "basic_2/rt_transition/cpx_drops.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+
+(* Properties with context-sensitive free variables ***************************)
+
+lemma lpx_cpx_frees_fwd_sge: ∀h,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ⬈[h] U2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, U1] L2 →
+ ∀g1. L1 ⊢ 𝐅*⦃U1⦄ ≡ g1 → ∀g2. L2 ⊢ 𝐅*⦃U2⦄ ≡ g2 →
+ g2 ⊆ g1.
+#h #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1
+#G0 #L0 #U0 #IH #G #L1 * *
+[ #s #HG #HL #HU #U2 #H0 #L2 #_ #g1 #H1 #g2 #H2 -IH -G0 -L0 -U0
+ elim (cpx_inv_sort1 … H0) -H0 #H destruct
+ /3 width=3 by frees_inv_sort, sle_isid_sn/
+| #i #HG #HL #HU #U2 #H0 #L2 #HL12 #g1 #H1 #g2 #H2 destruct
+ elim (cpx_inv_lref1_drops … H0) -H0
+ [ #H destruct
+ lapply (frees_inv_lref … H1) -H1 #Hg1
+ lapply (frees_inv_sort … H2) -H2 #Hg2 /2 width=1 by sle_isid_sn/
+
+
+
+| #l #HG #HL #HU #U2 #H0 #L2 #_ #g1 #H1 #g2 #H2 -IH -G0 -L0 -U0
+ lapply (cpx_inv_gref1 … H0) -H0 #H destruct
+ /3 width=3 by frees_inv_gref, sle_isid_sn/
+
+| #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_drop_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 (drop_fwd_drop2 … HLK1) #H0
+ elim (lpx_drop_conf … H0 … HL12) -H0 -HL12 #K2 #HK12 #HLK2
+ elim (ylt_split i (j+1)) >yplus_SO2 #Hji
+ [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by ylt_fwd_succ2/
+ | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // destruct
+ /4 width=11 by frees_lref_be, fqup_lref, yle_succ1_inj/
+ ]
+ ]
+| -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 (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, drop_drop/
+ ]
+| #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct
+ elim (cpx_inv_flat1 … HX2) -HX2 *
+ [ #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 (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 (lreq_frees_trans … Hi (L2.ⓛV2) ?) /2 width=1 by lreq_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, drop_drop/
+ | /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
+ ]
+ ]
+ ]
+]
+qed-.
+
+lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G).
+/2 width=8 by lpx_cpx_frees_trans/ qed-.
+
+lemma lpx_frees_trans: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 →
+ ∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄.
+/2 width=8 by lpx_cpx_frees_trans/ 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/lpx_sn_drop.ma".
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/lpx.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on local environment slicing ***********************************)
-
-lemma lpx_drop_conf: ∀h,o,G. dropable_sn (lpx h o G).
-/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
-
-lemma drop_lpx_trans: ∀h,o,G. dedropable_sn (lpx h o G).
-/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
-
-lemma lpx_drop_trans_O1: ∀h,o,G. dropable_dx (lpx h o G).
-/2 width=3 by lpx_sn_dropable/ qed-.
-
-(* Properties on supclosure *************************************************)
-
-lemma fqu_lpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, o] K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, o] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
-[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
- #K2 #W2 #HLK2 #HVW2 #H destruct
- /3 width=5 by cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #K2 #HK12
- elim (drop_lpx_trans … HLK1 … HK12) -HK12
- /3 width=7 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma fquq_lpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, o] K2 →
- ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, o] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
-[ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
- #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
- /4 width=7 by cpx_delta, fqu_drop, drop_drop, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #L0 #HL01
- elim (lpx_drop_trans_O1 … HL01 … HLK1) -L1
- /3 width=5 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-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/multiple/frees_lreq.ma".
-include "basic_2/multiple/frees_lift.ma".
-include "basic_2/reduction/lpx_drop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on context-sensitive free variables ***************************)
-
-lemma lpx_cpx_frees_trans: ∀h,o,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, o] U2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 →
- ∀i. L2 ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U1⦄.
-#h #o #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1
-#G0 #L0 #U0 #IH #G #L1 * *
-[ -IH #s #HG #HL #HU #U2 #H1 #L2 #_ #i #H2 elim (cpx_inv_sort1 … H1) -H1
- [| * #d #_ ] #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_drop_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 (drop_fwd_drop2 … HLK1) #H0
- elim (lpx_drop_conf … H0 … HL12) -H0 -HL12 #K2 #HK12 #HLK2
- elim (ylt_split i (j+1)) >yplus_SO2 #Hji
- [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by ylt_fwd_succ2/
- | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // destruct
- /4 width=11 by frees_lref_be, fqup_lref, yle_succ1_inj/
- ]
- ]
-| -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 (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, drop_drop/
- ]
-| #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct
- elim (cpx_inv_flat1 … HX2) -HX2 *
- [ #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 (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 (lreq_frees_trans … Hi (L2.ⓛV2) ?) /2 width=1 by lreq_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, drop_drop/
- | /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
- ]
- ]
- ]
-]
-qed-.
-
-lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G).
-/2 width=8 by lpx_cpx_frees_trans/ qed-.
-
-lemma lpx_frees_trans: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 →
- ∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄.
-/2 width=8 by lpx_cpx_frees_trans/ qed-.
(**************************************************************************)
include "ground_2/relocation/rtmap_pushs.ma".
+include "ground_2/relocation/rtmap_coafter.ma".
+include "basic_2/relocation/lifts_lifts.ma".
include "basic_2/relocation/drops.ma".
include "basic_2/static/frees.ma".
(* Advanced properties ******************************************************)
-lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆.
-#f @drops_atom #H destruct
+lemma frees_lref_atom: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → L ⊢ 𝐅*⦃#i⦄ ≡ 𝐈𝐝.
+#L elim L -L /2 width=1 by frees_atom/
+#L #I #V #IH *
+[ #H lapply (drops_fwd_isid … H ?) -H // #H destruct
+| /4 width=3 by frees_lref, drops_inv_drop1/
+]
+qed.
+
+lemma frees_lref_pair: ∀f,K,V. K ⊢ 𝐅*⦃V⦄ ≡ f →
+ ∀i,I,L. ⬇*[i] L ≡ K.ⓑ{I}V → L ⊢ 𝐅*⦃#i⦄ ≡ ↑*[i] ⫯f.
+#f #K #V #Hf #i elim i -i
+[ #I #L #H lapply (drops_fwd_isid … H ?) -H /2 width=1 by frees_zero/
+| #i #IH #I #L #H elim (drops_inv_succ … H) -H /3 width=2 by frees_lref/
+]
qed.
+(* Advanced inversion lemmas ************************************************)
+
lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f →
(⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∧ 𝐈⦃f⦄) ∨
∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g &
]
qed-.
+(* Properties with generic slicing for local environments *******************)
+(* Inversion lemmas with generic slicing for local environments *************)
-lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
-#L #U @(f2_ind … rfw … L U) -L -U
-#x #IH #L * *
-[ -IH /3 width=5 by frees_inv_sort, or_intror/
-| #j #Hx #l #i elim (ylt_split_eq i j) #Hji
- [ -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
- | -x /2 width=1 by or_introl/
- | elim (ylt_split j l) #Hli
- [ -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_skip … H ?) -L //
- | elim (lt_or_ge j (|L|)) #Hj
- [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
- elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
- @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
- lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
- | -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_free … H ?) -l //
- ]
- ]
- ]
-| -IH /3 width=5 by frees_inv_gref, or_intror/
-| #a #I #W #U #Hx #l #i destruct
- elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
- elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
- @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
-| #I #W #U #Hx #l #i destruct
- elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
- elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
- @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
-]
-qed-.
-
-lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
- (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
-#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
-* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
-lapply (yle_inv_inj … Hlj) -Hlj #Hlj
-elim (le_to_or_lt_eq … Hlj) -Hlj
-[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
-| -Hji -HnU #H destruct
- lapply (drop_mono … HLK0 … HLK) #H destruct -I
- elim HnW0 -L -U -HnW0 //
-]
-qed.
-
-(* Note: lemma 1250 *)
-lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
- L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
-#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,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
- ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
- L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
-#K #T #l #i #H elim H -K -T -l -i
-[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
- @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
-| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
- elim (ylt_split j l0) #H0
- [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW
- @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/
- [ lapply (ylt_fwd_lt_O1 … H0) #H1
- #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU
- <(ylt_inv_O1 l0) in H0; // -H1 #H0
- elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/
- | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/
- <yplus_pred1 /4 width=5 by monotonic_yle_minus_dx, yle_pred, ylt_to_minus/
- ]
- | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
- lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
- @(frees_be … HLK0) -HLK0 -IHV
- /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/
- [ #X <yplus_inj #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
- | <yplus_minus_assoc_comm_inj //
- ]
- ]
-]
-qed.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
- ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
- elim (lift_split … HTU i m0) -HTU /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
- elim (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- @(IHW … HKL0 … HVW)
- [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
- | >yplus_pred1 /2 width=1 by ylt_to_minus/
- <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
- ]
- | elim (lift_split … HTU j m0) -HTU /3 width=3 by ylt_yle_trans, ylt_fwd_le/
- ]
-]
-qed-.
-
-lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
- K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
- elim (yle_inv_plus_inj2 … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
- elim (lift_trans_le … HXT … HTU) -T // >ymax_pre_sn /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
- elim (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i
- @(frees_be … H) -H
- [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
- | /2 width=3 by ylt_yle_trans/
- | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/
- | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
- >yplus_pred1 /2 width=1 by ylt_to_minus/
- <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
- ]
- | elim (ylt_split j (l0+m0)) #H2
- [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct
- lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3
- lapply (ylt_fwd_lt_O1 … H3) -H3 #H3
- elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/
- [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ <minus_n_n
- -H2 #X #_ #H elim (HnU … H)
- | <yminus_inj >yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/
- ]
- | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
- elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
- @(frees_be … HK0)
- [ /2 width=1 by monotonic_yle_minus_dx/
- | /2 width=1 by monotonic_ylt_minus_dx/
- | #X #HXT elim (lift_trans_le … HXT … HTU) -T //
- <yminus_inj >ymax_pre_sn /2 width=2 by/
- | <yminus_inj >yplus_minus_assoc_comm_inj //
- >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/
- ]
- ]
- ]
+lemma frees_inv_lifts: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →
+ ∀f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U →
+ ∀f1. f ~⊚ f1 ≡ f2 → K ⊢ 𝐅*⦃T⦄ ≡ f1.
+#b #f2 #L #U #H lapply (frees_fwd_isfin … H) elim H -f2 -L -U
+[ #f2 #I #Hf2 #_ #f #K #H1 #T #H2 #f1 #H3
+ lapply (coafter_fwd_isid2 … H3 … Hf2) -H3 // -Hf2 #Hf1
+ elim (drops_inv_atom1 … H1) -H1 #H #_ destruct
+ elim (lifts_fwd_atom2 … H2) -H2
+ /2 width=3 by frees_atom/
+| #f2 #I #L #W #s #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ lapply (lifts_inv_sort2 … H2) -H2 #H destruct
+ elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1
+ ] /3 width=4 by frees_sort/
+| #f2 #I #L #W #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_inv_next … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (lifts_inv_lref2 … H2) -H2 #i #H2 #H destruct
+ lapply (at_inv_xxp … H2 ?) -H2 // * #g #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
+ elim (coafter_inv_pxn … H3) -H3 [ |*: // ] #g1 #Hf2 #H destruct
+ /3 width=4 by frees_zero/
+| #f2 #I #L #W #j #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (lifts_inv_lref2 … H2) -H2 #x #H2 #H destruct
+ elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
+ elim (at_inv_xpn … H2) -H2 [ |*: // ] #j #Hg #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1
+ lapply (at_inv_xnn … H2 ????) -H2 [5: |*: // ]
+ ] /4 width=4 by lifts_lref, frees_lref/
+| #f2 #I #L #W #l #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ lapply (lifts_inv_gref2 … H2) -H2 #H destruct
+ elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1
+ ] /3 width=4 by frees_gref/
+| #f2W #f2U #f2 #p #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
+ elim (sor_inv_isfin3 … H1f2) // #H1f2W #H
+ lapply (isfin_inv_tl … H) -H
+ elim (lifts_inv_bind2 … H2) -H2 #V #T #HVW #HTU #H destruct
+ elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 // #f1W #f1U #H2f2W #H
+ elim (coafter_inv_tl0 … H) -H /4 width=5 by frees_bind, drops_skip/
+| #f2W #f2U #f2 #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
+ elim (sor_inv_isfin3 … H1f2) //
+ elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
+ elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 /3 width=5 by frees_flat/
]
qed-.
}
]
[ { "context-sensitive free variables" * } {
- [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_frees" * ]
+ [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_drops" + "frees_frees" * ]
}
]
}
f1 ≗ g1 → f2 ≗ g2 → f ≗ g.
/4 width=4 by coafter_mono, coafter_eq_repl_back1, coafter_eq_repl_back2/ qed-.
+(* Inversion lemmas with tail ***********************************************)
+
+lemma coafter_inv_tl0: ∀g2,g1,g. g2 ~⊚ g1 ≡ ⫱g →
+ ∃∃f1. ↑g2 ~⊚ f1 ≡ g & ⫱f1 = g1.
+#g1 #g2 #g elim (pn_split g) * #f #H0 #H destruct
+[ /3 width=7 by coafter_refl, ex2_intro/
+| @(ex2_intro … (⫯g2)) /2 width=7 by coafter_push/ (**) (* full auto fails *)
+]
+qed-.
+
(* Properties on tls ********************************************************)
lemma coafter_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
#f elim (pn_split f) * #g #H #Hf destruct
/3 width=3 by isfin_fwd_push, isfin_inv_next/
qed.
+
+(* Inversion lemmas with tail ***********************************************)
+
+lemma isfin_inv_tl: ∀f. 𝐅⦃⫱f⦄ → 𝐅⦃f⦄.
+#f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/
+qed-.
/4 width=6 by sor_mono, fcla_eq_repl_back, ex3_intro/
qed-.
+(* Forward lemmas with finite colength **************************************)
+
+lemma sor_fwd_fcla_sn_ex: ∀f,n. 𝐂⦃f⦄ ≡ n → ∀f1,f2. f1 ⋓ f2 ≡ f →
+ ∃∃n1. 𝐂⦃f1⦄ ≡ n1 & n1 ≤ n.
+#f #n #H elim H -f -n
+[ /4 width=4 by sor_fwd_isid1, fcla_isid, ex2_intro/
+| #f #n #_ #IH #f1 #f2 #H
+ elim (sor_inv_xxp … H) -H [ |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
+ elim (IH … Hf) -f /3 width=3 by fcla_push, ex2_intro/
+| #f #n #_ #IH #f1 #f2 #H
+ elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
+ elim (IH … Hf) -f /3 width=3 by fcla_push, fcla_next, le_S_S, le_S, ex2_intro/
+]
+qed-.
+
+lemma sor_fwd_fcla_dx_ex: ∀f,n. 𝐂⦃f⦄ ≡ n → ∀f1,f2. f1 ⋓ f2 ≡ f →
+ ∃∃n2. 𝐂⦃f2⦄ ≡ n2 & n2 ≤ n.
+/3 width=4 by sor_fwd_fcla_sn_ex, sor_sym/ qed-.
+
(* Properties on test for finite colength ***********************************)
lemma sor_isfin_ex: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∃∃f. f1 ⋓ f2 ≡ f & 𝐅⦃f⦄.
/3 width=6 by sor_mono, isfin_eq_repl_back/
qed-.
+(* Forward lemmas with test for finite colength *****************************)
+
+lemma sor_fwd_isfin_sn: ∀f. 𝐅⦃f⦄ → ∀f1,f2. f1 ⋓ f2 ≡ f → 𝐅⦃f1⦄.
+#f * #n #Hf #f1 #f2 #H
+elim (sor_fwd_fcla_sn_ex … Hf … H) -f -f2 /2 width=2 by ex_intro/
+qed-.
+
+lemma sor_fwd_isfin_dx: ∀f. 𝐅⦃f⦄ → ∀f1,f2. f1 ⋓ f2 ≡ f → 𝐅⦃f2⦄.
+#f * #n #Hf #f1 #f2 #H
+elim (sor_fwd_fcla_dx_ex … Hf … H) -f -f1 /2 width=2 by ex_intro/
+qed-.
+
+(* Inversion lemmas with test for finite colength ***************************)
+
+lemma sor_inv_isfin3: ∀f1,f2,f. f1 ⋓ f2 ≡ f → 𝐅⦃f⦄ → 𝐅⦃f1⦄ ∧ 𝐅⦃f2⦄.
+/3 width=4 by sor_fwd_isfin_dx, sor_fwd_isfin_sn, conj/ qed-.
+
(* Inversion lemmas on inclusion ********************************************)
corec lemma sor_inv_sle_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f1 ⊆ f.
projects / helm.git / commitdiff