(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
definition cpre: relation4 genv lenv term term ≝
- λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ 𝐍⦃T2⦄.
+ λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃T2⦄.
interpretation "context-sensitive parallel evaluation (term)"
'PEval G L T1 T2 = (cpre G L T1 T2).
(* Basic_1: was just: nf2_sn3 *)
lemma csx_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄.
#h #g #G #L #T1 #H @(csx_ind … H) -T1
-#T1 #_ #IHT1
-elim (cnr_dec G L T1) /3 width=3/
-* #T #H1T1 #H2T1
-elim (IHT1 … H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/
+#T1 #_ #IHT1 elim (cnr_dec G L T1) /3 width=3 by ex_intro, conj/
+* #T #H1T1 #H2T1 elim (IHT1 … H2T1) -IHT1 -H2T1 /2 width=2 by cpr_cpx/
+#T2 * /4 width=3 by cprs_strap2, ex_intro, conj/
qed.
(* Basic_1: was: pr3_pr2 *)
lemma cpr_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-/2 width=1/ qed.
+/2 width=1 by inj/ qed.
(* Basic_1: was: pr3_refl *)
lemma cprs_refl: ∀G,L,T. ⦃G, L⦄ ⊢ T ➡* T.
-/2 width=1/ qed.
+/2 width=1 by cpr_cprs/ qed.
lemma cprs_strap1: ∀G,L,T1,T,T2.
⦃G, L⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-normalize /2 width=3/ 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/ 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_pr1 *)
lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2.
-#G #L #T1 #T2 #H @(lsubr_cprs_trans … H) -H //
-qed.
+/2 width=3 by lsubr_cprs_trans/ qed.
lemma cprs_bind_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
#G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
-/3 width=1/ /3 width=3/
-qed.
+/3 width=3 by cprs_strap2, cpr_cprs, cpr_pair_sn, cpr_bind/ qed.
(* Basic_1: was only: pr3_thin_dx *)
lemma cprs_flat_dx: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/
-#T #T2 #_ #HT2 #IHT1
-@(cprs_strap1 … IHT1) -V1 -T1 /2 width=1/
+#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2
+/3 width=5 by cprs_strap1, cpr_flat, cpr_cprs, cpr_pair_sn/
qed.
lemma cprs_flat_sn: ∀I,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 →
⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/
-#V #V2 #_ #HV2 #IHV1
-@(cprs_strap1 … IHV1) -V1 -T1 /2 width=1/
+#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2
+/3 width=3 by cprs_strap1, cpr_cprs, cpr_pair_sn, cpr_flat/
qed.
lemma cprs_zeta: ∀G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
⦃G, L.ⓓV⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2.
-#G #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
+#G #L #V #T1 #T #T2 #HT2 #H @(cprs_ind_dx … H) -T1
+/3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/
qed.
lemma cprs_tau: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2.
-#G #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
+#G #L #T1 #T2 #H @(cprs_ind … H) -T2
+/3 width=3 by cprs_strap1, cpr_cprs, cpr_tau/
qed.
lemma cprs_beta_dx: ∀a,G,L,V1,V2,W1,W2,T1,T2.
⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2 /3 width=1/
-/4 width=7 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_beta/ (**) (* auto too slow without trace *)
+#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2
+/4 width=7 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_beta/
qed.
lemma cprs_theta_dx: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
-/4 width=9 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_theta/ (**) (* auto too slow without trace *)
+#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2
+/4 width=9 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_theta/
qed.
(* Basic inversion lemmas ***************************************************)
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/
-#U2 #U #_ #HU2 * /3 width=3/ *
+#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/ *
-#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3 by cprs_strap1, or_introl/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5 by cprs_strap1, ex3_2_intro, or_intror/
qed-.
(* Basic_1: was: nf2_pr3_unfold *)
-lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → T = U.
+lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → T = U.
#G #L #T #U #H @(cprs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
-lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
+lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
qed-.
(* Basic_1: removed theorems 13:
(* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************)
definition cpxe: ∀h. sd h → relation4 genv lenv term term ≝
- λh,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 ∧ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T2⦄.
+ λh,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 ∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T2⦄.
interpretation "context-sensitive extended parallel evaluation (term)"
'PEval h g G L T1 T2 = (cpxe h g G L T1 T2).
lemma csx_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄.
#h #g #G #L #T1 #H @(csx_ind … H) -T1
-#T1 #_ #IHT1
-elim (cnx_dec h g G L T1) /3 width=3/
-* #T #H1T1 #H2T1
-elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/
+#T1 #_ #IHT1 elim (cnx_dec h g G L T1) /3 width=3 by ex_intro, conj/
+* #T #H1T1 #H2T1 elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1
+#T2 * /4 width=3 by cpxs_strap2, ex_intro, conj/
qed-.
lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/
qed-.
-lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → T = U.
+lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → T = U.
#h #g #G #L #T #U #H @(cpxs_ind_dx … H) -T //
#T0 #T #H1T0 #_ #IHT #H2T0
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/substitution/cpys_cpys.ma".
-include "basic_2/reduction/cpx_cpys.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Main properties **********************************************************)
-
-axiom cpys_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 →
- ∀i. d ≤ i → i ≤ d + e →
- ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[i, d+e-i] T & ⦃G, L⦄ ⊢ T ▶*×[d, i-d] T2.
-
-lemma cpys_tpxs_trans: ∀h,g,G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T →
- ∀T2. ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
-#h #g #G #L #T1 #T #d #e #HT1 #T2 #H @(cpxs_ind … H) -T2
-/3 width=5 by cpxs_strap1, cpys_cpx, lsubr_cpx_trans, cpx_cpxs/
-qed-.
-
-lemma cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
- ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[0, ∞] T & ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2.
-#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
-[ /2 width=3 by ex2_intro/
-| /4 width=3 by cpx_cpxs, cpx_sort, ex2_intro/
-| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 * #V #HV1 #HV2
- elim (lift_total V 0 (i+1)) #W #HVW
- lapply (cpxs_lift … HV2 (⋆) (Ⓣ) … HVW … HVW2)
- [ @ldrop_atom #H destruct | /3 width=7 by cpys_subst_Y2, ex2_intro/ ]
-| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * #T #HT1 #HT2
- @(ex2_intro … (ⓑ{a,I}V1.T))
- [ @cpys_bind //
- | @cpxs_bind //
-
- elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0
- @(ex2_intro … (ⓑ{a,I}V.T0))
- [ @cpys_bind //
- | @(cpxs_trans … (ⓑ{a,I}V.T)) @cpxs_bind // -HT10
-
-
-(*
- lapply (lsuby_cpys_trans … HT10 (L.ⓑ{I}V) ?) -HT10 /2 width=1 by lsuby_succ/ #HT10
-*)
-| #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 *
- /3 width=5 by cpys_flat, cpxs_flat, ex2_intro/
\ No newline at end of file
(* Forward lemmas involving same top term constructor ***********************)
-lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
+lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U.
#h #g #G #L #T #HT #U #H
>(cpxs_inv_cnx1 … H HT) -G -L -T //
qed-.
(* Vector form of forward lemmas involving same top term constructor ********)
(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ →
+lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≃ U.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
#V #Vs #IHVs #U #H
qed-.
(* Basic_1: was just: sn3_nf2 *)
-lemma cnx_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
+lemma cnx_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
/2 width=1 by NF_to_SN/ qed.
lemma csx_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k.
(* Advanced properties ******************************************************)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ →
+lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
#V #Vs #IHV #H
fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
// qed-.
-fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶×[d, e] T1 → e = ∞ →
+axiom cpxs_cpys_conf_lpxs: ∀h,g,G,d,e.
+ ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡*[h, g] T1 →
+ ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*×[d, e] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*×[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡*[h, g] T.
+
+axiom cpxs_conf_lpxs_lpys: ∀h,g,G,d,e.
+ ∀I,L0,V0,T0,T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡*[h, g] T1 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → ∀V2. ⦃G, L0⦄ ⊢ V0 ▶*×[d, e] V2 →
+ ∃∃T. ⦃G, L1.ⓑ{I}V0⦄ ⊢ T1 ▶*×[⫯d, e] T & ⦃G, L0.ⓑ{I}V2⦄ ⊢ T0 ➡*[h, g] T.
+
+
+include "basic_2/reduction/cpx_cpys.ma".
+
+fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶*×[d, e] T1 → e = ∞ →
∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
- ∃∃T2. ⦃G, L2⦄ ⊢ T ▶×[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 &
+ ∃∃T2. ⦃G, L2⦄ ⊢ T ▶*×[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 &
L1 ⋕[T, d] L2 ↔ T1 = T2.
-#h #g #G #L1 #T #T1 #d #e #H elim H -G -L1 -T -T1 -d -e [ * ]
+#h #g #G #L1 #T #T1 #d #e #H @(cpys_ind_alt … H) -G -L1 -T -T1 -d -e [ * ]
[ /5 width=5 by lpxs_fwd_length, lleq_sort, ex3_intro, conj/
| #i #G #L1 elim (lt_or_ge i (|L1|)) [2: /6 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux, ex3_intro, conj/ ]
#Hi #d elim (ylt_split i d) [ /5 width=5 by lpxs_fwd_length, lleq_skip, ex3_intro, conj/ ]
elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
elim (lift_total V2 0 (i+1)) #W2 #HVW2
- @(ex3_intro … W2) /2 width=7 by cpxs_delta, cpy_subst/ -I -K1 -V1 -Hdi
+ @(ex3_intro … W2) /2 width=7 by cpxs_delta, cpys_subst/ -I -K1 -V1 -Hdi
@conj #H [ elim HnL12 // | destruct elim (lift_inv_lref2_be … HVW2) // ]
| /5 width=5 by lpxs_fwd_length, lleq_gref, ex3_intro, conj/
-| #I #G #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #He #L2 #HL12 destruct
+| #I #G #L1 #K1 #V #V1 #T1 #i #d #e #Hdi #Hide #HLK1 #HV1 #HVT1 #_ #He #L2 #HL12 destruct
elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
- elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+ elim (lpxs_inv_pair1 … H) -H #K2 #W #HK12 #HVW #H destruct
+ elim (cpxs_cpys_conf_lpxs … HVW … HV1 … HK12) -HVW -HV1 -HK12 #W1 #HW1 #VW1
+ elim (lift_total W1 0 (i+1)) #U1 #HWU1
lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
- elim (lift_total V2 0 (i+1)) #W2 #HVW2
- @(ex3_intro … W2) /2 width=10 by cpxs_lift, cpy_subst/
+ @(ex3_intro … U1) /2 width=10 by cpxs_lift, cpys_subst/
+| #a #I #G #L #V #V1 #T #T1 #d #e #HV1 #_ #IHV1 #IHT1 #He #L2 #HL12
+ elim (IHV1 … HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V
+ elim (IHT1 … (L2.ⓑ{I}V2)) /4 width=3 by lpxs_cpx_trans, lpxs_pair, cpys_cpx/ -IHT1 -He #T2 #HT2 #HT12 * #H1T #H2T
+ elim (cpxs_conf_lpxs_lpys … HT12 … HL12 … HV1) -HT12 -HL12 -HV1 #T0 #HT20 #HT10
+ @(ex3_intro … (ⓑ{a,I}V2.T0))
+ [ @cpys_bind // @(cpys_trans_eq … T2) /3 width=5 by lsuby_cpys_trans, lsuby_succ/
+ | /2 width=1 by cpxs_bind/
+ | @conj #H destruct
+ [ elim (lleq_inv_bind … H) -H #HV #HT >H1V -H1V //
+ | @lleq_bind /2 width=1/
+
+
+ /3 width=5 by lsuby_cpys_trans, lsuby_succ/
+| #I #G #L #V #V1 #T #T1 #d #e #HV1 #HT1 #IHV1 #IHT1 #He #L2 #HL12
+ elim (IHV1 … HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V
+ elim (IHT1 … HL12) // -IHT1 #T2 #HT2 #HT12 * #H1T #H2T -He -HL12
+ @(ex3_intro … (ⓕ{I}V2.T2)) /2 width=1 by cpxs_flat, cpys_flat/
+ @conj #H destruct [2: /3 width=1 by lleq_flat/ ]
+ elim (lleq_inv_flat … H) -H /3 width=1 by eq_f2/
+]
+
- elim (lleq_dec (#i) L1 L2 d)
-
+ [
+ | @cpxs_bind //
+ @(lpx_cpxs_trans … HT12)
|
]
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐍 break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐍 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'Normal $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ 𝐍 break [ term 46 h , break term 46 g ] break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐍 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'Normal $h $g $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐈 break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐈 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'NotReducible $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ 𝐈 break [ term 46 h , break term 46 g ] break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐈 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'NotReducible $h $g $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐑 break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐑 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'Reducible $G $L $T }.
(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ 𝐑 break [ term 46 h , break term 46 g ] break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐑 break ⦃ term 46 T ⦄ )"
non associative with precedence 45
for @{ 'Reducible $h $g $G $L $T }.
(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
-definition cir: relation3 genv lenv term ≝ λG,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⊥.
+definition cir: relation3 genv lenv term ≝ λG,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⊥.
interpretation "context-sensitive irreducibility (term)"
'NotReducible G L T = (cir G L T).
(* Basic inversion lemmas ***************************************************)
-lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥.
+lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ ➡ 𝐈⦃#i⦄ → ⊥.
/3 width=3 by crr_delta/ qed-.
-lemma cir_inv_ri2: ∀I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈⦃②{I}V.T⦄ → ⊥.
+lemma cir_inv_ri2: ∀I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃②{I}V.T⦄ → ⊥.
/3 width=1 by crr_ri2/ qed-.
-lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
- ⦃G, L⦄ ⊢ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄ →
+ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄.
/4 width=1 by crr_ib2_sn, crr_ib2_dx, conj/ qed-.
-lemma cir_inv_bind: ∀a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ & ib2 a I.
+lemma cir_inv_bind: ∀a,I,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄ & ib2 a I.
#a * [ elim a -a ]
#G #L #V #T #H [ elim H -H /3 width=1 by crr_ri2, or_introl/ ]
elim (cir_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/
qed-.
-lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄.
+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/
generalize in match HVT; -HVT elim T -T //
* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/
qed-.
-lemma cir_inv_flat: ∀I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓕ{I}V.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
+lemma cir_inv_flat: ∀I,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓕ{I}V.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
* #G #L #V #T #H
[ elim (cir_inv_appl … H) -H /2 width=1 by and4_intro/
| elim (cir_inv_ri2 … H) -H //
(* Basic properties *********************************************************)
-lemma cir_sort: ∀G,L,k. ⦃G, L⦄ ⊢ 𝐈⦃⋆k⦄.
+lemma cir_sort: ∀G,L,k. ⦃G, L⦄ ⊢ ➡ 𝐈⦃⋆k⦄.
/2 width=4 by crr_inv_sort/ qed.
-lemma cir_gref: ∀G,L,p. ⦃G, L⦄ ⊢ 𝐈⦃§p⦄.
+lemma cir_gref: ∀G,L,p. ⦃G, L⦄ ⊢ ➡ 𝐈⦃§p⦄.
/2 width=4 by crr_inv_gref/ qed.
-lemma tir_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ 𝐈⦃⓪{I}⦄.
+lemma tir_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃⓪{I}⦄.
/2 width=3 by trr_inv_atom/ qed.
lemma cir_ib2: ∀a,I,G,L,V,T.
- ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
+ ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄.
#a #I #G #L #V #T #HI #HV #HT #H
elim (crr_inv_ib2 … HI H) -HI -H /2 width=1 by/
qed.
-lemma cir_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄.
+lemma cir_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓐV.T⦄.
#G #L #V #T #HV #HT #H1 #H2
elim (crr_inv_appl … H2) -H2 /2 width=1 by/
qed.
(* Advanved properties ******************************************************)
-lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐈⦃T⦄.
/3 width=2 by crr_inv_labst_last/ qed.
-lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄.
/3 width=2 by crr_inv_trr/ qed.
(* Advanced inversion lemmas ************************************************)
-lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄.
/3 width=1/ qed-.
-lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄.
/3 width=1/ qed-.
(* Properties on relocation *************************************************)
-lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈⦃U⦄.
+lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄.
/3 width=8 by crr_inv_lift/ qed.
-lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈⦃T⦄.
+lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄.
/3 width=8 by crr_lift/ qed-.
(* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************)
definition cix: ∀h. sd h → relation3 genv lenv term ≝
- λh,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⊥.
+ λh,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⊥.
interpretation "context-sensitive extended irreducibility (term)"
'NotReducible h g G L T = (cix h g G L T).
(* Basic inversion lemmas ***************************************************)
-lemma cix_inv_sort: ∀h,g,G,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄ → ⊥.
+lemma cix_inv_sort: ∀h,g,G,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃⋆k⦄ → ⊥.
/3 width=2 by crx_sort/ qed-.
-lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥.
+lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃#i⦄ → ⊥.
/3 width=4 by crx_delta/ qed-.
-lemma cix_inv_ri2: ∀h,g,I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃②{I}V.T⦄ → ⊥.
+lemma cix_inv_ri2: ∀h,g,I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃②{I}V.T⦄ → ⊥.
/3 width=1 by crx_ri2/ qed-.
-lemma cix_inv_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ →
- ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄.
+lemma cix_inv_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓑ{a,I}V.T⦄ →
+ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
/4 width=1 by crx_ib2_sn, crx_ib2_dx, conj/ qed-.
-lemma cix_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ & ib2 a I.
+lemma cix_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓑ{a,I}V.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ & ib2 a I.
#h #g #a * [ elim a -a ]
#G #L #V #T #H [ elim H -H /3 width=1 by crx_ri2, or_introl/ ]
elim (cix_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/
qed-.
-lemma cix_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄.
-#h #g #G #L #V #T #HVT @and3_intro /3 width=1/
+lemma cix_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓐV.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ & 𝐒⦃T⦄.
+#h #g #G #L #V #T #HVT @and3_intro /3 width=1 by crx_appl_sn, crx_appl_dx/
generalize in match HVT; -HVT elim T -T //
* // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crx_beta, crx_theta/
qed-.
-lemma cix_inv_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓕ{I}V.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
+lemma cix_inv_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓕ{I}V.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl.
#h #g * #G #L #V #T #H
[ elim (cix_inv_appl … H) -H /2 width=1 by and4_intro/
| elim (cix_inv_ri2 … H) -H //
(* Basic forward lemmas *****************************************************)
-lemma cix_inv_cir: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄.
+lemma cix_inv_cir: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄.
/3 width=1 by crr_crx/ qed-.
(* Basic properties *********************************************************)
-lemma cix_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄.
+lemma cix_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃⋆k⦄.
#h #g #G #L #k #Hk #H elim (crx_inv_sort … H) -L #l #Hkl
lapply (deg_mono … Hk Hkl) -h -k <plus_n_Sm #H destruct
qed.
-lemma tix_lref: ∀h,g,G,i. ⦃G, ⋆⦄ ⊢ 𝐈[h, g]⦃#i⦄.
+lemma tix_lref: ∀h,g,G,i. ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐈⦃#i⦄.
#h #g #G #i #H elim (trx_inv_atom … H) -H #k #l #_ #H destruct
qed.
-lemma cix_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃§p⦄.
+lemma cix_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃§p⦄.
#h #g #G #L #p #H elim (crx_inv_gref … H)
qed.
-lemma cix_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ →
- ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄.
+lemma cix_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ →
+ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓑ{a,I}V.T⦄.
#h #g #a #I #G #L #V #T #HI #HV #HT #H
elim (crx_inv_ib2 … HI H) -HI -H /2 width=1 by/
qed.
-lemma cix_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄.
+lemma cix_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓐV.T⦄.
#h #g #G #L #V #T #HV #HT #H1 #H2
elim (crx_inv_appl … H2) -H2 /2 width=1 by/
qed.
(* Advanced inversion lemmas ************************************************)
-lemma cix_inv_append_sn: ∀h,g,G,L,K,T. ⦃G, K @@ L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄.
-/3 width=1/ qed-.
+lemma cix_inv_append_sn: ∀h,g,G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
+/3 width=1 by crx_append_sn/ qed-.
-lemma cix_inv_tix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, ⋆⦄ ⊢ 𝐈[h, g]⦃T⦄.
-/3 width=1/ qed-.
+lemma cix_inv_tix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
+/3 width=1 by trx_crx/ qed-.
(* Advanced properties ******************************************************)
-lemma cix_lref: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄.
+lemma cix_lref: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃#i⦄.
#h #g #G #L #i #HL #H elim (crx_inv_lref … H) -h #I #K #V #HLK
lapply (ldrop_mono … HLK … HL) -L -i #H destruct
qed.
(* Properties on relocation *************************************************)
-lemma cix_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄.
+lemma cix_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃U⦄.
/3 width=8 by crx_inv_lift/ qed.
-lemma cix_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈[h, g]⦃T⦄.
+lemma cix_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
/3 width=8 by crx_lift/ qed-.
(* Basic inversion lemmas ***************************************************)
-lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄ → ⊥.
+lemma cnr_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄ → ⊥.
#G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
lapply (H W ?) -H [ /3 width=6 by cpr_delta/ ] -HLK #H destruct
elim (lift_inv_lref2_be … HVW) -HVW //
qed-.
-lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍⦃T⦄.
+lemma cnr_inv_abst: ∀a,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}V.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡ 𝐍⦃T⦄.
#a #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnr_inv_abbr: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃-ⓓV.T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍⦃T⦄.
+lemma cnr_inv_abbr: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃-ⓓV.T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡ 𝐍⦃T⦄.
#G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpr_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpr_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
+lemma cnr_inv_zeta: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃+ⓓV.T⦄ → ⊥.
#G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3 by cpr_zeta/ #H destruct
]
qed-.
-lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
+lemma cnr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄ → ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ & 𝐒⦃T⦄.
#G #L #V1 #T1 #HVT1 @and3_intro
[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpr_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpr_flat/ -HT2 #H destruct //
]
qed-.
-lemma cnr_inv_tau: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
+lemma cnr_inv_tau: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓝV.T⦄ → ⊥.
#G #L #V #T #H lapply (H T ?) -H
/2 width=4 by cpr_tau, discr_tpair_xy_y/
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: nf2_sort *)
-lemma cnr_sort: ∀G,L,k. ⦃G, L⦄ ⊢ 𝐍⦃⋆k⦄.
+lemma cnr_sort: ∀G,L,k. ⦃G, L⦄ ⊢ ➡ 𝐍⦃⋆k⦄.
#G #L #k #X #H
>(cpr_inv_sort1 … H) //
qed.
(* Basic_1: was: nf2_abst *)
-lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}W.T⦄.
+lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}W.T⦄.
#a #G #L #W #T #HW #HT #X #H
elim (cpr_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
>(HW … HW0) -W0 >(HT … HT0) -T0 //
qed.
(* Basic_1: was only: nf2_appl_lref *)
-lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄.
+lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄.
#G #L #V #T #HV #HT #HS #X #H
elim (cpr_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
>(HV … HV0) -V0 >(HT … HT0) -T0 //
qed.
(* Basic_1: was: nf2_dec *)
-axiom cnr_dec: ∀G,L,T1. ⦃G, L⦄ ⊢ 𝐍⦃T1⦄ ∨
+axiom cnr_dec: ∀G,L,T1. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T1⦄ ∨
∃∃T2. ⦃G, L⦄ ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
(* Basic_1: removed theorems 1: nf2_abst_shift *)
(* Main properties on context-sensitive irreducible terms *******************)
-theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
+theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄.
/2 width=4 by cpr_fwd_cir/ qed.
(* Main inversion lemmas on context-sensitive irreducible terms *************)
-theorem cnr_inv_cir: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄.
+theorem cnr_inv_cir: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄.
/2 width=5 by cnr_inv_crr/ qed-.
(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
(* Note: this property is unusual *)
-lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⊥.
+lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⊥.
#G #L #T #H elim H -L -T
[ #L #K #V #i #HLK #H
elim (cnr_inv_delta … HLK H)
(* Advanced properties ******************************************************)
(* Basic_1: was only: nf2_csort_lref *)
-lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
+lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
#G #L #i #HL #X #H
elim (cpr_inv_lref1 … H) -H // *
#K #V1 #V2 #HLK #_ #_
qed.
(* Basic_1: was: nf2_lref_abst *)
-lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄.
+lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄.
#G #L #K #V #i #HLK #X #H
elim (cpr_inv_lref1 … H) -H // *
#K0 #V1 #V2 #HLK0 #_ #_
(* Relocation properties ****************************************************)
(* Basic_1: was: nf2_lift *)
-lemma cnr_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ →
- ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄.
+lemma cnr_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ →
+ ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄.
#G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
<(HLT … HT1) in HT0; -L #HT0
qed.
(* Note: this was missing in basic_1 *)
-lemma cnr_inv_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄ →
- ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
+lemma cnr_inv_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄ →
+ ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄.
#G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
elim (lift_total X d e) #X0 #HX0
lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0
(* Basic inversion lemmas ***************************************************)
-lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄ → deg h g k 0.
+lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄ → deg h g k 0.
#h #g #G #L #k #H elim (deg_total h g k)
#l @(nat_ind_plus … l) -l // #l #_ #Hkl
lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_sort/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H)
qed-.
-lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥.
+lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄ → ⊥.
#h #g #I #G #L #K #V #i #HLK #H
elim (lift_total V 0 (i+1)) #W #HVW
lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct
elim (lift_inv_lref2_be … HVW) -HVW //
qed-.
-lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓛ{a}V.T⦄ →
- ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍[h, g]⦃T⦄.
+lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}V.T⦄ →
+ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
#h #g #a #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnx_inv_abbr: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃-ⓓV.T⦄ →
- ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍[h, g]⦃T⦄.
+lemma cnx_inv_abbr: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃-ⓓV.T⦄ →
+ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
#h #g #G #L #V1 #T1 #HVT1 @conj
[ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct //
| #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct //
]
qed-.
-lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃+ⓓV.T⦄ → ⊥.
+lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃+ⓓV.T⦄ → ⊥.
#h #g #G #L #V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3 by cpx_zeta/ #H destruct
]
qed-.
-lemma cnx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄ →
- ∧∧ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ & 𝐒⦃T⦄.
+lemma cnx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓐV.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ & 𝐒⦃T⦄.
#h #g #G #L #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpx_flat/ -HT2 #H destruct //
| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
[ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
- | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct
+ lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by cpr_cpx, cpr_theta/ -HV12 #H destruct
+ | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by cpr_cpx, cpr_beta/ #H destruct
]
]
qed-.
-lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓝV.T⦄ → ⊥.
+lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓝV.T⦄ → ⊥.
#h #g #G #L #V #T #H lapply (H T ?) -H
/2 width=4 by cpx_tau, discr_tpair_xy_y/
qed-.
(* Basic forward lemmas *****************************************************)
-lemma cnx_fwd_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄.
+lemma cnx_fwd_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄.
#h #g #G #L #T #H #U #HTU
@H /2 width=1 by cpr_cpx/ (**) (* auto fails because a δ-expansion gets in the way *)
qed-.
(* Basic properties *********************************************************)
-lemma cnx_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄.
+lemma cnx_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄.
#h #g #G #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_
lapply (deg_mono … Hkl Hk) -h -L <plus_n_Sm #H destruct
qed.
-lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆((next h)^l k)⦄.
+lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆((next h)^l k)⦄.
#h #g #G #L #k #l #Hkl
lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=6 by cnx_sort/
qed.
-lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍[h, g]⦃T⦄ →
- ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓛ{a}W.T⦄.
+lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
+ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}W.T⦄.
#h #g #a #G #L #W #T #HW #HT #X #H
elim (cpx_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
>(HW … HW0) -W0 >(HT … HT0) -T0 //
qed.
-lemma cnx_appl_simple: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → 𝐒⦃T⦄ →
- ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄.
+lemma cnx_appl_simple: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → 𝐒⦃T⦄ →
+ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓐV.T⦄.
#h #g #G #L #V #T #HV #HT #HS #X #H
elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct
>(HV … HV0) -V0 >(HT … HT0) -T0 //
qed.
-axiom cnx_dec: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T1⦄ ∨
+axiom cnx_dec: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T1⦄ ∨
∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & (T1 = T2 → ⊥).
(* Main properties on context-sensitive extended irreducible terms **********)
-theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄.
+theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
/2 width=6 by cpx_fwd_cix/ qed.
(* Main inversion lemmas on context-sensitive extended irreducible terms ****)
-theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄.
+theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄.
/2 width=7 by cnx_inv_crx/ qed-.
(* Advanced inversion lemmas on context-sensitive reducible terms ***********)
(* Note: this property is unusual *)
-lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⊥.
+lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⊥.
#h #g #G #L #T #H elim H -L -T
[ #L #k #l #Hkl #H
lapply (cnx_inv_sort … H) -H #H
| #I #L #K #V #i #HLK #H
elim (cnx_inv_delta … HLK H)
| #L #V #T #_ #IHV #H
- elim (cnx_inv_appl … H) -H /2 width=1/
+ elim (cnx_inv_appl … H) -H /2 width=1 by/
| #L #V #T #_ #IHT #H
- elim (cnx_inv_appl … H) -H /2 width=1/
+ elim (cnx_inv_appl … H) -H /2 width=1 by/
| #I #L #V #T * #H1 #H2 destruct
[ elim (cnx_inv_zeta … H2)
| elim (cnx_inv_tau … H2)
]
|6,7: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct
- [1,3: elim (cnx_inv_abbr … H2) -H2 /2 width=1/
- |*: elim (cnx_inv_abst … H2) -H2 /2 width=1/
+ [1,3: elim (cnx_inv_abbr … H2) -H2 /2 width=1 by/
+ |*: elim (cnx_inv_abst … H2) -H2 /2 width=1 by/
]
| #a #L #V #W #T #H
elim (cnx_inv_appl … H) -H #_ #_ #H
(* Advanced properties ******************************************************)
-lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄.
+lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄.
#h #g #G #L #i #HL #X #H
elim (cpx_inv_lref1 … H) -H // *
#I #K #V1 #V2 #HLK #_ #_
(* Relocation properties ****************************************************)
-lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⇩[s, d, e] L0 ≡ L →
- ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄.
+lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⇩[s, d, e] L0 ≡ L →
+ ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, g] 𝐍⦃T0⦄.
#h #g #G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H
elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1
<(HLT … HT1) in HT0; -L #HT0
>(lift_mono … HT10 … HT0) -T1 -X //
qed.
-lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[s, d, e] L0 ≡ L →
- ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄.
+lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ ➡[h, g] 𝐍⦃T0⦄ → ⇩[s, d, e] L0 ≡ L →
+ ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄.
#h #g #G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H
elim (lift_total X d e) #X0 #HX0
lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0
(* Advanced forward lemmas on context-sensitive irreducible terms ***********)
-lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ 𝐈⦃T1⦄ → T2 = T1.
+lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T1⦄ → T2 = T1.
#G #L #T1 #T2 #H elim H -G -L -T1 -T2
[ //
| #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
[ elim (cir_inv_bind … H) -H #HV1 #HT1 * #H destruct
lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
lapply (IHT1 … HT1) -IHT1 #H destruct //
- | elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=2/
+ | elim (cir_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/
]
| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
[ elim (cir_inv_appl … H) -H #HV1 #HT1 #_
>IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (cir_inv_ri2 … H) /2 width=1/
+ | elim (cir_inv_ri2 … H) /2 width=1 by/
]
| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
- elim (cir_inv_ri2 … H) /2 width=1/
+ 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/
| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
(* Advanced forward lemmas on context-sensitive extended irreducible terms **)
-lemma cpx_fwd_cix: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T1⦄ → T2 = T1.
+lemma cpx_fwd_cix: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T1⦄ → T2 = T1.
#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
[ //
| #G #L #k #l #Hkl #H elim (cix_inv_sort … Hkl H)
[ elim (cix_inv_bind … H) -H #HV1 #HT1 * #H destruct
lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct
lapply (IHT1 … HT1) -IHT1 #H destruct //
- | elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=2/
+ | elim (cix_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/
]
| * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H
[ elim (cix_inv_appl … H) -H #HV1 #HT1 #_
>IHV1 -IHV1 // -HV1 >IHT1 -IHT1 //
- | elim (cix_inv_ri2 … H) /2 width=1/
+ | elim (cix_inv_ri2 … H) /2 width=1 by/
]
| #G #L #V1 #T1 #T #T2 #_ #_ #_ #H
- elim (cix_inv_ri2 … H) /2 width=1/
+ elim (cix_inv_ri2 … H) /2 width=1 by or_introl/
| #G #L #V1 #T1 #T2 #_ #_ #H
- elim (cix_inv_ri2 … H) /2 width=1/
+ elim (cix_inv_ri2 … H) /2 width=1 by/
| #G #L #V1 #V2 #T #_ #_ #H
- elim (cix_inv_ri2 … H) /2 width=1/
+ elim (cix_inv_ri2 … H) /2 width=1 by/
| #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H
elim (cix_inv_appl … H) -H #_ #_ #H
elim (simple_inv_bind … H)
(* Basic inversion lemmas ***************************************************)
-fact crr_inv_sort_aux: ∀G,L,T,k. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⋆k → ⊥.
+fact crr_inv_sort_aux: ∀G,L,T,k. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = ⋆k → ⊥.
#G #L #T #k0 * -L -T
[ #L #K #V #i #HLK #H destruct
| #L #V #T #_ #H destruct
]
qed-.
-lemma crr_inv_sort: ∀G,L,k. ⦃G, L⦄ ⊢ 𝐑⦃⋆k⦄ → ⊥.
+lemma crr_inv_sort: ∀G,L,k. ⦃G, L⦄ ⊢ ➡ 𝐑⦃⋆k⦄ → ⊥.
/2 width=6 by crr_inv_sort_aux/ qed-.
-fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = #i →
+fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = #i →
∃∃K,V. ⇩[i] L ≡ K.ⓓV.
#G #L #T #j * -L -T
[ #L #K #V #i #HLK #H destruct /2 width=3 by ex1_2_intro/
]
qed-.
-lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[i] L ≡ K.ⓓV.
+lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ ➡ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[i] L ≡ K.ⓓV.
/2 width=4 by crr_inv_lref_aux/ qed-.
-fact crr_inv_gref_aux: ∀G,L,T,p. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = §p → ⊥.
+fact crr_inv_gref_aux: ∀G,L,T,p. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = §p → ⊥.
#G #L #T #q * -L -T
[ #L #K #V #i #HLK #H destruct
| #L #V #T #_ #H destruct
]
qed-.
-lemma crr_inv_gref: ∀G,L,p. ⦃G, L⦄ ⊢ 𝐑⦃§p⦄ → ⊥.
+lemma crr_inv_gref: ∀G,L,p. ⦃G, L⦄ ⊢ ➡ 𝐑⦃§p⦄ → ⊥.
/2 width=6 by crr_inv_gref_aux/ qed-.
-lemma trr_inv_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
+lemma trr_inv_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃⓪{I}⦄ → ⊥.
#G * #i #H
[ elim (crr_inv_sort … H)
| elim (crr_inv_lref … H) -H #L #V #H
]
qed-.
-fact crr_inv_ib2_aux: ∀a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W.U →
- ⦃G, L⦄ ⊢ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑⦃U⦄.
+fact crr_inv_ib2_aux: ∀a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = ⓑ{a,I}W.U →
+ ⦃G, L⦄ ⊢ ➡ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡ 𝐑⦃U⦄.
#G #b #J #L #W0 #U #T #HI * -L -T
[ #L #K #V #i #_ #H destruct
| #L #V #T #_ #H destruct
]
qed-.
-lemma crr_inv_ib2: ∀a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ →
- ⦃G, L⦄ ⊢ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑⦃T⦄.
+lemma crr_inv_ib2: ∀a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐑⦃ⓑ{a,I}W.T⦄ →
+ ⦃G, L⦄ ⊢ ➡ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡ 𝐑⦃T⦄.
/2 width=5 by crr_inv_ib2_aux/ qed-.
-fact crr_inv_appl_aux: ∀G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⓐW.U →
- ∨∨ ⦃G, L⦄ ⊢ 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
+fact crr_inv_appl_aux: ∀G,L,W,U,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = ⓐW.U →
+ ∨∨ ⦃G, L⦄ ⊢ ➡ 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
#G #L #W0 #U #T * -L -T
[ #L #K #V #i #_ #H destruct
| #L #V #T #HV #H destruct /2 width=1 by or3_intro0/
]
qed-.
-lemma crr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐑⦃ⓐV.T⦄ →
- ∨∨ ⦃G, L⦄ ⊢ 𝐑⦃V⦄ | ⦃G, L⦄ ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
+lemma crr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃ⓐV.T⦄ →
+ ∨∨ ⦃G, L⦄ ⊢ ➡ 𝐑⦃V⦄ | ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
/2 width=3 by crr_inv_appl_aux/ qed-.
(* Advanved properties ******************************************************)
-lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ 𝐑⦃T⦄.
+lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡ 𝐑⦃T⦄.
#G #L #K0 #T #H elim H -L -T /2 width=1/
#L #K #V #i #HLK
lapply (ldrop_fwd_length_lt2 … HLK) #Hi
lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=3/
qed.
-lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑⦃T⦄.
+lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄.
#G #L #T #H lapply (crr_append_sn … H) //
qed.
(* Advanced inversion lemmas ************************************************)
-fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ 𝐑⦃T⦄ →
- ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ 𝐑⦃T⦄.
+fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ ➡ 𝐑⦃T⦄ →
+ ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ ➡ 𝐑⦃T⦄.
#G #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/
[ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct
lapply (ldrop_fwd_length_lt2 … HLK1)
]
qed.
-lemma crr_inv_labst_last: ∀G,L,T,W. ⦃G, ⋆.ⓛW @@ L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑⦃T⦄.
+lemma crr_inv_labst_last: ∀G,L,T,W. ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄.
/2 width=4/ qed-.
-lemma crr_inv_trr: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐑⦃T⦄ → ⦃G, ⋆⦄ ⊢ 𝐑⦃T⦄.
+lemma crr_inv_trr: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄.
/2 width=4/ qed-.
(* Properties on relocation *************************************************)
-lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑⦃U⦄.
+lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄.
#G #K #T #H elim H -K -T
[ #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H
elim (lift_inv_lref1 … H) -H * #Hid #H destruct
]
qed.
-lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑⦃T⦄.
+lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐑⦃T⦄.
#G #L #U #H elim H -L -U
[ #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
(* Basic properties *********************************************************)
-lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄.
+lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
#h #g #G #L #T #H elim H -L -T
/2 width=4 by crx_delta, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
qed.
(* Basic inversion lemmas ***************************************************)
-fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⋆k →
+fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = ⋆k →
∃l. deg h g k (l+1).
#h #g #G #L #T #k0 * -L -T
[ #L #k #l #Hkl #H destruct /2 width=2 by ex_intro/
]
qed-.
-lemma crx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃⋆k⦄ → ∃l. deg h g k (l+1).
+lemma crx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃⋆k⦄ → ∃l. deg h g k (l+1).
/2 width=5 by crx_inv_sort_aux/ qed-.
-fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i →
+fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = #i →
∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V.
#h #g #G #L #T #j * -L -T
[ #L #k #l #_ #H destruct
]
qed-.
-lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V.
+lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃#i⦄ → ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V.
/2 width=6 by crx_inv_lref_aux/ qed-.
-fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = §p → ⊥.
+fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = §p → ⊥.
#h #g #G #L #T #q * -L -T
[ #L #k #l #_ #H destruct
| #I #L #K #V #i #HLK #H destruct
]
qed-.
-lemma crx_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃§p⦄ → ⊥.
+lemma crx_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃§p⦄ → ⊥.
/2 width=8 by crx_inv_gref_aux/ qed-.
-lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ →
+lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐑⦃⓪{I}⦄ →
∃∃k,l. deg h g k (l+1) & I = Sort k.
#h #g * #i #G #H
[ elim (crx_inv_sort … H) -H /2 width=4 by ex2_2_intro/
]
qed-.
-fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ →
- T = ⓑ{a,I}W.U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃U⦄.
+fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ →
+ T = ⓑ{a,I}W.U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡[h, g] 𝐑⦃U⦄.
#h #g #b #J #G #L #W0 #U #T #HI * -L -T
[ #L #k #l #_ #H destruct
| #I #L #K #V #i #_ #H destruct
]
qed-.
-lemma crx_inv_ib2: ∀h,g,a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓑ{a,I}W.T⦄ →
- ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃T⦄.
+lemma crx_inv_ib2: ∀h,g,a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃ⓑ{a,I}W.T⦄ →
+ ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
/2 width=5 by crx_inv_ib2_aux/ qed-.
-fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⓐW.U →
- ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ | (𝐒⦃U⦄ → ⊥).
+fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = ⓐW.U →
+ ∨∨ ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
#h #g #G #L #W0 #U #T * -L -T
[ #L #k #l #_ #H destruct
| #I #L #K #V #i #_ #H destruct
]
qed-.
-lemma crx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓐV.T⦄ →
- ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃V⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ | (𝐒⦃T⦄ → ⊥).
+lemma crx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃ⓐV.T⦄ →
+ ∨∨ ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃V⦄ | ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
/2 width=3 by crx_inv_appl_aux/ qed-.
(* Advanved properties ******************************************************)
-lemma crx_append_sn: ∀h,g,G,L,K,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, K @@ L⦄ ⊢ 𝐑[h, g]⦃T⦄.
-#h #g #G #L #K0 #T #H elim H -L -T /2 width=1/ /2 width=2/
+lemma crx_append_sn: ∀h,g,G,L,K,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
+#h #g #G #L #K0 #T #H elim H -L -T
+/2 width=2 by crx_sort, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/
#I #L #K #V #i #HLK
lapply (ldrop_fwd_length_lt2 … HLK) #Hi
-lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=4/
+lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=4 by crx_delta, lt_to_le/
qed.
-lemma trx_crx: ∀h,g,G,L,T. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄.
+lemma trx_crx: ∀h,g,G,L,T. ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
#h #g #G #L #T #H lapply (crx_append_sn … H) //
qed.
(* Properties on relocation *************************************************)
-lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄.
+lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄.
#h #g #G #K #T #H elim H -K -T
[ #K #k #l #Hkl #L #s #d #e #_ #X #H
>(lift_inv_sort1 … H) -X /2 width=2 by crx_sort/
]
qed.
-lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
- ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄.
+lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K →
+ ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄.
#h #g #G #L #U #H elim H -L -U
[ #L #k #l #Hkl #K #s #d #e #_ #X #H
>(lift_inv_sort2 … H) -X /2 width=2 by crx_sort/
]
[ { "context-sensitive extended computation" * } {
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_cpys" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
[ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_aaa" * ]
}
]
- [ { "context-sensitive extended normal forms" * } {
- [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
+ [ { "normal forms for context-sensitive extended reduction" * } {
+ [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
}
]
[ { "context-sensitive extended reduction" * } {
[ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ]
}
]
- [ { "context-sensitive extended irreducible forms" * } {
- [ "cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ )" "cix_append" + "cix_lift" * ]
+ [ { "irreducible forms for context-sensitive extended reduction" * } {
+ [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_append" + "cix_lift" * ]
}
]
- [ { "context-sensitive extended reducible forms" * } {
- [ "crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ )" "crx_append" + "crx_lift" * ]
+ [ { "reducible forms for context-sensitive extended reduction" * } {
+ [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_append" + "crx_lift" * ]
}
]
- [ { "context-sensitive normal forms" * } {
- [ "cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
+ [ { "normal forms for context-sensitive reduction" * } {
+ [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ]
}
]
[ { "context-sensitive reduction" * } {
[ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cir" * ]
}
]
- [ { "context-sensitive irreducible forms" * } {
- [ "cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ]
+ [ { "irreducible forms for context-sensitive reduction" * } {
+ [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ]
}
]
- [ { "context-sensitive reducible forms" * } {
- [ "crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ]
+ [ { "reducible forms for context-sensitive reduction" * } {
+ [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ]
}
]
}
projects / helm.git / commitdiff