lemma cprs_strap1: ∀G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3 by step/ qed.
+normalize /2 width=3 by step/ qed-.
(* Basic_1: was: pr3_step *)
lemma cprs_strap2: ∀G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 ➡ T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3 by TC_strap/ qed.
+normalize /2 width=3 by TC_strap/ qed-.
lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
/3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/
(* Basic_1: was: pr3_gen_cast *)
lemma cprs_inv_cast1: ∀G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡* U2 → ⦃G, L⦄ ⊢ T1 ➡* U2 ∨
∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L⦄ ⊢ T1 ➡* T2 & U2 = ⓝW2.T2.
-#G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_intror/
#U2 #U #_ #HU2 * /3 width=3 by cprs_strap1, or_introl/ *
#W #T #HW1 #HT1 #H destruct
elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3 by cprs_strap1, or_introl/ *
lemma csx_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T →
⦃G, L⦄ ⊢ ⬊*[h, g] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T.
-#h #g #G #L #T #Vs elim Vs -Vs /2 width=1/
+#h #g #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/
#V #Vs #IHVs #HVs
lapply (csx_fwd_pair_sn … HVs) #HV
lapply (csx_fwd_flat_dx … HVs) -HVs #HVs
-elim (IHVs HVs) -IHVs -HVs /3 width=1/
+elim (IHVs HVs) -IHVs -HVs /3 width=1 by conj/
qed-.
(* Basic_1: was: sc3_arity_csubc *)
theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
gcp RR RS RP → gcr RR RS RP RP →
- ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⬇*[Ⓕ, des] L0 ≡ L1 →
- ∀T0. ⬆*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+ ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,cs. ⬇*[Ⓕ, cs] L0 ≡ L1 →
+ ∀T0. ⬆*[cs] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
-[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20
+[ #G #L #k #L0 #cs #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #cs #HL01 #X #H #L2 #HL20
lapply (acr_gcr … H1RP H2RP B) #HB
elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
lapply (drop_fwd_drop2 … HLK1) #HK1b
- elim (drops_drop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hcs1
+ elim (drops_drop_trans … HL01 … HLK1) #X #cs1 #i0 #HL0 #H #Hi0 #Hcs1
>(at_mono … Hi1 … Hi0) -i1
- elim (drops_inv_skip2 … Hcs1 … H) -des1 #K0 #V0 #des0 #Hcs0 #HK01 #HV10 #H destruct
+ elim (drops_inv_skip2 … Hcs1 … H) -cs1 #K0 #V0 #cs0 #Hcs0 #HK01 #HV10 #H destruct
elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
elim (lsubc_inv_pair2 … H) -H *
[ #K2 #HK20 #H destruct
lapply (s5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/
lapply (s7 … HB G L2 (◊)) /3 width=7 by gcr_lift/
]
-| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (acr_gcr … H1RP H2RP B) #HB
lapply (s1 … HB) -HB #HB
lapply (s6 … HA G L2 (◊) (◊)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/
-| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
+| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL02
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
@(acr_abst … H1RP H2RP) /2 width=5 by/
- #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
+ #L3 #V3 #W3 #T3 #cs3 #HL32 #HW03 #HT03 #H1B #H2B
elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
- @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
+ lapply (aaa_lifts … L2 W3 … (cs @@ cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
+ @(IHA (L2. ⓛW3) … (cs + 1 @@ cs3 + 1)) -IHA
/3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
-| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
+| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
/3 width=10 by drops_nil, lifts_nil/
-| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
+| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #cs #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (s7 … HA G L2 (◊)) /3 width=5 by/
(* the functional construction for candidates *)
definition cfun: candidate → candidate → candidate ≝
- λC1,C2,G,K,T. ∀L,W,U,des.
- ⬇*[Ⓕ, des] L ≡ K → ⬆*[des] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
+ λC1,C2,G,K,T. ∀L,W,U,cs.
+ ⬇*[Ⓕ, cs] L ≡ K → ⬆*[cs] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
(* the reducibility candidate associated to an atomic arity *)
let rec acr (RP:candidate) (A:aarity) on A: candidate ≝
[ lapply (s2 … IHB G L (◊) … HK) //
| /3 width=6 by s1, cp3/
]
-| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB
+| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
lapply (s1 … IHB … HB) #HV0
@(s2 … IHA … (V0 @ V0s))
/3 width=14 by gcp2_lifts_all, gcp2_lifts, gcp0_lifts, lifts_simple_dx, conj/
-| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB
+| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
@(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
-| #G #L #Vs #HVs #k #L0 #V0 #X #des #HL0 #H #HB
+| #G #L #Vs #HVs #k #L0 #V0 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
>(lifts_inv_sort1 … HY) -Y
lapply (s1 … IHB … HB) #HV0
@(s4 … IHA … (V0 @ V0s)) /3 width=7 by gcp2_lifts_all, conj/
-| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB
+| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
- elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hcs0
+ elim (drops_drop_trans … HL0 … HLK) #X #cs0 #i1 #HL02 #H #Hi1 #Hcs0
>(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
- elim (drops_inv_skip2 … Hcs0 … H) -H -des0 #L2 #W1 #des0 #Hcs0 #HLK #HVW1 #H destruct
+ elim (drops_inv_skip2 … Hcs0 … H) -H -cs0 #L2 #W1 #cs0 #Hcs0 #HLK #HVW1 #H destruct
elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
elim (lifts_lift_trans … Hcs0 … HVW1 … HW12) // -Hcs0 -Hi0 #V3 #HV13 #HVW2
>(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
@(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
-| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HL0 #H #HB
+| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
elim (lift_total V10 0 1) #V20 #HV120
elim (liftv_total 0 1 V10s) #V20s #HV120s
@(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by gcp2_lifts, liftv_cons/
- @(HA … (des + 1)) /2 width=2 by drops_skip/
+ @(HA … (cs + 1)) /2 width=2 by drops_skip/
[ @lifts_applv //
elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
>(liftv_mono … HV12s … HV10s) -V1s //
| @(gcr_lift … H1RP … HB … HV120) /2 width=2 by drop_drop/
]
-| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB
+| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #cs #HL0 #H #HB
elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
@(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
- ∀L0,V0,W0,T0,des. ⬇*[Ⓕ, des] L0 ≡ L → ⬆*[des] W ≡ W0 → ⬆*[des + 1] T ≡ T0 →
+ ∀L0,V0,W0,T0,cs. ⬇*[Ⓕ, cs] L0 ≡ L → ⬆*[cs] W ≡ W0 → ⬆*[cs + 1] T ≡ T0 →
⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
) →
⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
-#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB
+#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #cs #HL0 #H #HB
lapply (acr_gcr … H1RP H2RP A) #HCA
lapply (acr_gcr … H1RP H2RP B) #HCB
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
(* Basic properties *********************************************************)
lemma lpr_lprs: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=1/ qed.
+/2 width=1 by inj/ qed.
lemma lprs_refl: ∀G,L. ⦃G, L⦄ ⊢ ➡* L.
-/2 width=1/ qed.
+/2 width=1 by lpr_lprs/ qed.
lemma lprs_strap1: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡* L → ⦃G, L⦄ ⊢ ➡ L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
+/2 width=3 by step/ qed-.
lemma lprs_strap2: ∀G,L1,L,L2. ⦃G, L1⦄ ⊢ ➡ L → ⦃G, L⦄ ⊢ ➡* L2 → ⦃G, L1⦄ ⊢ ➡* L2.
-/2 width=3/ qed.
+/2 width=3 by TC_strap/ qed-.
lemma lprs_pair_refl: ∀G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡* L2.ⓑ{I}V.
/2 width=1 by TC_lpx_sn_pair_refl/ qed.
/3 width=3 by TC_confluent2, lpr_conf/ qed-.
theorem lprs_trans: ∀G. Transitive … (lprs G).
-/2 width=3/ qed-.
+/2 width=3 by trans_TC/ qed-.
(* Basic_1: was: csubc_drop1_conf_rev *)
lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP →
- ∀G,L1,K1,des. ⬇*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
- ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[Ⓕ, des] L2 ≡ K2.
-#RR #RS #RP #Hgcp #G #L1 #K1 #des #H elim H -L1 -K1 -des
+ ∀G,L1,K1,cs. ⬇*[Ⓕ, cs] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
+ ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[Ⓕ, cs] L2 ≡ K2.
+#RR #RS #RP #Hgcp #G #L1 #K1 #cs #H elim H -L1 -K1 -cs
[ /2 width=3 by drops_nil, ex2_intro/
-| #L1 #L #K1 #des #l #m #_ #HLK1 #IHL #K2 #HK12
+| #L1 #L #K1 #cs #l #m #_ #HLK1 #IHL #K2 #HK12
elim (drop_lsubc_trans … Hgcp … HLK1 … HK12) -Hgcp -K1 #K #HLK #HK2
elim (IHL … HLK) -IHL -HLK /3 width=5 by drops_cons, ex2_intro/
]
(* Basic properties *********************************************************)
lemma cpc_refl: ∀G,L. reflexive … (cpc G L).
-/2 width=1/ qed.
+/2 width=1 by or_intror/ qed.
lemma cpc_sym: ∀G,L. symmetric … (cpc L G).
-#G #L #T1 #T2 * /2 width=1/
-qed.
+#G #L #T1 #T2 * /2 width=1 by or_introl, or_intror/
+qed-.
(* Basic forward lemmas *****************************************************)
lemma cpc_fwd_cpr: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ∃∃T. ⦃G, L⦄ ⊢ T1 ➡ T & ⦃G, L⦄ ⊢ T2 ➡ T.
-#G #L #T1 #T2 * /2 width=3/
+#G #L #T1 #T2 * /2 width=3 by ex2_intro/
qed-.
theorem cpc_conf: ∀G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌ T1 → ⦃G, L⦄ ⊢ T0 ⬌ T2 →
∃∃T. ⦃G, L⦄ ⊢ T1 ⬌ T & ⦃G, L⦄ ⊢ T2 ⬌ T.
-/3 width=3/ qed-.
+/3 width=3 by cpc_sym, ex2_intro/ qed-.
(* Basic_1: was: pc3_s *)
lemma cpcs_sym: ∀G,L. symmetric … (cpcs G L).
-#G #L @TC_symmetric // qed-. (**) (* auto fails even after normalize *)
+normalize /3 width=1 by cpc_sym, TC_symmetric/
+qed-.
lemma cpc_cpcs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌ T2 → ⦃G, L⦄ ⊢ T1 ⬌* T2.
/2 width=1 by inj/ qed.
lemma lenv_ind_alt: ∀R:predicate lenv.
R (⋆) → (∀I,L,T. R L → R (ⓑ{I}T.L)) →
∀L. R L.
-#R #IH1 #IH2 #L @(f_ind … length … L) -L #n #IHn * // -IH1
+#R #IH1 #IH2 #L @(f_ind … length … L) -L #x #IHx * // -IH1
#L #I #V normalize #H destruct elim (lpair_ltail L I V) /3 width=1 by/
qed-.
(* Basic properties *********************************************************)
lemma lw_pair: ∀I,L,V. ♯{L} < ♯{L.ⓑ{I}V}.
-/3 width=1/ qed.
+/3 width=1 by lt_plus_to_minus_r, monotonic_lt_plus_r/ qed.
(* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *)
(* Basic_1: removed local theorems 1: clt_wf__q_ind *)
qed.
lemma simple_inv_bind: ∀a,I,V,T. 𝐒⦃ⓑ{a,I} V. T⦄ → ⊥.
-/2 width=7/ qed-.
+/2 width=7 by simple_inv_bind_aux/ qed-.
lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J.
-* /2 width=2/ #a #I #V #T #H
+* /2 width=2 by ex_intro/ #a #I #V #T #H
elim (simple_inv_bind … H)
qed-.
inductive drops (s:bool): list2 nat nat → relation lenv ≝
| drops_nil : ∀L. drops s (◊) L L
-| drops_cons: ∀L1,L,L2,des,l,m.
- drops s des L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ des) L1 L2
+| drops_cons: ∀L1,L,L2,cs,l,m.
+ drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s ({l, m} @ cs) L1 L2
.
interpretation "iterated slicing (local environment) abstract"
- 'RDropStar s des T1 T2 = (drops s des T1 T2).
+ 'RDropStar s cs T1 T2 = (drops s cs T1 T2).
(*
interpretation "iterated slicing (local environment) general"
'RDropStar des T1 T2 = (drops true des T1 T2).
∀U. ⬆[l, m] T ≡ U → R L U.
definition d_liftables1: relation2 lenv term → predicate bool ≝
- λR,s. ∀L,K,des. ⬇*[s, des] L ≡ K →
- ∀T,U. ⬆*[des] T ≡ U → R K T → R L U.
+ λR,s. ∀L,K,cs. ⬇*[s, cs] L ≡ K →
+ ∀T,U. ⬆*[cs] T ≡ U → R K T → R L U.
definition d_liftables1_all: relation2 lenv term → predicate bool ≝
- λR,s. ∀L,K,des. ⬇*[s, des] L ≡ K →
- ∀Ts,Us. ⬆*[des] Ts ≡ Us →
+ λR,s. ∀L,K,cs. ⬇*[s, cs] L ≡ K →
+ ∀Ts,Us. ⬆*[cs] Ts ≡ Us →
all … (R K) Ts → all … (R L) Us.
(* Basic inversion lemmas ***************************************************)
-fact drops_inv_nil_aux: ∀L1,L2,s,des. ⬇*[s, des] L1 ≡ L2 → des = ◊ → L1 = L2.
-#L1 #L2 #s #des * -L1 -L2 -des //
-#L1 #L #L2 #l #m #des #_ #_ #H destruct
+fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = ◊ → L1 = L2.
+#L1 #L2 #s #cs * -L1 -L2 -cs //
+#L1 #L #L2 #l #m #cs #_ #_ #H destruct
qed-.
(* Basic_1: was: drop1_gen_pnil *)
lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, ◊] L1 ≡ L2 → L1 = L2.
/2 width=4 by drops_inv_nil_aux/ qed-.
-fact drops_inv_cons_aux: ∀L1,L2,s,des. ⬇*[s, des] L1 ≡ L2 →
- ∀l,m,tl. des = {l, m} @ tl →
+fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 →
+ ∀l,m,tl. cs = {l, m} @ tl →
∃∃L. ⬇*[s, tl] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
-#L1 #L2 #s #des * -L1 -L2 -des
+#L1 #L2 #s #cs * -L1 -L2 -cs
[ #L #l #m #tl #H destruct
-| #L1 #L #L2 #des #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
+| #L1 #L #L2 #cs #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
/2 width=3 by ex2_intro/
]
qed-.
(* Basic_1: was: drop1_gen_pcons *)
-lemma drops_inv_cons: ∀L1,L2,s,l,m,des. ⬇*[s, {l, m} @ des] L1 ≡ L2 →
- ∃∃L. ⬇*[s, des] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
+lemma drops_inv_cons: ∀L1,L2,s,l,m,cs. ⬇*[s, {l, m} @ cs] L1 ≡ L2 →
+ ∃∃L. ⬇*[s, cs] L1 ≡ L & ⬇[s, l, m] L ≡ L2.
/2 width=3 by drops_inv_cons_aux/ qed-.
-lemma drops_inv_skip2: ∀I,s,des,des2,i. des ▭ i ≡ des2 →
- ∀L1,K2,V2. ⬇*[s, des2] L1 ≡ K2. ⓑ{I} V2 →
- ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 &
- ⬇*[s, des1] K1 ≡ K2 &
- ⬆*[des1] V2 ≡ V1 &
+lemma drops_inv_skip2: ∀I,s,cs,cs2,i. cs ▭ i ≡ cs2 →
+ ∀L1,K2,V2. ⬇*[s, cs2] L1 ≡ K2. ⓑ{I} V2 →
+ ∃∃K1,V1,cs1. cs + 1 ▭ i + 1 ≡ cs1 + 1 &
+ ⬇*[s, cs1] K1 ≡ K2 &
+ ⬆*[cs1] V2 ≡ V1 &
L1 = K1. ⓑ{I} V1.
-#I #s #des #des2 #i #H elim H -des -des2 -i
+#I #s #cs #cs2 #i #H elim H -cs -cs2 -i
[ #i #L1 #K2 #V2 #H
>(drops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, drops_nil/
-| #des #des2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
+| #cs #cs2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
elim (drops_inv_cons … H) -H #L #HL1 #H
elim (drop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ #K #V >minus_plus #HK2 #HV2 #H destruct
- elim (IHcs2 … HL1) -IHcs2 -HL1 #K1 #V1 #des1 #Hcs1 #HK1 #HV1 #X destruct
+ elim (IHcs2 … HL1) -IHcs2 -HL1 #K1 #V1 #cs1 #Hcs1 #HK1 #HV1 #X destruct
@(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7 by lifts_cons, drops_cons/ | skip ]
normalize >plus_minus /3 width=1 by minuss_lt, lt_minus_to_plus/ (**) (* explicit constructors *)
-| #des #des2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
- elim (IHcs2 … H) -IHcs2 -H #K1 #V1 #des1 #Hcs1 #HK1 #HV1 #X destruct
+| #cs #cs2 #l #m #i #Hil #_ #IHcs2 #L1 #K2 #V2 #H
+ elim (IHcs2 … H) -IHcs2 -H #K1 #V1 #cs1 #Hcs1 #HK1 #HV1 #X destruct
/4 width=7 by minuss_ge, ex4_3_intro, le_S_S/
]
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: drop1_skip_bind *)
-lemma drops_skip: ∀L1,L2,s,des. ⬇*[s, des] L1 ≡ L2 → ∀V1,V2. ⬆*[des] V2 ≡ V1 →
- ∀I. ⬇*[s, des + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
-#L1 #L2 #s #des #H elim H -L1 -L2 -des
+lemma drops_skip: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → ∀V1,V2. ⬆*[cs] V2 ≡ V1 →
+ ∀I. ⬇*[s, cs + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
+#L1 #L2 #s #cs #H elim H -L1 -L2 -cs
[ #L #V1 #V2 #HV12 #I
>(lifts_inv_nil … HV12) -HV12 //
-| #L1 #L #L2 #des #l #m #_ #HL2 #IHL #V1 #V2 #H #I
+| #L1 #L #L2 #cs #l #m #_ #HL2 #IHL #V1 #V2 #H #I
elim (lifts_inv_cons … H) -H /3 width=5 by drop_skip, drops_cons/
].
qed.
lemma d1_liftable_liftables: ∀R,s. d_liftable1 R s → d_liftables1 R s.
-#R #s #HR #L #K #des #H elim H -L -K -des
+#R #s #HR #L #K #cs #H elim H -L -K -cs
[ #L #T #U #H #HT <(lifts_inv_nil … H) -H //
-| #L1 #L #L2 #des #l #m #_ #HL2 #IHL #T2 #T1 #H #HLT2
+| #L1 #L #L2 #cs #l #m #_ #HL2 #IHL #T2 #T1 #H #HLT2
elim (lifts_inv_cons … H) -H /3 width=10 by/
]
qed.
lemma d1_liftables_liftables_all: ∀R,s. d_liftables1 R s → d_liftables1_all R s.
-#R #s #HR #L #K #des #HLK #Ts #Us #H elim H -Ts -Us normalize //
+#R #s #HR #L #K #cs #HLK #Ts #Us #H elim H -Ts -Us normalize //
#Ts #Us #T #U #HTU #_ #IHTUs * /3 width=7 by conj/
qed.
(* Properties concerning basic local environment slicing ********************)
-lemma drops_drop_trans: ∀L1,L,des. ⬇*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 →
- ∃∃L0,des0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, des0] L0 ≡ L2 &
- @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
-#L1 #L #des #H elim H -L1 -L -des
+lemma drops_drop_trans: ∀L1,L,cs. ⬇*[Ⓕ, cs] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 →
+ ∃∃L0,cs0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, cs0] L0 ≡ L2 &
+ @⦃i, cs⦄ ≡ i0 & cs ▭ i ≡ cs0.
+#L1 #L #cs #H elim H -L1 -L -cs
[ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/
-| #L1 #L0 #L #des #l #m #_ #HL0 #IHL0 #L2 #i #HL2
+| #L1 #L0 #L #cs #l #m #_ #HL0 #IHL0 #L2 #i #HL2
elim (lt_or_ge i l) #Hil
[ elim (drop_trans_le … HL0 … HL2) -L /2 width=2 by lt_to_le/
#L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by drops_cons, minuss_lt, at_lt, ex4_3_intro/
(* Main properties **********************************************************)
(* Basic_1: was: drop1_trans *)
-theorem drops_trans: ∀L,L2,s,des2. ⬇*[s, des2] L ≡ L2 → ∀L1,des1. ⬇*[s, des1] L1 ≡ L →
- ⬇*[s, des2 @@ des1] L1 ≡ L2.
-#L #L2 #s #des2 #H elim H -L -L2 -des2 /3 width=3 by drops_cons/
+theorem drops_trans: ∀L,L2,s,cs2. ⬇*[s, cs2] L ≡ L2 → ∀L1,cs1. ⬇*[s, cs1] L1 ≡ L →
+ ⬇*[s, cs2 @@ cs1] L1 ≡ L2.
+#L #L2 #s #cs2 #H elim H -L -L2 -cs2 /3 width=3 by drops_cons/
qed-.
∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
R G1 L1 T1
) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=1 by fqup_fwd_fw/
+#R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=1 by fqup_fwd_fw/
qed-.
lemma fqup_wf_ind_eq: ∀R:relation3 …. (
∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2
) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/
+#R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/
qed-.
lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
#L #U @(f2_ind … rfw … L U) -L -U
-#n #IH #L * *
+#x #IH #L * *
[ -IH /3 width=5 by frees_inv_sort, or_intror/
-| #j #Hn #l #i elim (lt_or_eq_or_gt i j) #Hji
- [ -n @or_intror #H elim (lt_refl_false i)
+| #j #Hx #l #i elim (lt_or_eq_or_gt i j) #Hji
+ [ -x @or_intror #H elim (lt_refl_false i)
lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by lt_to_le/
- | -n /2 width=1 by or_introl/
+ | -x /2 width=1 by or_introl/
| elim (ylt_split j l) #Hli
- [ -n @or_intror #H elim (lt_refl_false i)
+ [ -x @or_intror #H elim (lt_refl_false i)
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/
- | -n @or_intror #H elim (lt_refl_false i)
+ | -x @or_intror #H elim (lt_refl_false i)
lapply (frees_inv_lref_free … H ?) -l //
]
]
]
| -IH /3 width=5 by frees_inv_gref, or_intror/
-| #a #I #W #U #Hn #l #i destruct
+| #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 #Hn #l #i destruct
+| #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/
inductive lifts: list2 nat nat → relation term ≝
| lifts_nil : ∀T. lifts (◊) T T
-| lifts_cons: ∀T1,T,T2,des,l,m.
- ⬆[l,m] T1 ≡ T → lifts des T T2 → lifts ({l, m} @ des) T1 T2
+| lifts_cons: ∀T1,T,T2,cs,l,m.
+ ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts ({l, m} @ cs) T1 T2
.
interpretation "generic relocation (term)"
- 'RLiftStar des T1 T2 = (lifts des T1 T2).
+ 'RLiftStar cs T1 T2 = (lifts cs T1 T2).
(* Basic inversion lemmas ***************************************************)
-fact lifts_inv_nil_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → des = ◊ → T1 = T2.
-#T1 #T2 #des * -T1 -T2 -des //
-#T1 #T #T2 #l #m #des #_ #_ #H destruct
+fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = ◊ → T1 = T2.
+#T1 #T2 #cs * -T1 -T2 -cs //
+#T1 #T #T2 #l #m #cs #_ #_ #H destruct
qed-.
lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2.
/2 width=3 by lifts_inv_nil_aux/ qed-.
-fact lifts_inv_cons_aux: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 →
- ∀l,m,tl. des = {l, m} @ tl →
+fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 →
+ ∀l,m,tl. cs = {l, m} @ tl →
∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[tl] T ≡ T2.
-#T1 #T2 #des * -T1 -T2 -des
+#T1 #T2 #cs * -T1 -T2 -cs
[ #T #l #m #tl #H destruct
-| #T1 #T #T2 #des #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
+| #T1 #T #T2 #cs #l #m #HT1 #HT2 #l0 #m0 #tl #H destruct
/2 width=3 by ex2_intro/
qed-.
-lemma lifts_inv_cons: ∀T1,T2,l,m,des. ⬆*[{l, m} @ des] T1 ≡ T2 →
- ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[des] T ≡ T2.
+lemma lifts_inv_cons: ∀T1,T2,l,m,cs. ⬆*[{l, m} @ cs] T1 ≡ T2 →
+ ∃∃T. ⬆[l, m] T1 ≡ T & ⬆*[cs] T ≡ T2.
/2 width=3 by lifts_inv_cons_aux/ qed-.
(* Basic_1: was: lift1_sort *)
-lemma lifts_inv_sort1: ∀T2,k,des. ⬆*[des] ⋆k ≡ T2 → T2 = ⋆k.
-#T2 #k #des elim des -des
+lemma lifts_inv_sort1: ∀T2,k,cs. ⬆*[cs] ⋆k ≡ T2 → T2 = ⋆k.
+#T2 #k #cs elim cs -cs
[ #H <(lifts_inv_nil … H) -H //
-| #l #m #des #IH #H
+| #l #m #cs #IH #H
elim (lifts_inv_cons … H) -H #X #H
>(lift_inv_sort1 … H) -H /2 width=1 by/
]
qed-.
(* Basic_1: was: lift1_lref *)
-lemma lifts_inv_lref1: ∀T2,des,i1. ⬆*[des] #i1 ≡ T2 →
- ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
-#T2 #des elim des -des
+lemma lifts_inv_lref1: ∀T2,cs,i1. ⬆*[cs] #i1 ≡ T2 →
+ ∃∃i2. @⦃i1, cs⦄ ≡ i2 & T2 = #i2.
+#T2 #cs elim cs -cs
[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/
-| #l #m #des #IH #i1 #H
+| #l #m #cs #IH #i1 #H
elim (lifts_inv_cons … H) -H #X #H1 #H2
elim (lift_inv_lref1 … H1) -H1 * #Hli1 #H destruct
elim (IH … H2) -IH -H2 /3 width=3 by at_lt, at_ge, ex2_intro/
]
qed-.
-lemma lifts_inv_gref1: ∀T2,p,des. ⬆*[des] §p ≡ T2 → T2 = §p.
-#T2 #p #des elim des -des
+lemma lifts_inv_gref1: ∀T2,p,cs. ⬆*[cs] §p ≡ T2 → T2 = §p.
+#T2 #p #cs elim cs -cs
[ #H <(lifts_inv_nil … H) -H //
-| #l #m #des #IH #H
+| #l #m #cs #IH #H
elim (lifts_inv_cons … H) -H #X #H
>(lift_inv_gref1 … H) -H /2 width=1 by/
]
qed-.
(* Basic_1: was: lift1_bind *)
-lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⬆*[des] ⓑ{a,I} V1. U1 ≡ T2 →
- ∃∃V2,U2. ⬆*[des] V1 ≡ V2 & ⬆*[des + 1] U1 ≡ U2 &
+lemma lifts_inv_bind1: ∀a,I,T2,cs,V1,U1. ⬆*[cs] ⓑ{a,I} V1. U1 ≡ T2 →
+ ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs + 1] U1 ≡ U2 &
T2 = ⓑ{a,I} V2. U2.
-#a #I #T2 #des elim des -des
+#a #I #T2 #cs elim cs -cs
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
-| #l #m #des #IHcs #V1 #U1 #H
+| #l #m #cs #IHcs #V1 #U1 #H
elim (lifts_inv_cons … H) -H #X #H #HT2
elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
elim (IHcs … HT2) -IHcs -HT2 #V2 #U2 #HV2 #HU2 #H destruct
qed-.
(* Basic_1: was: lift1_flat *)
-lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⬆*[des] ⓕ{I} V1. U1 ≡ T2 →
- ∃∃V2,U2. ⬆*[des] V1 ≡ V2 & ⬆*[des] U1 ≡ U2 &
+lemma lifts_inv_flat1: ∀I,T2,cs,V1,U1. ⬆*[cs] ⓕ{I} V1. U1 ≡ T2 →
+ ∃∃V2,U2. ⬆*[cs] V1 ≡ V2 & ⬆*[cs] U1 ≡ U2 &
T2 = ⓕ{I} V2. U2.
-#I #T2 #des elim des -des
+#I #T2 #cs elim cs -cs
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/
-| #l #m #des #IHcs #V1 #U1 #H
+| #l #m #cs #IHcs #V1 #U1 #H
elim (lifts_inv_cons … H) -H #X #H #HT2
elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
elim (IHcs … HT2) -IHcs -HT2 #V2 #U2 #HV2 #HU2 #H destruct
(* Basic forward lemmas *****************************************************)
-lemma lifts_simple_dx: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_dx/
+lemma lifts_simple_dx: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 #cs #H elim H -T1 -T2 -cs /3 width=5 by lift_simple_dx/
qed-.
-lemma lifts_simple_sn: ∀T1,T2,des. ⬆*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_sn/
+lemma lifts_simple_sn: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+#T1 #T2 #cs #H elim H -T1 -T2 -cs /3 width=5 by lift_simple_sn/
qed-.
(* Basic properties *********************************************************)
-lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⬆*[des] V1 ≡ V2 →
- ∀T1. ⬆*[des + 1] T1 ≡ T2 →
- ⬆*[des] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
-#a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+lemma lifts_bind: ∀a,I,T2,V1,V2,cs. ⬆*[cs] V1 ≡ V2 →
+ ∀T1. ⬆*[cs + 1] T1 ≡ T2 →
+ ⬆*[cs] ⓑ{a,I} V1. T1 ≡ ⓑ{a,I} V2. T2.
+#a #I #T2 #V1 #V2 #cs #H elim H -V1 -V2 -cs
[ #V #T1 #H >(lifts_inv_nil … H) -H //
-| #V1 #V #V2 #des #l #m #HV1 #_ #IHV #T1 #H
+| #V1 #V #V2 #cs #l #m #HV1 #_ #IHV #T1 #H
elim (lifts_inv_cons … H) -H /3 width=3 by lift_bind, lifts_cons/
]
qed.
-lemma lifts_flat: ∀I,T2,V1,V2,des. ⬆*[des] V1 ≡ V2 →
- ∀T1. ⬆*[des] T1 ≡ T2 →
- ⬆*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
-#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+lemma lifts_flat: ∀I,T2,V1,V2,cs. ⬆*[cs] V1 ≡ V2 →
+ ∀T1. ⬆*[cs] T1 ≡ T2 →
+ ⬆*[cs] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
+#I #T2 #V1 #V2 #cs #H elim H -V1 -V2 -cs
[ #V #T1 #H >(lifts_inv_nil … H) -H //
-| #V1 #V #V2 #des #l #m #HV1 #_ #IHV #T1 #H
+| #V1 #V #V2 #cs #l #m #HV1 #_ #IHV #T1 #H
elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/
]
qed.
-lemma lifts_total: ∀des,T1. ∃T2. ⬆*[des] T1 ≡ T2.
-#des elim des -des /2 width=2 by lifts_nil, ex_intro/
-#l #m #des #IH #T1 elim (lift_total T1 l m)
+lemma lifts_total: ∀cs,T1. ∃T2. ⬆*[cs] T1 ≡ T2.
+#cs elim cs -cs /2 width=2 by lifts_nil, ex_intro/
+#l #m #cs #IH #T1 elim (lift_total T1 l m)
#T #HT1 elim (IH T) -IH /3 width=4 by lifts_cons, ex_intro/
qed.
(* Properties concerning basic term relocation ******************************)
(* Basic_1: was: lift1_xhg (right to left) *)
-lemma lifts_lift_trans_le: ∀T1,T,des. ⬆*[des] T1 ≡ T → ∀T2. ⬆[0, 1] T ≡ T2 →
- ∃∃T0. ⬆[0, 1] T1 ≡ T0 & ⬆*[des + 1] T0 ≡ T2.
-#T1 #T #des #H elim H -T1 -T -des
-[ /2 width=3/
-| #T1 #T3 #T #des #l #m #HT13 #_ #IHT13 #T2 #HT2
+lemma lifts_lift_trans_le: ∀T1,T,cs. ⬆*[cs] T1 ≡ T → ∀T2. ⬆[0, 1] T ≡ T2 →
+ ∃∃T0. ⬆[0, 1] T1 ≡ T0 & ⬆*[cs + 1] T0 ≡ T2.
+#T1 #T #cs #H elim H -T1 -T -cs
+[ /2 width=3 by lifts_nil, ex2_intro/
+| #T1 #T3 #T #cs #l #m #HT13 #_ #IHT13 #T2 #HT2
elim (IHT13 … HT2) -T #T #HT3 #HT2
- elim (lift_trans_le … HT13 … HT3) -T3 // /3 width=5/
+ elim (lift_trans_le … HT13 … HT3) -T3 /3 width=5 by lifts_cons, ex2_intro/
]
qed-.
(* Basic_1: was: lift1_free (right to left) *)
-lemma lifts_lift_trans: ∀des,i,i0. @⦃i, des⦄ ≡ i0 →
- ∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 →
- ∀T1,T0. ⬆*[des0] T1 ≡ T0 →
+lemma lifts_lift_trans: ∀cs,i,i0. @⦃i, cs⦄ ≡ i0 →
+ ∀cs0. cs + 1 ▭ i + 1 ≡ cs0 + 1 →
+ ∀T1,T0. ⬆*[cs0] T1 ≡ T0 →
∀T2. ⬆[O, i0 + 1] T0 ≡ T2 →
- ∃∃T. ⬆[0, i + 1] T1 ≡ T & ⬆*[des] T ≡ T2.
-#des elim des -des normalize
-[ #i #x #H1 #des0 #H2 #T1 #T0 #HT10 #T2
+ ∃∃T. ⬆[0, i + 1] T1 ≡ T & ⬆*[cs] T ≡ T2.
+#cs elim cs -cs normalize
+[ #i #x #H1 #cs0 #H2 #T1 #T0 #HT10 #T2
<(at_inv_nil … H1) -x #HT02
lapply (minuss_inv_nil1 … H2) -H2 #H
- >(pluss_inv_nil2 … H) in HT10; -des0 #H
- >(lifts_inv_nil … H) -T1 /2 width=3/
-| #l #m #des #IHcs #i #i0 #H1 #des0 #H2 #T1 #T0 #HT10 #T2 #HT02
+ >(pluss_inv_nil2 … H) in HT10; -cs0 #H
+ >(lifts_inv_nil … H) -T1 /2 width=3 by lifts_nil, ex2_intro/
+| #l #m #cs #IHcs #i #i0 #H1 #cs0 #H2 #T1 #T0 #HT10 #T2 #HT02
elim (at_inv_cons … H1) -H1 * #Hil #Hi0
- [ elim (minuss_inv_cons1_lt … H2) -H2 [2: /2 width=1/ ] #des1 #Hcs1 <minus_le_minus_minus_comm // <minus_plus_m_m #H
- elim (pluss_inv_cons2 … H) -H #des2 #H1 #H2 destruct
+ [ elim (minuss_inv_cons1_lt … H2) -H2 [2: /2 width=1 by lt_minus_to_plus/ ] #cs1 #Hcs1 <minus_le_minus_minus_comm // <minus_plus_m_m #H
+ elim (pluss_inv_cons2 … H) -H #cs2 #H1 #H2 destruct
elim (lifts_inv_cons … HT10) -HT10 #T >minus_plus #HT1 #HT0
elim (IHcs … Hi0 … Hcs1 … HT0 … HT02) -IHcs -Hi0 -Hcs1 -T0 #T0 #HT0 #HT02
- elim (lift_trans_le … HT1 … HT0) -T /2 width=1/ #T #HT1 <plus_minus_m_m /2 width=1/ /3 width=5/
+ elim (lift_trans_le … HT1 … HT0) -T /2 width=1 by/ #T #HT1 <plus_minus_m_m /3 width=5 by lifts_cons, ex2_intro/
| >commutative_plus in Hi0; #Hi0
- lapply (minuss_inv_cons1_ge … H2 ?) -H2 [ /2 width=1/ ] <associative_plus #Hcs0
+ lapply (minuss_inv_cons1_ge … H2 ?) -H2 [ /2 width=1
by le_S_S/ ] <associative_plus #Hcs0
elim (IHcs … Hi0 … Hcs0 … HT10 … HT02) -IHcs -Hi0 -Hcs0 -T0 #T0 #HT0 #HT02
- elim (lift_split … HT0 l (i+1)) -HT0 /2 width=1/ /3 width=5/
+ elim (lift_split … HT0 l (i+1)) -HT0 /3 width=5 by lifts_cons, le_S, ex2_intro/
]
]
qed-.
(* Main properties **********************************************************)
(* Basic_1: was: lifts1_xhg (right to left) *)
-lemma liftsv_liftv_trans_le: ∀T1s,Ts,des. ⬆*[des] T1s ≡ Ts →
+lemma liftsv_liftv_trans_le: ∀T1s,Ts,cs. ⬆*[cs] T1s ≡ Ts →
∀T2s:list term. ⬆[0, 1] Ts ≡ T2s →
- ∃∃T0s. ⬆[0, 1] T1s ≡ T0s & ⬆*[des + 1] T0s ≡ T2s.
-#T1s #Ts #des #H elim H -T1s -Ts
+ ∃∃T0s. ⬆[0, 1] T1s ≡ T0s & ⬆*[cs + 1] T0s ≡ T2s.
+#T1s #Ts #cs #H elim H -T1s -Ts
[ #T1s #H
- >(liftv_inv_nil1 … H) -T1s /2 width=3/
+ >(liftv_inv_nil1 … H) -T1s /2 width=3 by liftsv_nil, liftv_nil, ex2_intro/
| #T1s #Ts #T1 #T #HT1 #_ #IHT1s #X #H
elim (liftv_inv_cons1 … H) -H #T2 #T2s #HT2 #HT2s #H destruct
elim (IHT1s … HT2s) -Ts #Ts #HT1s #HT2s
- elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5/
+ elim (lifts_lift_trans_le … HT1 … HT2) -T /3 width=5 by liftsv_cons, liftv_cons, ex2_intro/
]
qed-.
(* Main properties **********************************************************)
(* Basic_1: was: lift1_lift1 (left to right) *)
-theorem lifts_trans: ∀T1,T,des1. ⬆*[des1] T1 ≡ T → ∀T2:term. ∀des2. ⬆*[des2] T ≡ T2 →
- ⬆*[des1 @@ des2] T1 ≡ T2.
-#T1 #T #des1 #H elim H -T1 -T -des1 // /3 width=3/
+theorem lifts_trans: ∀T1,T,cs1. ⬆*[cs1] T1 ≡ T → ∀T2:term. ∀cs2. ⬆*[cs2] T ≡ T2 →
+ ⬆*[cs1 @@ cs2] T1 ≡ T2.
+#T1 #T #cs1 #H elim H -T1 -T -cs1 /3 width=3 by lifts_cons/
qed.
(* GENERIC TERM VECTOR RELOCATION *******************************************)
-inductive liftsv (des:list2 nat nat) : relation (list term) ≝
-| liftsv_nil : liftsv des (◊) (◊)
+inductive liftsv (cs:list2 nat nat) : relation (list term) ≝
+| liftsv_nil : liftsv cs (◊) (◊)
| liftsv_cons: ∀T1s,T2s,T1,T2.
- ⬆*[des] T1 ≡ T2 → liftsv des T1s T2s →
- liftsv des (T1 @ T1s) (T2 @ T2s)
+ ⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s →
+ liftsv cs (T1 @ T1s) (T2 @ T2s)
.
interpretation "generic relocation (vector)"
- 'RLiftStar des T1s T2s = (liftsv des T1s T2s).
+ 'RLiftStar cs T1s T2s = (liftsv cs T1s T2s).
(* Basic inversion lemmas ***************************************************)
(* Basic_1: was: lifts1_flat (left to right) *)
-lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⬆*[des] Ⓐ V1s. U1 ≡ T2 →
- ∃∃V2s,U2. ⬆*[des] V1s ≡ V2s & ⬆*[des] U1 ≡ U2 &
+lemma lifts_inv_applv1: ∀V1s,U1,T2,cs. ⬆*[cs] Ⓐ V1s. U1 ≡ T2 →
+ ∃∃V2s,U2. ⬆*[cs] V1s ≡ V2s & ⬆*[cs] U1 ≡ U2 &
T2 = Ⓐ V2s. U2.
#V1s elim V1s -V1s normalize
-[ #T1 #T2 #des #HT12
+[ #T1 #T2 #cs #HT12
@ex3_2_intro [3,4: // |1,2: skip | // ] (**) (* explicit constructor *)
-| #V1 #V1s #IHV1s #T1 #X #des #H
+| #V1 #V1s #IHV1s #T1 #X #cs #H
elim (lifts_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct
elim (IHV1s … HY) -IHV1s -HY #V2s #T2 #HV12s #HT12 #H destruct
@(ex3_2_intro) [4: // |3: /2 width=2 by liftsv_cons/ |1,2: skip | // ] (**) (* explicit constructor *)
(* Basic properties *********************************************************)
(* Basic_1: was: lifts1_flat (right to left) *)
-lemma lifts_applv: ∀V1s,V2s,des. ⬆*[des] V1s ≡ V2s →
- ∀T1,T2. ⬆*[des] T1 ≡ T2 →
- ⬆*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
-#V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/
+lemma lifts_applv: ∀V1s,V2s,cs. ⬆*[cs] V1s ≡ V2s →
+ ∀T1,T2. ⬆*[cs] T1 ≡ T2 →
+ ⬆*[cs] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
+#V1s #V2s #cs #H elim H -V1s -V2s /3 width=1 by lifts_flat/
qed.
| ∃∃I,K1,K2,V. ⬇[i] L1 ≡ K1.ⓑ{I}V &
⬇[i] L2 ≡ K2.ⓑ{I}V &
K1 ≡[V, yinj 0] K2 & l ≤ yinj i.
-#L1 #L2 #l #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/
+#L1 #L2 #l #i #H elim (llpx_sn_fwd_lref … H) /2 width=1 by or3_intro0, or3_intro1/
* /3 width=7 by or3_intro2, ex4_4_intro/
qed-.
lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,l. llpx_sn R l T L L.
#R #HR #T #L @(f2_ind … rfw … L T) -L -T
-#n #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
-#i #Hn elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
+#x #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/
+#i #Hx elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/
#HiL #l elim (ylt_split i l) /2 width=1 by llpx_sn_skip/
elim (drop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
qed-.
lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2.
#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/
-#a #I #V1 #T1 #Hn #L2 #HL12
-@llpx_sn_bind /2 width=1/ (**) (* explicit constructor *)
+#x #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/
+#a #I #V1 #T1 #Hx #L2 #HL12
+@llpx_sn_bind /2 width=1 by/ (**) (* explicit constructor *)
@IH -IH // normalize /2 width=1 by eq_f2/
qed-.
theorem llpx_sn_llpx_sn_alt: ∀R,T,L1,L2,l. llpx_sn R l T L1 L2 → llpx_sn_alt R l T L1 L2.
#R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U
-#n #IHn #L1 #U #Hn #L2 #l #H elim (llpx_sn_inv_alt_r … H) -H
+#x #IHx #L1 #U #Hx #L2 #l #H elim (llpx_sn_inv_alt_r … H) -H
#HL12 #IHU @conj //
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #H #HLK1 #HLK2 elim (frees_inv … H) -H
-[ -n #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/
+[ -x #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/
| * #J1 #K10 #W10 #j #Hlj #Hji #HnU #HLK10 #HnW10 destruct
lapply (drop_fwd_drop2 … HLK10) #H
lapply (drop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK10
elim (drop_O1_lt (Ⓕ) L2 j) [2: <HL12 /2 width=5 by drop_fwd_length_lt2/ ] #J2 #K20 #W20 #HLK20
lapply (drop_fwd_drop2 … HLK20) #H
lapply (drop_conf_ge … H … HLK2 ?) -H /2 width=1 by lt_to_le/ <minus_plus #HK20
- elim (IHn K10 W10 … K20 0) -IHn -HL12 /3 width=6 by drop_fwd_rfw/
+ elim (IHx K10 W10 … K20 0) -IHx -HL12 /3 width=6 by drop_fwd_rfw/
elim (IHU … HnU HLK10 HLK20) -IHU -HnU -HLK10 -HLK20 //
]
qed.
theorem llpx_sn_alt_inv_llpx_sn: ∀R,T,L1,L2,l. llpx_sn_alt R l T L1 L2 → llpx_sn R l T L1 L2.
#R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U
-#n #IHn #L1 #U #Hn #L2 #l * #HL12 #IHU @llpx_sn_intro_alt_r //
+#x #IHx #L1 #U #Hx #L2 #l * #HL12 #IHU @llpx_sn_intro_alt_r //
#I1 #I2 #K1 #K2 #V1 #V2 #i #Hli #HnU #HLK1 #HLK2 destruct
elim (IHU … HLK1 HLK2) /3 width=2 by frees_eq/
-#H #HV12 @and3_intro // @IHn -IHn /3 width=6 by drop_fwd_rfw/
+#H #HV12 @and3_intro // @IHx -IHx /3 width=6 by drop_fwd_rfw/
lapply (drop_fwd_drop2 … HLK1) #H1
lapply (drop_fwd_drop2 … HLK2) -HLK2 #H2
@conj [ @(drop_fwd_length_eq1 … H1 H2) // ] -HL12
(* Main inversion lemmas ****************************************************)
theorem llpx_sn_alt_r_inv_lpx_sn: ∀R,T,L1,L2,l. llpx_sn_alt_r R l T L1 L2 → llpx_sn R l T L1 L2.
-#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * *
+#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #x #IH #L1 * *
[1,3: /3 width=4 by llpx_sn_alt_r_fwd_length, llpx_sn_gref, llpx_sn_sort/
-| #i #Hn #L2 #l #H lapply (llpx_sn_alt_r_fwd_length … H)
+| #i #Hx #L2 #l #H lapply (llpx_sn_alt_r_fwd_length … H)
#HL12 elim (llpx_sn_alt_r_fwd_lref … H) -H
[ * /2 width=1 by llpx_sn_free/
| /2 width=1 by llpx_sn_skip/
| * /4 width=9 by llpx_sn_lref, drop_fwd_rfw/
]
-| #a #I #V #T #Hn #L2 #l #H elim (llpx_sn_alt_r_inv_bind … H) -H
+| #a #I #V #T #Hx #L2 #l #H elim (llpx_sn_alt_r_inv_bind … H) -H
/3 width=1 by llpx_sn_bind/
-| #I #V #T #Hn #L2 #l #H elim (llpx_sn_alt_r_inv_flat … H) -H
+| #I #V #T #Hx #L2 #l #H elim (llpx_sn_alt_r_inv_flat … H) -H
/3 width=1 by llpx_sn_flat/
]
qed-.
lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) →
∀T,L1,L2,l. Decidable (llpx_sn R l T L1 L2).
#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 * *
-[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/
-| #i #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|))
+#x #IH #L1 * *
+[ #k #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/
+| #i #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|))
[ #HL12 #l elim (ylt_split i l) /3 width=1 by llpx_sn_skip, or_introl/
#Hli elim (lt_or_ge i (|L1|)) #HiL1
elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, llpx_sn_free/
lapply (drop_mono … HLY2 … HLK2) -HLY2 -HLK2
#H #H0 destruct /2 width=1 by/
]
-| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_gref/
-| #a #I #V #T #Hn #L2 #l destruct
+| #p #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_gref/
+| #a #I #V #T #Hx #L2 #l destruct
elim (IH L1 V … L2 l) /2 width=1 by/
elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (⫯l)) -IH /3 width=1 by or_introl, llpx_sn_bind/
#H1 #H2 @or_intror
#H elim (llpx_sn_inv_bind … H) -H /2 width=1 by/
-| #I #V #T #Hn #L2 #l destruct
+| #I #V #T #Hx #L2 #l destruct
elim (IH L1 V … L2 l) /2 width=1 by/
elim (IH L1 T … L2 l) -IH /3 width=1 by or_introl, llpx_sn_flat/
#H1 #H2 @or_intror
#H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/
]
--n /4 width=4 by llpx_sn_fwd_length, or_intror/
+-x /4 width=4 by llpx_sn_fwd_length, or_intror/
qed-.
(* Properties on relocation *************************************************)
lemma lpx_sn_llpx_sn: ∀R. (∀L. reflexive … (R L)) →
∀T,L1,L2,l. lpx_sn R L1 L2 → llpx_sn R l T L1 L2.
#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T
-#n #IH #L1 * *
+#x #IH #L1 * *
[ -HR -IH /4 width=2 by lpx_sn_fwd_length, llpx_sn_sort/
| -HR #i elim (lt_or_ge i (|L1|))
[2: -IH /4 width=4 by lpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux/ ]
- #Hi #Hn #L2 #l elim (ylt_split i l)
- [ -n /3 width=2 by llpx_sn_skip, lpx_sn_fwd_length/ ]
+ #Hi #Hx #L2 #l elim (ylt_split i l)
+ [ -x /3 width=2 by llpx_sn_skip, lpx_sn_fwd_length/ ]
#Hli #HL12 elim (drop_O1_lt (Ⓕ) L1 i) //
#I #K1 #V1 #HLK1 elim (lpx_sn_drop_conf … HL12 … HLK1) -HL12
/4 width=9 by llpx_sn_lref, drop_fwd_rfw/
inductive at: list2 nat nat → relation nat ≝
| at_nil: ∀i. at (◊) i i
-| at_lt : ∀des,l,m,i1,i2. i1 < l →
- at des i1 i2 → at ({l, m} @ des) i1 i2
-| at_ge : ∀des,l,m,i1,i2. l ≤ i1 →
- at des (i1 + m) i2 → at ({l, m} @ des) i1 i2
+| at_lt : ∀cs,l,m,i1,i2. i1 < l →
+ at cs i1 i2 → at ({l, m} @ cs) i1 i2
+| at_ge : ∀cs,l,m,i1,i2. l ≤ i1 →
+ at cs (i1 + m) i2 → at ({l, m} @ cs) i1 i2
.
interpretation "application (multiple relocation with pairs)"
- 'RAt i1 des i2 = (at des i1 i2).
+ 'RAt i1 cs i2 = (at cs i1 i2).
(* Basic inversion lemmas ***************************************************)
-fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ◊ → i1 = i2.
-#des #i1 #i2 * -des -i1 -i2
+fact at_inv_nil_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = i2.
+#cs #i1 #i2 * -cs -i1 -i2
[ //
-| #des #l #m #i1 #i2 #_ #_ #H destruct
-| #des #l #m #i1 #i2 #_ #_ #H destruct
+| #cs #l #m #i1 #i2 #_ #_ #H destruct
+| #cs #l #m #i1 #i2 #_ #_ #H destruct
]
qed-.
lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = i2.
/2 width=3 by at_inv_nil_aux/ qed-.
-fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
- ∀l,m,des0. des = {l, m} @ des0 →
- i1 < l ∧ @⦃i1, des0⦄ ≡ i2 ∨
- l ≤ i1 ∧ @⦃i1 + m, des0⦄ ≡ i2.
-#des #i1 #i2 * -des -i1 -i2
-[ #i #l #m #des #H destruct
-| #des1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #des2 #H destruct /3 width=1 by or_introl, conj/
-| #des1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #des2 #H destruct /3 width=1 by or_intror, conj/
+fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 →
+ ∀l,m,cs0. cs = {l, m} @ cs0 →
+ i1 < l ∧ @⦃i1, cs0⦄ ≡ i2 ∨
+ l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≡ i2.
+#cs #i1 #i2 * -cs -i1 -i2
+[ #i #l #m #cs #H destruct
+| #cs1 #l1 #m1 #i1 #i2 #Hil1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
+| #cs1 #l1 #m1 #i1 #i2 #Hli1 #Hi12 #l2 #m2 #cs2 #H destruct /3 width=1 by or_intror, conj/
]
qed-.
-lemma at_inv_cons: ∀des,l,m,i1,i2. @⦃i1, {l, m} @ des⦄ ≡ i2 →
- i1 < l ∧ @⦃i1, des⦄ ≡ i2 ∨
- l ≤ i1 ∧ @⦃i1 + m, des⦄ ≡ i2.
+lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+ i1 < l ∧ @⦃i1, cs⦄ ≡ i2 ∨
+ l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≡ i2.
/2 width=3 by at_inv_cons_aux/ qed-.
-lemma at_inv_cons_lt: ∀des,l,m,i1,i2. @⦃i1, {l, m} @ des⦄ ≡ i2 →
- i1 < l → @⦃i1, des⦄ ≡ i2.
-#des #l #m #i1 #m2 #H
+lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+ i1 < l → @⦃i1, cs⦄ ≡ i2.
+#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l
lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl
elim (lt_refl_false … Hl)
qed-.
-lemma at_inv_cons_ge: ∀des,l,m,i1,i2. @⦃i1, {l, m} @ des⦄ ≡ i2 →
- l ≤ i1 → @⦃i1 + m, des⦄ ≡ i2.
-#des #l #m #i1 #m2 #H
+lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} @ cs⦄ ≡ i2 →
+ l ≤ i1 → @⦃i1 + m, cs⦄ ≡ i2.
+#cs #l #m #i1 #m2 #H
elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1
lapply (le_to_lt_to_lt … Hli1 Hi1l) -Hli1 -Hi1l #Hl
elim (lt_refl_false … Hl)
inductive minuss: nat → relation (list2 nat nat) ≝
| minuss_nil: ∀i. minuss i (◊) (◊)
-| minuss_lt : ∀des1,des2,l,m,i. i < l → minuss i des1 des2 →
- minuss i ({l, m} @ des1) ({l - i, m} @ des2)
-| minuss_ge : ∀des1,des2,l,m,i. l ≤ i → minuss (m + i) des1 des2 →
- minuss i ({l, m} @ des1) des2
+| minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 →
+ minuss i ({l, m} @ cs1) ({l - i, m} @ cs2)
+| minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 →
+ minuss i ({l, m} @ cs1) cs2
.
interpretation "minus (multiple relocation with pairs)"
- 'RMinus des1 i des2 = (minuss i des1 des2).
+ 'RMinus cs1 i cs2 = (minuss i cs1 cs2).
(* Basic inversion lemmas ***************************************************)
-fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ◊ → des2 = ◊.
-#des1 #des2 #i * -des1 -des2 -i
+fact minuss_inv_nil1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 → cs1 = ◊ → cs2 = ◊.
+#cs1 #cs2 #i * -cs1 -cs2 -i
[ //
-| #des1 #des2 #l #m #i #_ #_ #H destruct
-| #des1 #des2 #l #m #i #_ #_ #H destruct
+| #cs1 #cs2 #l #m #i #_ #_ #H destruct
+| #cs1 #cs2 #l #m #i #_ #_ #H destruct
]
qed-.
-lemma minuss_inv_nil1: ∀des2,i. ◊ ▭ i ≡ des2 → des2 = ◊.
+lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≡ cs2 → cs2 = ◊.
/2 width=4 by minuss_inv_nil1_aux/ qed-.
-fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
- ∀l,m,des. des1 = {l, m} @ des →
- l ≤ i ∧ des ▭ m + i ≡ des2 ∨
- ∃∃des0. i < l & des ▭ i ≡ des0 &
- des2 = {l - i, m} @ des0.
-#des1 #des2 #i * -des1 -des2 -i
-[ #i #l #m #des #H destruct
-| #des1 #des #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/
-| #des1 #des #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #des2 #H destruct /3 width=1 by or_introl, conj/
+fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≡ cs2 →
+ ∀l,m,cs. cs1 = {l, m} @ cs →
+ l ≤ i ∧ cs ▭ m + i ≡ cs2 ∨
+ ∃∃cs0. i < l & cs ▭ i ≡ cs0 &
+ cs2 = {l - i, m} @ cs0.
+#cs1 #cs2 #i * -cs1 -cs2 -i
+[ #i #l #m #cs #H destruct
+| #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/
+| #cs1 #cs #l1 #m1 #i1 #Hli1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=1 by or_introl, conj/
]
qed-.
-lemma minuss_inv_cons1: ∀des1,des2,l,m,i. {l, m} @ des1 ▭ i ≡ des2 →
- l ≤ i ∧ des1 ▭ m + i ≡ des2 ∨
- ∃∃des. i < l & des1 ▭ i ≡ des &
- des2 = {l - i, m} @ des.
+lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
+ l ≤ i ∧ cs1 ▭ m + i ≡ cs2 ∨
+ ∃∃cs. i < l & cs1 ▭ i ≡ cs &
+ cs2 = {l - i, m} @ cs.
/2 width=3 by minuss_inv_cons1_aux/ qed-.
-lemma minuss_inv_cons1_ge: ∀des1,des2,l,m,i. {l, m} @ des1 ▭ i ≡ des2 →
- l ≤ i → des1 ▭ m + i ≡ des2.
-#des1 #des2 #l #m #i #H
-elim (minuss_inv_cons1 … H) -H * // #des #Hil #_ #_ #Hli
+lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
+ l ≤ i → cs1 ▭ m + i ≡ cs2.
+#cs1 #cs2 #l #m #i #H
+elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli
lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli #Hi
elim (lt_refl_false … Hi)
qed-.
-lemma minuss_inv_cons1_lt: ∀des1,des2,l,m,i. {l, m} @ des1 ▭ i ≡ des2 →
+lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} @ cs1 ▭ i ≡ cs2 →
i < l →
- ∃∃des. des1 ▭ i ≡ des & des2 = {l - i, m} @ des.
-#des1 #des2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
+ ∃∃cs. cs1 ▭ i ≡ cs & cs2 = {l - i, m} @ cs.
+#cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
#Hli #_ #Hil lapply (lt_to_le_to_lt … Hil Hli) -Hil -Hli
#Hi elim (lt_refl_false … Hi)
qed-.
(* Main properties **********************************************************)
-theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2.
-#des #i #i1 #H elim H -des -i -i1
+theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
+#cs #i #i1 #H elim H -cs -i -i1
[ #i #x #H <(at_inv_nil … H) -x //
-| #des #l #m #i #i1 #Hil #_ #IHi1 #x #H
+| #cs #l #m #i #i1 #Hil #_ #IHi1 #x #H
lapply (at_inv_cons_lt … H Hil) -H -Hil /2 width=1 by/
-| #des #l #m #i #i1 #Hli #_ #IHi1 #x #H
+| #cs #l #m #i #i1 #Hli #_ #IHi1 #x #H
lapply (at_inv_cons_ge … H Hli) -H -Hli /2 width=1 by/
]
qed-.
(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
-let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
+let rec pluss (cs:list2 nat nat) (i:nat) on cs ≝ match cs with
[ nil2 ⇒ ◊
-| cons2 l m des ⇒ {l + i, m} @ pluss des i
+| cons2 l m cs ⇒ {l + i, m} @ pluss cs i
].
interpretation "plus (multiple relocation with pairs)"
(* Basic inversion lemmas ***************************************************)
-lemma pluss_inv_nil2: ∀i,des. des + i = ◊ → des = ◊.
+lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊.
#i * // normalize
-#l #m #des #H destruct
+#l #m #cs #H destruct
qed.
-lemma pluss_inv_cons2: ∀i,l,m,des2,des. des + i = {l, m} @ des2 →
- ∃∃des1. des1 + i = des2 & des = {l - i, m} @ des1.
-#i #l #m #des2 * normalize
+lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} @ cs2 →
+ ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} @ cs1.
+#i #l #m #cs2 * normalize
[ #H destruct
-| #l1 #m1 #des1 #H destruct /2 width=3/
+| #l1 #m1 #cs1 #H destruct /2 width=3 by ex2_intro/
]
qed-.
lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓐV.T⦄ →
∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ & 𝐒⦃T⦄.
-#G #L #V #T #HVT @and3_intro /3 width=1/
+#G #L #V #T #HVT @and3_intro /3 width=1 by crr_appl_sn, crr_appl_dx/
generalize in match HVT; -HVT elim T -T //
* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/
qed-.
[ #L #K #V #i #HLK #H
elim (cnr_inv_delta … HLK H)
| #L #V #T #_ #IHV #H
- elim (cnr_inv_appl … H) -H /2 width=1/
+ elim (cnr_inv_appl … H) -H /2 width=1 by/
| #L #V #T #_ #IHT #H
- elim (cnr_inv_appl … H) -H /2 width=1/
+ elim (cnr_inv_appl … H) -H /2 width=1 by/
| #I #L #V #T * #H1 #H2 destruct
[ elim (cnr_inv_zeta … H2)
| elim (cnr_inv_eps … H2)
]
|5,6: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
- [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1/
- |*: elim (cnr_inv_abst … H2) -H2 /2 width=1/
+ [1,3: elim (cnr_inv_abbr … H2) -H2 /2 width=1 by/
+ |*: elim (cnr_inv_abst … H2) -H2 /2 width=1 by/
]
| #a #L #V #W #T #H
elim (cnr_inv_appl … H) -H #_ #_ #H
U = ⓐV2. T2.
#G #L #V1 #T1 #U #H #HT1
elim (cpr_inv_appl1 … H) -H *
-[ /2 width=5/
+[ /2 width=5 by ex3_2_intro/
| #a #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H #_ destruct
elim (simple_inv_bind … HT1)
| #a #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
elim (cir_inv_ri2 … H) /2 width=1 by or_introl/
| #G #L #V1 #T1 #T2 #_ #_ #H
- elim (cir_inv_ri2 … H) /2 width=1/
+ elim (cir_inv_ri2 … H) /2 width=1 by/
| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
elim (cir_inv_appl … H) -H #_ #_ #H
elim (simple_inv_bind … H)
elim (IHU12 … HLK … HTU1) -U1 -HLK /3 width=5 by cpx_flat, lift_flat, ex2_intro/
| #G #L #V #U1 #U #U2 #_ #HU2 #IHU1 #K #s #l #m #HLK #X #H
elim (lift_inv_bind2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
- elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1/ -L -U1 #T #HTU #HT1
+ elim (IHU1 (K.ⓓW1) s … HTU1) /2 width=1 by drop_skip/ -L -U1 #T #HTU #HT1
elim (lift_div_le … HU2 … HTU) -U /3 width=5 by cpx_zeta, ex2_intro/
| #G #L #V #U1 #U2 #_ #IHU12 #K #s #l #m #HLK #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HWV1 #HTU1 #H destruct
#a #G #L0 #V0 #W0 #T0 #IH #V1 #HV01 #W1 #HW01 #T1 #HT01
#V2 #HV02 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
-elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2
+elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2
elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/
lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/
>(aaa_inv_sort … H) -H //
| #I1 #G #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2
- lapply (drop_mono … HLK1 … HLK2) -L #H destruct /2 width=1/
+ lapply (drop_mono … HLK1 … HLK2) -L #H destruct /2 width=1 by/
| #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
- elim (aaa_inv_abbr … H) -H /2 width=1/
+ elim (aaa_inv_abbr … H) -H /2 width=1 by/
| #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
- elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1/
+ elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1 by eq_f2/
| #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_appl … H) -H #B2 #_ #HA2
lapply (IHA1 … HA2) -L #H destruct //
| #G #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
- elim (aaa_inv_cast … H) -H /2 width=1/
+ elim (aaa_inv_cast … H) -H /2 width=1 by/
]
qed-.
(* Properties concerning generic relocation *********************************)
-lemma aaa_lifts: ∀G,L1,L2,T2,A,s,des. ⬇*[s, des] L2 ≡ L1 → ∀T1. ⬆*[des] T1 ≡ T2 →
+lemma aaa_lifts: ∀G,L1,L2,T2,A,s,cs. ⬇*[s, cs] L2 ≡ L1 → ∀T1. ⬆*[cs] T1 ≡ T2 →
⦃G, L1⦄ ⊢ T1 ⁝ A → ⦃G, L2⦄ ⊢ T2 ⁝ A.
-#G #L1 #L2 #T2 #A #s #des #H elim H -L1 -L2 -des
+#G #L1 #L2 #T2 #A #s #cs #H elim H -L1 -L2 -cs
[ #L #T1 #H #HT1
<(lifts_inv_nil … H) -H //
-| #L1 #L #L2 #des #l #m #_ #HL2 #IHL1 #T1 #H #HT1
+| #L1 #L #L2 #cs #l #m #_ #HL2 #IHL1 #T1 #H #HT1
elim (lifts_inv_cons … H) -H /3 width=10 by aaa_lift/
]
qed.
>(deg_mono … Hkd2 … Hkd1) -h -k -d2 //
| #G #L #K #V #i #d1 #HLK #_ #IHV #d2 #H
elim (da_inv_lref … H) -H * #K0 #V0 [| #d0 ] #HLK0 #HV0 [| #Hd0 ]
- lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /2 width=1/
+ lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /2 width=1 by/
| #G #L #K #W #i #d1 #HLK #_ #IHW #d2 #H
elim (da_inv_lref … H) -H * #K0 #W0 [| #d0 ] #HLK0 #HW0 [| #Hd0 ]
- lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /3 width=1/
+ lapply (drop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct /3 width=1 by eq_f/
| #a #I #G #L #V #T #d1 #_ #IHT #d2 #H
- lapply (da_inv_bind … H) -H /2 width=1/
+ lapply (da_inv_bind … H) -H /2 width=1 by/
| #I #G #L #V #T #d1 #_ #IHT #d2 #H
- lapply (da_inv_flat … H) -H /2 width=1/
+ lapply (da_inv_flat … H) -H /2 width=1 by/
]
qed-.
[ #X #H >(lsuba_inv_atom1 … H) -H //
| #I #L1 #L #Y #HL1 #IHL1 #X #H
elim (lsuba_inv_pair1 … H) -H * #L2
- [ #HL2 #H destruct /3 width=1/
+ [ #HL2 #H destruct /3 width=1 by lsuba_pair/
| #W #V #A #HV #HW #HL2 #H1 #H2 #H3 destruct
/3 width=3 by lsuba_beta, lsuba_aaa_trans/
]
lemma lsubd_da_trans: ∀h,g,G,L2,T,d. ⦃G, L2⦄ ⊢ T ▪[h, g] d →
∀L1. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] d.
#h #g #G #L2 #T #d #H elim H -G -L2 -T -d
-[ /2 width=1/
+[ /2 width=1 by da_sort/
| #G #L2 #K2 #V #i #d #HLK2 #_ #IHV #L1 #HL12
elim (lsubd_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
elim (lsubd_inv_pair2 … H) -H * #K1 [ | -IHV -HLK1 ]
- [ #HK12 #H destruct /3 width=4/
+ [ #HK12 #H destruct /3 width=4 by da_ldef/
| #W #d0 #_ #_ #_ #H destruct
]
| #G #L2 #K2 #W #i #d #HLK2 #HW #IHW #L1 #HL12
elim (lsubd_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
elim (lsubd_inv_pair2 … H) -H * #K1 [ -HW | -IHW ]
- [ #HK12 #H destruct /3 width=4/
+ [ #HK12 #H destruct /3 width=4 by da_ldec/
| #V #d0 #HV #H0W #_ #_ #H destruct
- lapply (da_mono … H0W … HW) -H0W -HW #H destruct /3 width=7/
+ lapply (da_mono … H0W … HW) -H0W -HW #H destruct /3 width=7 by da_ldef, da_flat/
]
-| /4 width=1/
-| /3 width=1/
+| /4 width=1 by lsubd_pair, da_bind/
+| /3 width=1 by da_flat/
]
qed-.
lemma lsubd_da_conf: ∀h,g,G,L1,T,d. ⦃G, L1⦄ ⊢ T ▪[h, g] d →
∀L2. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] d.
#h #g #G #L1 #T #d #H elim H -G -L1 -T -d
-[ /2 width=1/
+[ /2 width=1 by da_sort/
| #G #L1 #K1 #V #i #d #HLK1 #HV #IHV #L2 #HL12
elim (lsubd_drop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
elim (lsubd_inv_pair1 … H) -H * #K2 [ -HV | -IHV ]
- [ #HK12 #H destruct /3 width=4/
+ [ #HK12 #H destruct /3 width=4 by da_ldef/
| #W0 #V0 #d0 #HV0 #HW0 #_ #_ #H1 #H2 destruct
lapply (da_inv_flat … HV) -HV #H0V0
- lapply (da_mono … H0V0 … HV0) -H0V0 -HV0 #H destruct /2 width=4/
+ lapply (da_mono … H0V0 … HV0) -H0V0 -HV0 #H destruct /2 width=4 by da_ldec/
]
| #G #L1 #K1 #W #i #d #HLK1 #HW #IHW #L2 #HL12
elim (lsubd_drop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
elim (lsubd_inv_pair1 … H) -H * #K2 [ -HW | -IHW ]
- [ #HK12 #H destruct /3 width=4/
+ [ #HK12 #H destruct /3 width=4 by da_ldec/
| #W0 #V0 #d0 #HV0 #HW0 #_ #H destruct
]
-| /4 width=1/
-| /3 width=1/
+| /4 width=1 by lsubd_pair, da_bind/
+| /3 width=1 by da_flat/
]
qed-.
[ #X #H >(lsubd_inv_atom1 … H) -H //
| #I #L1 #L #Y #HL1 #IHL1 #X #H
elim (lsubd_inv_pair1 … H) -H * #L2
- [ #HL2 #H destruct /3 width=1/
+ [ #HL2 #H destruct /3 width=1 by lsubd_pair/
| #W #V #d #HV #HW #HL2 #H1 #H2 #H3 destruct
/3 width=3 by lsubd_beta, lsubd_da_trans/
]
∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → R G2 L2 T2) →
R G1 L1 T1
) → ∀G1,L1,T1. R G1 L1 T1.
-#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=1 by fqu_fwd_fw/
+#R #HR @(f3_ind … fw) #x #IHx #G1 #L1 #T1 #H destruct /4 width=1 by fqu_fwd_fw/
qed-.
#m #G1 elim G1 -G1 /3 width=2 by gget_gt, ex_intro/
#I #V #G1 * #G2 #HG12
elim (lt_or_eq_or_gt m (|G1|)) #Hm
-[ /3 width=2/
+[ /3 width=2 by gget_lt, ex_intro/
| destruct /3 width=2 by gget_eq, ex_intro/
| @ex_intro [2: @gget_gt normalize /2 width=1 by/ | skip ] (**) (* explicit constructor *)
]
| #G #Hm #G2 #H
>(gget_inv_eq … H Hm) -H -Hm //
| #I #G #G1 #V #Hm #_ #IHG1 #G2 #H
- lapply (gget_inv_lt … H Hm) -H -Hm /2 width=1/
+ lapply (gget_inv_lt … H Hm) -H -Hm /2 width=1 by/
]
qed-.
#G1 #G2 #m
elim (gget_total m G1) #G #HG1
elim (eq_genv_dec G G2) #HG2
-[ destruct /2 width=1/
+[ destruct /2 width=1 by or_introl/
| @or_intror #HG12
- lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/
+ lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1 by/
]
qed-.
qed.
lemma lift_lref_ge_minus_eq: ∀l,m,i,j. l + m ≤ i → j = i - m → ⬆[l, m] #j ≡ #i.
-/2 width=1/ qed-.
+/2 width=1 by lift_lref_ge_minus/ qed-.
(* Basic_1: was: lift_r *)
lemma lift_refl: ∀T,l. ⬆[l, 0] T ≡ T.
lemma lift_total: ∀T1,l,m. ∃T2. ⬆[l,m] T1 ≡ T2.
#T1 elim T1 -T1
-[ * #i /2 width=2/ #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/
+[ * #i /2 width=2 by lift_sort, lift_gref, ex_intro/
+ #l #m elim (lt_or_ge i l) /3 width=2 by lift_lref_lt, lift_lref_ge, ex_intro/
| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #l #m
elim (IHV1 l m) -IHV1 #V2 #HV12
[ elim (IHT1 (l+1) m) -IHT1 /3 width=2 by lift_bind, ex_intro/
∀l2,m1. l1 ≤ l2 → l2 ≤ l1 + m1 → m1 ≤ m2 →
∃∃T. ⬆[l1, m1] T1 ≡ T & ⬆[l2, m2 - m1] T ≡ T2.
#l1 #m2 #T1 #T2 #H elim H -l1 -m2 -T1 -T2
-[ /3 width=3/
+[ /3 width=3 by lift_sort, ex2_intro/
| #i #l1 #m2 #Hil1 #l2 #m1 #Hl12 #_ #_
lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/
| #i #l1 #m2 #Hil1 #l2 #m1 #_ #Hl21 #Hm12
lapply (transitive_le … (i+m1) Hl21 ?) /2 width=1 by monotonic_le_plus_l/ -Hl21 #Hl21
>(plus_minus_m_m m2 m1 ?) /3 width=3 by lift_lref_ge, ex2_intro/
-| /3 width=3/
+| /3 width=3 by lift_gref, ex2_intro/
| #a #I #V1 #V2 #T1 #T2 #l1 #m2 #_ #_ #IHV #IHT #l2 #m1 #Hl12 #Hl21 #Hm12
elim (IHV … Hl12 Hl21 Hm12) -IHV #V0 #HV0a #HV0b
elim (IHT (l2+1) … ? ? Hm12) /3 width=5 by lift_bind, le_S_S, ex2_intro/
]
| elim (IHV2 l m) -IHV2
[ * #V1 #HV12 elim (IHT2 l m) -IHT2
- [ * #T1 #HT12 /4 width=2/
+ [ * #T1 #HT12 /4 width=2 by lift_flat, ex_intro, or_introl/
| -V1 #HT2 @or_intror * #X #H
elim (lift_inv_flat2 … H) -H /3 width=2 by ex_intro/
]
[ #U2s #H >(liftv_inv_nil1 … H) -H //
| #Ts #U1s #T #U1 #HTU1 #_ #IHTU1s #X #H destruct
elim (liftv_inv_cons1 … H) -H #U2 #U2s #HTU2 #HTU2s #H destruct
- >(lift_mono … HTU1 … HTU2) -T /3 width=1/
+ >(lift_mono … HTU1 … HTU2) -T /3 width=1 by eq_f/
]
qed.
theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 →
confluent2 … (lpx_sn R1) (lpx_sn R2).
-#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH *
-[ #_ #X1 #H1 #X2 #H2 -n
+#R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #x #IH *
+[ #_ #X1 #H1 #X2 #H2 -x
>(lpx_sn_inv_atom1 … H1) -X1
>(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/
-| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct
+| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct
elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct
elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct
elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2
projects / helm.git / commitdiff