#h #G #L #T1 #R @ltc_ind_dx_refl //
qed-.
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpms_inv_sort1 (n) (h) (G) (L): ∀X2,s. ⦃G, L⦄ ⊢ ⋆s ➡*[n, h] X2 → X2 = ⋆(((next h)^n) s).
+#n #h #G #L #X2 #s #H @(cpms_ind_dx … H) -X2 //
+#n1 #n2 #X #X2 #_ #IH #HX2 destruct
+elim (cpm_inv_sort1 … HX2) -HX2 * // #H1 #H2 destruct
+/2 width=3 by refl, trans_eq/
+qed-.
+
(* Basic properties *********************************************************)
(* Basic_1: includes: pr1_pr0 *)
/3 width=3 by cpms_step_sn, cpm_cpms, cpm_eps/
qed.
+lemma cpms_ee (n) (h) (G) (L):
+ ∀U1,U2. ⦃G, L⦄ ⊢ U1 ➡*[n, h] U2 →
+ ∀T. ⦃G, L⦄ ⊢ ⓝU1.T ➡*[↑n, h] U2.
+#n #h #G #L #U1 #U2 #H @(cpms_ind_sn … H) -U1 -n
+[ /3 width=1 by cpm_cpms, cpm_ee/
+| #n1 #n2 #U1 #U #HU1 #HU2 #_ #T >plus_S1
+ /3 width=3 by cpms_step_sn, cpm_ee/
+]
+qed.
+
(* Basic_2A1: uses: cprs_beta_dx *)
lemma cpms_beta_dx (n) (h) (G) (L):
∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 →
/4 width=9 by cpms_step_dx, cpm_cpms, cpms_bind_dx, cpms_appl_dx, cpm_theta/
qed.
-(* Basic inversion lemmas ***************************************************)
-
-lemma cpms_inv_sort1 (n) (h) (G) (L): ∀X2,s. ⦃G, L⦄ ⊢ ⋆s ➡*[n, h] X2 → X2 = ⋆(((next h)^n) s).
-#n #h #G #L #X2 #s #H @(cpms_ind_dx … H) -X2 //
-#n1 #n2 #X #X2 #_ #IH #HX2 destruct
-elim (cpm_inv_sort1 … HX2) -HX2 * // #H1 #H2 destruct
-/2 width=3 by refl, trans_eq/
-qed-.
-
(* Basic properties with r-transition ***************************************)
(* Basic_1: was: pr3_refl *)
lemma cprs_refl: ∀h,G,L. reflexive … (cpms h G L 0).
/2 width=1 by cpm_cpms/ qed.
-(* Basic_2A1: removed theorems 4:
+(* Basic_2A1: removed theorems 5:
sta_cprs_scpds lstas_scpds scpds_strap1 scpds_fwd_cprs
+ scpds_inv_lstas_eq
*)
--- /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/rt_computation/cpms_drops.ma".
+include "basic_2/rt_computation/cprs.ma".
+
+(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Main properties **********************************************************)
+
+(* Basic_2A1: uses: lstas_scpds_trans scpds_strap2 *)
+theorem cpms_trans (h) (G) (L):
+ ∀n1,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T →
+ ∀n2,T2. ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2.
+/2 width=3 by ltc_trans/ qed-.
+
+(* Basic_2A1: uses: scpds_cprs_trans *)
+theorem cpms_cprs_trans (n) (h) (G) (L):
+ ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T →
+ ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2.
+#n #h #G #L #T1 #T #HT1 #T2 #HT2 >(plus_n_O … n)
+/2 width=3 by cpms_trans/ qed-.
+
+(* Basic_2A1: includes: cprs_bind *)
+theorem cpms_bind (n) (h) (G) (L):
+ ∀I,V1,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n, h] ⓑ{p,I}V2.T2.
+#n #h #G #L #I #V1 #T1 #T2 #HT12 #V2 #H @(cprs_ind_dx … H) -V2
+[ /2 width=1 by cpms_bind_dx/
+| #V #V2 #_ #HV2 #IH #p >(plus_n_O … n) -HT12
+ /3 width=3 by cpr_pair_sn, cpms_step_dx/
+]
+qed.
+
+theorem cpms_appl (n) (h) (G) (L):
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 →
+ ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[n, h] ⓐV2.T2.
+#n #h #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind_dx … H) -V2
+[ /2 width=1 by cpms_appl_dx/
+| #V #V2 #_ #HV2 #IH >(plus_n_O … n) -HT12
+ /3 width=3 by cpr_pair_sn, cpms_step_dx/
+]
+qed.
+
+lemma cpms_inv_plus (h) (G) (L): ∀n1,n2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T & ⦃G, L⦄ ⊢ T ➡*[n2, h] T2.
+#h #G #L #n1 elim n1 -n1 /2 width=3 by ex2_intro/
+#n1 #IH #n2 #T1 #T2 <plus_S1 #H
+elim (cpms_inv_succ_sn … H) -H #T0 #HT10 #HT02
+elim (IH … HT02) -IH -HT02 #T #HT0 #HT2
+lapply (cpms_trans … HT10 … HT0) -T0 #HT1
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma cpms_cast (n) (h) (G) (L):
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀U1,U2. ⦃G, L⦄ ⊢ U1 ➡*[n, h] U2 →
+ ⦃G, L⦄ ⊢ ⓝU1.T1 ➡*[n, h] ⓝU2.T2.
+#n #h #G #L #T1 #T2 #H @(cpms_ind_sn … H) -T1 -n
+[ /3 width=3 by cpms_cast_sn/
+| #n1 #n2 #T1 #T #HT1 #_ #IH #U1 #U2 #H
+ elim (cpms_inv_plus … H) -H #U #HU1 #HU2
+ /3 width=3 by cpms_trans, cpms_cast_sn/
+]
+qed.
+
+(* Basic_2A1: includes: cprs_beta_rc *)
+theorem cpms_beta_rc (n) (h) (G) (L):
+ ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 →
+ ∀W1,T1,T2. ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀W2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ➡*[n, h] ⓓ{p}ⓝW2.V2.T2.
+#n #h #G #L #V1 #V2 #HV12 #W1 #T1 #T2 #HT12 #W2 #H @(cprs_ind_dx … H) -W2
+[ /2 width=1 by cpms_beta_dx/
+| #W #W2 #_ #HW2 #IH #p >(plus_n_O … n) -HT12
+ /4 width=3 by cpr_pair_sn, cpms_step_dx/
+]
+qed.
+
+(* Basic_2A1: includes: cprs_beta *)
+theorem cpms_beta (n) (h) (G) (L):
+ ∀W1,T1,T2. ⦃G, L.ⓛW1⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀W2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 →
+ ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓐV1.ⓛ{p}W1.T1 ➡*[n, h] ⓓ{p}ⓝW2.V2.T2.
+#n #h #G #L #W1 #T1 #T2 #HT12 #W2 #HW12 #V1 #V2 #H @(cprs_ind_dx … H) -V2
+[ /2 width=1 by cpms_beta_rc/
+| #V #V2 #_ #HV2 #IH #p >(plus_n_O … n) -HT12
+ /4 width=5 by cpms_step_dx, cpr_pair_sn, cpm_cast/
+]
+qed.
+
+(* Basic_2A1: includes: cprs_theta_rc *)
+theorem cpms_theta_rc (n) (h) (G) (L):
+ ∀V1,V. ⦃G, L⦄ ⊢ V1 ➡[h] V → ∀V2. ⬆*[1] V ≘ V2 →
+ ∀W1,T1,T2. ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀W2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n, h] ⓓ{p}W2.ⓐV2.T2.
+#n #h #G #L #V1 #V #HV1 #V2 #HV2 #W1 #T1 #T2 #HT12 #W2 #H @(cprs_ind_dx … H) -W2
+[ /2 width=3 by cpms_theta_dx/
+| #W #W2 #_ #HW2 #IH #p >(plus_n_O … n) -HT12
+ /3 width=3 by cpr_pair_sn, cpms_step_dx/
+]
+qed.
+
+(* Basic_2A1: includes: cprs_theta *)
+theorem cpms_theta (n) (h) (G) (L):
+ ∀V,V2. ⬆*[1] V ≘ V2 → ∀W1,W2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 →
+ ∀T1,T2. ⦃G, L.ⓓW1⦄ ⊢ T1 ➡*[n, h] T2 →
+ ∀V1. ⦃G, L⦄ ⊢ V1 ➡*[h] V →
+ ∀p. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}W1.T1 ➡*[n, h] ⓓ{p}W2.ⓐV2.T2.
+#n #h #G #L #V #V2 #HV2 #W1 #W2 #HW12 #T1 #T2 #HT12 #V1 #H @(cprs_ind_sn … H) -V1
+[ /2 width=3 by cpms_theta_rc/
+| #V1 #V0 #HV10 #_ #IH #p >(plus_O_n … n) -HT12
+ /3 width=3 by cpr_pair_sn, cpms_step_sn/
+]
+qed.
+(*
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was pr3_gen_appl *)
+lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 →
+ ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L⦄ ⊢ T1 ➡* T2 &
+ U2 = ⓐV2. T2
+ | ∃∃a,W,T. ⦃G, L⦄ ⊢ T1 ➡* ⓛ{a}W.T &
+ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V1.T ➡* U2
+ | ∃∃a,V0,V2,V,T. ⦃G, L⦄ ⊢ V1 ➡* V0 & ⬆[0,1] V0 ≘ V2 &
+ ⦃G, L⦄ ⊢ T1 ➡* ⓓ{a}V.T &
+ ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡* U2.
+#G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpr_inv_appl1 … HU2) -HU2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cprs_strap1, or3_intro0, ex3_2_intro/
+ | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
+ lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12
+ lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
+ /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_beta, ex2_3_intro, or3_intro1/
+ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
+ /5 width=10 by cprs_flat_sn, cprs_bind_dx, cprs_strap1, ex4_5_intro, or3_intro2/
+ ]
+| /4 width=9 by cprs_strap1, or3_intro1, ex2_3_intro/
+| /4 width=11 by cprs_strap1, or3_intro2, ex4_5_intro/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma scpds_inv_abst1: ∀h,o,a,G,L,V1,T1,U2,d. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, o, d] U2 →
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, o, d] T2 &
+ U2 = ⓛ{a}V2.T2.
+#h #o #a #G #L #V1 #T1 #U2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
+lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
+elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
+/3 width=6 by ex4_2_intro, ex3_2_intro/
+qed-.
+
+lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 →
+ ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true.
+#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
+lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
+elim (cprs_inv_abbr1 … H2) -H2 *
+[ #V2 #U2 #HV12 #HU12 #H destruct
+| /3 width=6 by ex4_2_intro, ex3_intro/
+]
+qed-.
+
+lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 →
+ ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2.
+#h #o #G #L #T1 #T2 #d2 *
+#T0 #d1 #_ #_ #HT10 #HT02 #T #HT1
+lapply (lstas_mono … HT10 … HT1) #H destruct //
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem scpds_conf_eq: ∀h,o,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T1 →
+ ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
+#h #o #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2
+lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_conf/
+qed-.
+*)
(* Forward lemmas with unbound context-sensitive rt-computation for terms ***)
-(* Basic_2A1: includes: cprs_cpxs *)
+(* Basic_2A1: includes: scpds_fwd_cpxs cprs_cpxs *)
lemma cpms_fwd_cpxs (n) (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 → ⦃G, L⦄ ⊢ T1 ⬈*[h] T2.
#n #h #G #L #T1 #T2 #H @(cpms_ind_dx … H) -T2
/3 width=4 by cpxs_strap1, cpm_fwd_cpx/
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+(* Properties with generic slicing for local environments *******************)
+
+lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n).
+/3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-.
+
+(* Basic_2A1: uses: scpds_lift *)
+(* Basic_2A1: includes: cprs_lift *)
+(* Basic_1: includes: pr3_lift *)
+lemma cpms_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpms h G L n).
+#n #h #G @d_liftable2_sn_bi
+/2 width=6 by cpms_lifts_sn, lifts_mono/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: uses: scpds_inv_lift1 *)
+(* Basic_2A1: includes: cprs_inv_lift1 *)
+(* Basic_1: includes: pr3_gen_lift *)
+lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n).
+/3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-.
+
+lemma cpms_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpms h G L n).
+#n #h #G @d_deliftable2_sn_bi
+/2 width=6 by cpms_inv_lifts_sn, lifts_inj/
+qed-.
+
(* Advanced properties ******************************************************)
+lemma cpms_delta (n) (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡*[n, h] V2 →
+ ∀W2. ⬆*[1] V2 ≘ W2 → ⦃G, K.ⓓV1⦄ ⊢ #0 ➡*[n, h] W2.
+#n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2
+[ /3 width=3 by cpm_cpms, cpm_delta/
+| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
+ elim (lifts_total V (𝐔❴1❵)) #W #HVW
+ /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpms_ell (n) (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡*[n, h] V2 →
+ ∀W2. ⬆*[1] V2 ≘ W2 → ⦃G, K.ⓛV1⦄ ⊢ #0 ➡*[↑n, h] W2.
+#n #h #G #K #V1 #V2 #H @(cpms_ind_dx … H) -V2
+[ /3 width=3 by cpm_cpms, cpm_ell/
+| #n1 #n2 #V #V2 #_ #IH #HV2 #W2 #HVW2
+ elim (lifts_total V (𝐔❴1❵)) #W #HVW >plus_S1
+ /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpms_lref (n) (h) (I) (G): ∀K,T,i. ⦃G, K⦄ ⊢ #i ➡*[n, h] T →
+ ∀U. ⬆*[1] T ≘ U → ⦃G, K.ⓘ{I}⦄ ⊢ #↑i ➡*[n, h] U.
+#n #h #I #G #K #T #i #H @(cpms_ind_dx … H) -T
+[ /3 width=3 by cpm_cpms, cpm_lref/
+| #n1 #n2 #T #T2 #_ #IH #HT2 #U2 #HTU2
+ elim (lifts_total T (𝐔❴1❵)) #U #TU
+ /5 width=11 by cpms_step_dx, cpm_lifts_bi, drops_refl, drops_drop/
+]
+qed.
+
+lemma cpms_cast_sn (n) (h) (G) (L):
+ ∀U1,U2. ⦃G, L⦄ ⊢ U1 ➡*[n, h] U2 →
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
+ ⦃G, L⦄ ⊢ ⓝU1.T1 ➡*[n, h] ⓝU2.T2.
+#n #h #G #L #U1 #U2 #H @(cpms_ind_sn … H) -U1 -n
+[ /3 width=3 by cpm_cpms, cpm_cast/
+| #n1 #n2 #U1 #U #HU1 #_ #IH #T1 #T2 #H
+ elim (cpm_fwd_plus … H) -H #T #HT1 #HT2
+ /3 width=3 by cpms_step_sn, cpm_cast/
+]
+qed.
+
(* Note: apparently this was missing in basic_1 *)
(* Basic_2A1: uses: cprs_delta *)
lemma cpms_delta_drops (n) (h) (G):
]
qed-.
-(* Properties with generic slicing for local environments *******************)
-
-lemma cpms_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpms h G L n).
-/3 width=6 by d2_liftable_sn_ltc, cpm_lifts_sn/ qed-.
-
-(* Basic_2A1: uses: scpds_lift *)
-(* Basic_2A1: includes: cprs_lift *)
-(* Basic_1: includes: pr3_lift *)
-lemma cpms_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpms h G L n).
-#n #h #G @d_liftable2_sn_bi
-/2 width=6 by cpms_lifts_sn, lifts_mono/
-qed-.
-
-(* Inversion lemmas with generic slicing for local environments *************)
-
-(* Basic_2A1: uses: scpds_inv_lift1 *)
-(* Basic_2A1: includes: cprs_inv_lift1 *)
-(* Basic_1: includes: pr3_gen_lift *)
-lemma cpms_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpms h G L n).
-/3 width=6 by d2_deliftable_sn_ltc, cpm_inv_lifts_sn/ qed-.
-
-lemma cpms_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpms h G L n).
-#n #h #G @d_deliftable2_sn_bi
-/2 width=6 by cpms_inv_lifts_sn, lifts_inj/
+fact cpms_inv_succ_sn (n) (h) (G) (L):
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[↑n, h] T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[1, h] T & ⦃G, L⦄ ⊢ T ➡*[n, h] T2.
+#n #h #G #L #T1 #T2
+@(insert_eq_0 … (↑n)) #m #H
+@(cpms_ind_sn … H) -T1 -m
+[ #H destruct
+| #x1 #n2 #T1 #T #HT1 #HT2 #IH #H
+ elim (plus_inv_S3_sn x1 n2) [1,2: * |*: // ] -H
+ [ #H1 #H2 destruct -HT2
+ elim IH -IH // #T0 #HT0 #HT02
+ /3 width=3 by cpms_step_sn, ex2_intro/
+ | #n1 #H1 #H2 destruct -IH
+ elim (cpm_fwd_plus … 1 n1 T1 T) [|*: // ] -HT1 #T0 #HT10 #HT0
+ /3 width=5 by cpms_step_sn, cpm_cpms, ex2_intro/
+ ]
+]
qed-.
(* *)
(**************************************************************************)
-include "ground_2/lib/star.ma".
include "basic_2/rt_transition/lpr.ma".
-include "basic_2/rt_computation/cpms.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* Properties concerning sn parallel reduction on local environments ********)
-(* Basic_1: uses: pr3_pr2_pr2_t *)
-(* Basic_1: includes: pr3_pr0_pr2_t *)
-(* Basic_2A1: uses: lpr_cpr_trans *)
-lemma lpr_cpm_trans (n) (h) (G): s_r_transitive … (λL. cpm h G L n) (λ_. lpr h G).
-#n #h #G #L2 #T1 #T2 #H @(cpm_ind … H) -G -L2 -T1 -T2
+lemma lpr_cpm_trans (n) (h) (G):
+ ∀L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[n, h] T2 →
+ ∀L1. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[n, h] T2.
+#n #h #G #L2 #T1 #T2 #H @(cpm_ind … H) -n -G -L2 -T1 -T2
[ /2 width=3 by/
-| /3 width=2 by cpx_cpxs, cpx_ess/
-| #I #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H
- elim (lpx_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct
- /4 width=3 by cpxs_delta, cpxs_strap2/
-| #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H
- elim (lpx_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct
- /4 width=3 by cpxs_lref, cpxs_strap2/
-|5,10: /4 width=1 by cpxs_beta, cpxs_bind, lpx_bind_refl_dx/
-|6,8,9: /3 width=1 by cpxs_flat, cpxs_ee, cpxs_eps/
-| /4 width=3 by cpxs_zeta, lpx_bind_refl_dx/
-| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_bind_refl_dx/
+| /3 width=2 by cpm_cpms/
+| #n #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H
+ elim (lpr_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct
+ /4 width=3 by cpms_delta, cpms_step_sn/
+| #n #G #K2 #V2 #V4 #W4 #_ #IH #HVW4 #L1 #H
+ elim (lpr_inv_pair_dx … H) -H #K1 #V1 #HK12 #HV12 #H destruct
+ /4 width=3 by cpms_ell, cpms_step_sn/
+| #n #I2 #G #K2 #T #U #i #_ #IH #HTU #L1 #H
+ elim (lpr_inv_bind_dx … H) -H #I1 #K1 #HK12 #HI12 #H destruct
+ /4 width=3 by cpms_lref, cpms_step_sn/
+| /4 width=1 by cpms_bind, lpr_bind_refl_dx/
+| /3 width=1 by cpms_appl/
+| /3 width=1 by cpms_cast/
+| /4 width=3 by cpms_zeta, lpr_bind_refl_dx/
+| /3 width=1 by cpms_eps/
+| /3 width=1 by cpms_ee/
+| /4 width=1 by lpr_bind_refl_dx, cpms_beta/
+| /4 width=3 by lpr_bind_refl_dx, cpms_theta/
]
qed-.
+(*
-
-
-
-
-
-#G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
-[ /2 width=3 by/
-| #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
- elim (lpr_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
- elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
- /4 width=6 by cprs_strap2, cprs_delta/
-|3,7: /4 width=1 by lpr_pair, cprs_bind, cprs_beta/
-|4,6: /3 width=1 by cprs_flat, cprs_eps/
-|5,8: /4 width=3 by lpr_pair, cprs_zeta, cprs_theta, cprs_strap1/
-]
-qed-.
+(* Basic_1: uses: pr3_pr2_pr2_t *)
+(* Basic_1: includes: pr3_pr0_pr2_t *)
+(* Basic_2A1: includes: lpr_cpr_trans *)
+lemma lpr_cpm_trans (n) (h) (G): s_r_transitive … (λL. cpm h G L n) (λ_. lpr h G).
lemma cpr_bind2: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡ T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ➡* T2 →
∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
/4 width=5 by lpr_cprs_trans, cprs_bind_dx, lpr_pair/ qed.
+*)
\ No newline at end of file
(* *)
(**************************************************************************)
-include "basic_2/reduction/lpr_lpr.ma".
-include "basic_2/computation/cprs_lift.ma".
+include "basic_2/rt_transition/lpr_lpr.ma".
+include "basic_2/rt_computation/cpms_cpms.ma".
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION FOR TERMS *************************)
(* Main properties **********************************************************)
theorem cprs_conf: ∀G,L. confluent2 … (cprs G L) (cprs G L).
normalize /3 width=3 by cpr_conf, TC_confluent2/ qed-.
-theorem cprs_bind: ∀a,I,G,L,V1,V2,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
- ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
-#a #I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2
-/3 width=5 by cprs_trans, cprs_bind_dx/
-qed.
-
(* Basic_1: was: pr3_flat *)
-theorem cprs_flat: ∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
- ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡* ⓕ{I}V2.T2.
-#I #G #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2
-/3 width=3 by cprs_flat_dx, cprs_strap1, cpr_pair_sn/
-qed.
-
-theorem cprs_beta_rc: ∀a,G,L,V1,V2,W1,W2,T1,T2.
- ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 →
- ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HT12 #H @(cprs_ind … H) -W2 /2 width=1 by cprs_beta_dx/
-#W #W2 #_ #HW2 #IHW1 (**) (* fulla uto too slow 14s *)
-@(cprs_trans … IHW1) -IHW1 /3 width=1 by cprs_flat_dx, cprs_bind/
-qed.
-
-theorem cprs_beta: ∀a,G,L,V1,V2,W1,W2,T1,T2.
- ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L⦄ ⊢ V1 ➡* V2 →
- ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2.
-#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HT12 #HW12 #H @(cprs_ind … H) -V2 /2 width=1 by cprs_beta_rc/
-#V #V2 #_ #HV2 #IHV1
-@(cprs_trans … IHV1) -IHV1 /3 width=1 by cprs_flat_sn, cprs_bind/
-qed.
-
-theorem cprs_theta_rc: ∀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 #HT12 #H @(cprs_ind … H) -W2
-/3 width=5 by cprs_trans, cprs_theta_dx, cprs_bind_dx/
-qed.
-
-theorem cprs_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
- ⬆[0, 1] V ≘ V2 → ⦃G, L⦄ ⊢ W1 ➡* W2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 →
- ⦃G, L⦄ ⊢ V1 ➡* V → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(cprs_ind_dx … H) -V1
-/3 width=3 by cprs_trans, cprs_theta_rc, cprs_flat_dx/
+theorem cprs_flat (h) (G) (L):
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h] T2 →
+ ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 →
+ ∀I. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡*[h] ⓕ{I}V2.T2.
+#h #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind_dx … H) -V2
+[ /2 width=3 by cprs_flat_dx/
+| /3 width=3 by cpr_pair_sn, cprs_step_dx/
+]
qed.
(* Advanced inversion lemmas ************************************************)
--- /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/syntax/cext2.ma".
+include "basic_2/rt_computation/cpms.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL R-COMPUTATION FOR BINDERS *********************)
+
+definition cprs_ext (h) (G): relation3 lenv bind bind ≝
+ cext2 (λL. cpms h G L 0).
+
+interpretation
+ "context-sensitive parallel r-computation (binder)"
+ 'PRedStar h G L I1 I2 = (cprs_ext h G L I1 I2).
include "basic_2/notation/relations/predsnstar_4.ma".
include "basic_2/relocation/lex.ma".
-include "basic_2/rt_computation/cpms.ma".
+include "basic_2/rt_computation/cprs_ext.ma".
(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
+++ /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/reduction/lpr_drop.ma".
-include "basic_2/computation/lprs.ma".
-
-(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
-
-(* Properties on local environment slicing ***********************************)
-
-lemma lprs_drop_conf: ∀G. dropable_sn (lprs G).
-/3 width=3 by dropable_sn_TC, lpr_drop_conf/ qed-.
-
-lemma drop_lprs_trans: ∀G. dedropable_sn (lprs G).
-/3 width=3 by dedropable_sn_TC, drop_lpr_trans/ qed-.
-
-lemma lprs_drop_trans_O1: ∀G. dropable_dx (lprs G).
-/3 width=3 by dropable_dx_TC, lpr_drop_trans_O1/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/relocation/drops_lex.ma".
+include "basic_2/rt_computation/cpms_drops.ma".
+
+(* PARALLEL R-COMPUTATION FOR FULL LOCAL ENVIRONMENTS ***********************)
+
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_2A1: was: drop_lprs_trans *)
+lemma drops_lprs_trans (h) (G): dedropable_sn (λL.cpms h G L 0).
+/3 width=6 by lex_liftable_dedropable_sn, cpms_lifts_sn/ qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_2A1: was: lprs_drop_conf *)
+lemma lprs_drops_conf (h) (G): dropable_sn (λL.cpms h G L 0).
+/2 width=3 by lex_dropable_sn/ qed-.
+
+(* Basic_2A1: was: lprs_drop_trans_O1 *)
+lemma lprs_drops_trans (h) (G): dropable_dx (λL.cpms h G L 0).
+/2 width=3 by lex_dropable_dx/ qed-.
(**************************************************************************)
include "basic_2/relocation/lex_tc.ma".
-include "basic_2/rt_computation/lpxs.ma".
include "basic_2/rt_computation/cpxs_lpx.ma".
+include "basic_2/rt_computation/lpxs.ma".
(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lpxs.ma fpbs_csx.ma fpbs_fpbs.ma
fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma
-cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_cpxs.ma
+cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_lpr.ma cpms_cpxs.ma cpms_cpms.ma
cprs.ma cprs_drops.ma
-lprs.ma lprs_length.ma
+cprs_ext.ma
+lprs.ma lprs_length.ma lprs_drops.ma
+++ /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/unfold/lstas_da.ma".
-include "basic_2/computation/lprs_cprs.ma".
-include "basic_2/computation/cpxs_cpxs.ma".
-include "basic_2/computation/scpds.ma".
-
-(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************)
-
-(* Advanced properties ******************************************************)
-
-lemma scpds_strap2: ∀h,o,G,L,T1,T,T2,d1,d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d1+1 →
- ⦃G, L⦄ ⊢ T1 •*[h, 1] T → ⦃G, L⦄ ⊢ T •*➡*[h, o, d] T2 →
- ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d+1] T2.
-#h #o #G #L #T1 #T #T2 #d1 #d #Hd1 #HT1 *
-#T0 #d0 #Hd0 #HTd0 #HT0 #HT02
-lapply (lstas_da_conf … HT1 … Hd1) <minus_plus_k_k #HTd1
-lapply (da_mono … HTd0 … HTd1) -HTd0 -HTd1 #H destruct
-lapply (lstas_trans … HT1 … HT0) -T >commutative_plus
-/3 width=6 by le_S_S, ex4_2_intro/
-qed.
-
-lemma scpds_cprs_trans: ∀h,o,G,L,T1,T,T2,d.
- ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2.
-#h #o #G #L #T1 #T #T2 #d * /3 width=8 by cprs_trans, ex4_2_intro/
-qed-.
-
-lemma lstas_scpds_trans: ∀h,o,G,L,T1,T,T2,d1,d2,d.
- d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 →
- ⦃G, L⦄ ⊢ T1 •*[h, d2] T → ⦃G, L⦄ ⊢ T •*➡*[h, o, d] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d2+d] T2.
-#h #o #G #L #T1 #T #T2 #d1 #d2 #d #Hd21 #HTd1 #HT1 * #T0 #d0 #Hd0 #HTd0 #HT0 #HT02
-lapply (lstas_da_conf … HT1 … HTd1) #HTd12
-lapply (da_mono … HTd12 … HTd0) -HTd12 -HTd0 #H destruct
-lapply (le_minus_to_plus_c … Hd21 Hd0) -Hd21 -Hd0
-/3 width=7 by lstas_trans, ex4_2_intro/
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma scpds_inv_abst1: ∀h,o,a,G,L,V1,T1,U2,d. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, o, d] U2 →
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, o, d] T2 &
- U2 = ⓛ{a}V2.T2.
-#h #o #a #G #L #V1 #T1 #U2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
-lapply (da_inv_bind … Hd1) -Hd1 #Hd1
-elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
-elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
-/3 width=6 by ex4_2_intro, ex3_2_intro/
-qed-.
-
-lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 →
- ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true.
-#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
-lapply (da_inv_bind … Hd1) -Hd1 #Hd1
-elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
-elim (cprs_inv_abbr1 … H2) -H2 *
-[ #V2 #U2 #HV12 #HU12 #H destruct
-| /3 width=6 by ex4_2_intro, ex3_intro/
-]
-qed-.
-
-lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 →
- ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2.
-#h #o #G #L #T1 #T2 #d2 *
-#T0 #d1 #_ #_ #HT10 #HT02 #T #HT1
-lapply (lstas_mono … HT10 … HT1) #H destruct //
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma scpds_fwd_cpxs: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, o] T2.
-#h #o #G #L #T1 #T2 #d * /3 width=5 by cpxs_trans, lstas_cpxs, cprs_cpxs/
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem scpds_conf_eq: ∀h,o,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T1 →
- ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T2 →
- ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T.
-#h #o #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2
-lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_conf/
-qed-.
(* Basic eliminators ********************************************************)
-lemma isrt_inv_max_shift_sn: ∀n,c1,c2. 𝐑𝐓⦃n, ↕*c1 ∨ c2⦄ →
- ∧∧ 𝐑𝐓⦃0, c1⦄ & 𝐑𝐓⦃n, c2⦄.
-#n #c1 #c2 #H
-elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
-elim (isrt_inv_shift … Hc1) -Hc1 #Hc1 * -n1
-/2 width=1 by conj/
-qed-.
-
-lemma isrt_inv_max_eq_t: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → eq_t c1 c2 →
- ∧∧ 𝐑𝐓⦃n, c1⦄ & 𝐑𝐓⦃n, c2⦄.
-#n #c1 #c2 #H #Hc12
-elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
-lapply (isrt_eq_t_trans … Hc1 … Hc12) -Hc12 #H
-<(isrt_inj … H … Hc2) -Hc2
-<idempotent_max /2 width=1 by conj/
-qed-.
-
lemma cpm_ind (h): ∀R:relation5 nat genv lenv term term.
(∀I,G,L. R 0 G L (⓪{I}) (⓪{I})) →
(∀G,L,s. R 1 G L (⋆s) (⋆(next h s))) →
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* Properties with generic slicing for local environments *******************)
+
+(* Basic_1: includes: pr0_lift pr2_lift *)
+(* Basic_2A1: includes: cpr_lift *)
+lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpm h G L n).
+#n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
+elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
+/3 width=5 by ex2_intro/
+qed-.
+
+lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpm h G L n).
+#n #h #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/
+qed-.
+
+(* Inversion lemmas with generic slicing for local environments *************)
+
+(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
+(* Basic_2A1: includes: cpr_inv_lift1 *)
+lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpm h G L n).
+#n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
+elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
+/3 width=5 by ex2_intro/
+qed-.
+
+lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpm h G L n).
+#n #h #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
+qed-.
+
(* Advanced properties ******************************************************)
(* Basic_1: includes: pr2_delta1 *)
]
qed-.
-(* Properties with generic slicing for local environments *******************)
-
-(* Basic_1: includes: pr0_lift pr2_lift *)
-(* Basic_2A1: includes: cpr_lift *)
-lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (λL. cpm h G L n).
-#n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
-elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
-/3 width=5 by ex2_intro/
-qed-.
-
-lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (λL. cpm h G L n).
-#n #h #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/
-qed-.
-
-(* Inversion lemmas with generic slicing for local environments *************)
+(* Advanced forward lemmas **************************************************)
-(* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
-(* Basic_2A1: includes: cpr_inv_lift1 *)
-lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (λL. cpm h G L n).
-#n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
-elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
-/3 width=5 by ex2_intro/
+fact cpm_fwd_plus_aux (n) (h): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
+ ∀n1,n2. n1+n2 = n →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T & ⦃G, L⦄ ⊢ T ➡[n2, h] T2.
+#n #h #G #L #T1 #T2 #H @(cpm_ind … H) -G -L -T1 -T2 -n
+[ #I #G #L #n1 #n2 #H
+ elim (plus_inv_O3 … H) -H #H1 #H2 destruct
+ /2 width=3 by ex2_intro/
+| #G #L #s #x1 #n2 #H
+ elim (plus_inv_S3_sn … H) -H *
+ [ #H1 #H2 destruct /2 width=3 by ex2_intro/
+ | #n1 #H1 #H elim (plus_inv_O3 … H) -H #H2 #H3 destruct
+ /2 width=3 by ex2_intro/
+ ]
+| #n #G #K #V1 #V2 #W2 #_ #IH #HVW2 #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #V #HV1 #HV2
+ elim (lifts_total V 𝐔❴↑O❵) #W #HVW
+ /5 width=11 by cpm_lifts_bi, cpm_delta, drops_refl, drops_drop, ex2_intro/
+| #n #G #K #V1 #V2 #W2 #HV12 #IH #HVW2 #x1 #n2 #H
+ elim (plus_inv_S3_sn … H) -H *
+ [ #H1 #H2 destruct -IH /3 width=3 by cpm_ell, ex2_intro/
+ | #n1 #H1 #H2 destruct -HV12
+ elim (IH n1) [|*: // ] -IH #V #HV1 #HV2
+ elim (lifts_total V 𝐔❴↑O❵) #W #HVW
+ /5 width=11 by cpm_lifts_bi, cpm_ell, drops_refl, drops_drop, ex2_intro/
+ ]
+| #n #I #G #K #T2 #U2 #i #_ #IH #HTU2 #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #T #HT1 #HT2
+ elim (lifts_total T 𝐔❴↑O❵) #U #HTU
+ /5 width=11 by cpm_lifts_bi, cpm_lref, drops_refl, drops_drop, ex2_intro/
+| #n #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
+ elim IHT [|*: // ] -IHT #T #HT1 #HT2
+ /3 width=5 by cpm_bind, ex2_intro/
+| #n #G #L #V1 #V2 #T1 #T2 #HV12 #_ #_ #IHT #n1 #n2 #H destruct
+ elim IHT [|*: // ] -IHT #T #HT1 #HT2
+ /3 width=5 by cpm_appl, ex2_intro/
+| #n #G #L #U1 #U2 #T1 #T2 #_ #_ #IHU #IHT #n1 #n2 #H destruct
+ elim IHU [|*: // ] -IHU #U #HU1 #HU2
+ elim IHT [|*: // ] -IHT #T #HT1 #HT2
+ /3 width=5 by cpm_cast, ex2_intro/
+| #n #G #K #V #T1 #T2 #V2 #_ #IH #HVT2 #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #T #HT1 #HT2
+ /3 width=6 by cpm_zeta, cpm_bind, ex2_intro/
+| #n #G #L #U #T1 #T2 #_ #IH #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #T #HT1 #HT2
+ /3 width=3 by cpm_eps, ex2_intro/
+| #n #G #L #U1 #U2 #T #HU12 #IH #x1 #n2 #H
+ elim (plus_inv_S3_sn … H) -H *
+ [ #H1 #H2 destruct -IH /3 width=4 by cpm_ee, cpm_cast, ex2_intro/
+ | #n1 #H1 #H2 destruct -HU12
+ elim (IH n1) [|*: // ] -IH #U #HU1 #HU2
+ /3 width=3 by cpm_ee, ex2_intro/
+ ]
+| #n #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #T #HT1 #HT2
+ /4 width=7 by cpm_beta, cpm_appl, cpm_bind, ex2_intro/
+| #n #p #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #HV12 #HW12 #_ #_ #_ #IH #HVU2 #n1 #n2 #H destruct
+ elim IH [|*: // ] -IH #T #HT1 #HT2
+ /4 width=7 by cpm_theta, cpm_appl, cpm_bind, ex2_intro/
+]
qed-.
-lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (λL. cpm h G L n).
-#n #h #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/
-qed-.
+lemma cpm_fwd_plus (h) (G) (L): ∀n1,n2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[n1+n2, h] T2 →
+ ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[n1, h] T & ⦃G, L⦄ ⊢ T ➡[n2, h] T2.
+/2 width=3 by cpm_fwd_plus_aux/ qed-.
(* *)
(**************************************************************************)
+include "ground_2/insert_eq/insert_eq_0.ma".
include "basic_2/rt_transition/cpm.ma".
(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
) →
∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → R G L T1 T2.
#h #R #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T1 #T2
-* #c #HC #H generalize in match HC; -HC
-elim H -c -G -L -T1 -T2
-[ /2 width=3 by ex2_intro/
-| #G #L #s #H
- lapply (isrt_inv_01 … H) -H #H destruct
-| /3 width=4 by ex2_intro/
-| #c #G #L #V1 #V2 #W2 #_ #_ #_ #H
- elim (isrt_inv_plus_SO_dx … H) -H // #n #_ #H destruct
-| /3 width=4 by ex2_intro/
-| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV #IHT #H
- elim (isrt_O_inv_max … H) -H #HcV #HcT
- /4 width=3 by isr_inv_shift, ex2_intro/
-| #cV #cT #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #IHV #IHT #H
- elim (isrt_O_inv_max … H) -H #HcV #HcT
- /4 width=3 by isr_inv_shift, ex2_intro/
-| #cU #cT #G #L #U1 #U2 #T1 #T2 #HUT #HU12 #HT12 #IHU #IHT #H
- elim (isrt_O_inv_max … H) -H #HcV #HcT
- /3 width=3 by ex2_intro/
-| /4 width=4 by isrt_inv_plus_O_dx, ex2_intro/
-| /4 width=4 by isrt_inv_plus_O_dx, ex2_intro/
-| #c #G #L #U1 #U2 #T #_ #_ #H
- elim (isrt_inv_plus_SO_dx … H) -H // #n #_ #H destruct
-| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #IHV #IHW #IHT #H
- lapply (isrt_inv_plus_O_dx … H ?) -H // #H
- elim (isrt_O_inv_max … H) -H #H #HcT
- elim (isrt_O_inv_max … H) -H #HcV #HcW
- /4 width=3 by isr_inv_shift, ex2_intro/
-| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #IHV #IHW #IHT #H
- lapply (isrt_inv_plus_O_dx … H ?) -H // #H
- elim (isrt_O_inv_max … H) -H #H #HcT
- elim (isrt_O_inv_max … H) -H #HcV #HcW
- /4 width=4 by isr_inv_shift, ex2_intro/
+@(insert_eq_0 … 0) #n #H
+@(cpm_ind … H) -G -L -T1 -T2 -n /3 width=4 by/
+[ #G #L #s #H destruct
+| #n #G #K #V1 #V2 #W2 #_ #_ #_ #H destruct
+| #n #G #L #U1 #U2 #T #_ #_ #H destruct
]
qed-.
]
*)
[ { "context-sensitive parallel r-computation" * } {
-(*
- [ [ "" ] "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ]
-*)
+ [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_length" + "lprs_drops" (* + "lprs_cprs" + "lprs_lprs" *) * ]
+ [ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ]
[ [ "for terms" ] "cprs" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" "cprs_drops" (* + "cprs_cprs" *) * ]
}
]
[ { "t-bound context-sensitive parallel rt-computation" * } {
- [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_aaa" + "cpms_cpxs" * ]
+ [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpms_drops" + "cpms_lsubr" + "cpms_aaa" + "cpms_lpr" + "cpms_cpxs" + "cpms_cpms" * ]
}
]
[ { "unbound context-sensitive parallel rst-computation" * } {
lemma plus_inv_O3: ∀x,y. x + y = 0 → x = 0 ∧ y = 0.
/2 width=1 by plus_le_0/ qed-.
+lemma plus_inv_S3_sn: ∀x1,x2,x3. x1+x2 = ↑x3 →
+ ∨∨ ∧∧ x1 = 0 & x2 = ↑x3
+ | ∃∃y1. x1 = ↑y1 & y1 + x2 = x3.
+* /3 width=1 by or_introl, conj/
+#x1 #x2 #x3 <plus_S1 #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma plus_inv_S3_dx: ∀x2,x1,x3. x1+x2 = ↑x3 →
+ ∨∨ ∧∧ x2 = 0 & x1 = ↑x3
+ | ∃∃y2. x2 = ↑y2 & x1 + y2 = x3.
+* /3 width=1 by or_introl, conj/
+#x2 #x1 #x3 <plus_n_Sm #H destruct
+/3 width=3 by ex2_intro, or_intror/
+qed-.
+
lemma max_inv_O3: ∀x,y. (x ∨ y) = 0 → 0 = x ∧ 0 = y.
/4 width=2 by le_maxr, le_maxl, le_n_O_to_eq, conj/
qed-.
lapply (isrt_inj … Hn2 H2) -c2 #H destruct //
qed-.
+lemma isrt_inv_max_eq_t: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → eq_t c1 c2 →
+ ∧∧ 𝐑𝐓⦃n, c1⦄ & 𝐑𝐓⦃n, c2⦄.
+#n #c1 #c2 #H #Hc12
+elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
+lapply (isrt_eq_t_trans … Hc1 … Hc12) -Hc12 #H
+<(isrt_inj … H … Hc2) -Hc2
+<idempotent_max /2 width=1 by conj/
+qed-.
+
(* Properties with shift ****************************************************)
lemma max_shift: ∀c1,c2. ((↕*c1) ∨ (↕*c2)) = ↕*(c1∨c2).
* #ri1 #rs1 #ti1 #ts1 * #ri2 #rs2 #ti2 #ts2
<shift_rew <shift_rew <shift_rew <max_rew //
qed.
+
+(* Inversion lemmaswith shift ***********************************************)
+
+lemma isrt_inv_max_shift_sn: ∀n,c1,c2. 𝐑𝐓⦃n, ↕*c1 ∨ c2⦄ →
+ ∧∧ 𝐑𝐓⦃0, c1⦄ & 𝐑𝐓⦃n, c2⦄.
+#n #c1 #c2 #H
+elim (isrt_inv_max … H) -H #n1 #n2 #Hc1 #Hc2 #H destruct
+elim (isrt_inv_shift … Hc1) -Hc1 #Hc1 * -n1
+/2 width=1 by conj/
+qed-.
projects / helm.git / commitdiff