(* *)
(**************************************************************************)
-include "basic_2/rt_transition/cpm_aaa.ma".
include "basic_2/rt_computation/cpms_aaa.ma".
include "basic_2/dynamic/cnv.ma".
elim (cnv_fwd_aaa … H) -H #A #HA
/2 width=2 by aaa_cpm_SO/
qed-.
+
+(* Forward lemmas with t_bound rt_computation for terms *********************)
+
+lemma cnv_fwd_cpms_total (a) (h) (n) (G) (L):
+ ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
+#a #h #n #G #L #T #H
+elim (cnv_fwd_aaa … H) -H #A #HA
+/2 width=2 by aaa_cpms_total/
+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/rt_equivalence/cpcs_cprs.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Forward lemmas with r-equivalence ****************************************)
+
+lemma cnv_cpms_conf_eq (a) (h) (n) (G) (L):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] →
+ ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2.
+#a #h #n #G #L #T #HT #T1 #HT1 #T2 #HT2
+elim (cnv_cpms_conf … HT … HT1 … HT2) -T <minus_n_n #T #HT1 #HT2
+/2 width=3 by cprs_div/
+qed-.
+
+lemma cnv_cpms_fwd_appl_sn_decompose (a) (h) (G) (L):
+ ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → ∀n,X. ⦃G,L⦄ ⊢ ⓐV.T ➡*[n,h] X →
+ ∃∃U. ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X.
+#a #h #G #L #V #T #H0 #n #X #HX
+elim (cnv_inv_appl … H0) #m #p #W #U #_ #_ #HT #_ #_ -m -p -W -U
+elim (cnv_fwd_cpms_total … h n … HT) #U #HTU
+lapply (cpms_appl_dx … V V … HTU) [ // ] #H
+/3 width=8 by cnv_cpms_conf_eq, ex3_intro/
+qed-.
+++ /dev/null
-
-include "basic_2/rt_computation/cpms_lpr.ma".
-(*
-lemma cpm_lsubr_trans (h) (n) (G) (L1) (T1):
- ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[↑n,h] T2 → ∀L2. L1 ⫃ L2 →
- ∃∃T0. ⦃G,L2⦄ ⊢ T1 ➡[↑n,h] T0 & ⦃G,L2⦄ ⊢ T0 ➡*[h] T2.
-#h #m #G #L1 #T1 #T2
-@(insert_eq_0 … (↑m)) #n #H
-@(cpm_ind … H) -n -G -L1 -T1 -T2
-[
-|
-| #n #G #K1 #V1 #V2 #W2 #_ #IH #HVW2 #Hm #L2 #H destruct
- elim (lsubr_inv_bind1 … H) -H *
- [ #K2 #HK #H destruct
- elim (IH … HK) -K1 [| // ] #V0 #HV10 #HV02
- elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
- lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K2.ⓓV1) … HVW0 … HVW2) -V2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HW02
- /3 width=3 by cpm_delta, ex2_intro/
- | #K2 #VX #WX #HK #H1 #H2 destruct
- elim (IH … HK) -K1 [| // ] #X0 #H1 #H2
- elim (cpm_inv_cast1 … H1) -H1 [ * || * ]
- [ #W0 #V0 #HW0 #HV0 #H destruct
- @(ex2_intro … (#0)) [ // |
- | #I1 #I2 #K2 #VX #HK #H1 #H2 destruct
-
-|
-|
-| #n #p #I #G #L1 #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #L2 #HL
- elim (IHV … HL) -IHV #V0 #HV01 #HV02
- elim (IHT (L2.ⓑ{I}V1)) [| /2 width=1 by lsubr_bind/ ] -L1 #T0 #HT10 #HT02
- @(ex2_intro … (ⓑ{p,I}V1.T0)) /3 width=3 by cprs_step_sn, cpms_bind, cpm_bind/ (**) (* full auto a bit slow *)
-|
-|
-| //
-*)
-(*
-lemma cpr_cpm_trans_swap_lsubr_lpr (h) (G) (L1) (T1):
- ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L. L ⫃ L1 →
- ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 →
- ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[h] T2.
-#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1
-#G0 #L0 #T0 #IH #G #L1 * [| * [| * ]]
-[ (*
- #I #HG #HL #HT #X #H1 #L2 #HL12 #m2 #X2 #H2 destruct
- elim (cpr_inv_atom1 … H1) -H1 [|*: * ]
- [ #H destruct
- elim (cpm_inv_atom1 … H2) -H2 *
- [ #H1 #H2 destruct /3 width=3 by cpm_cpms, ex2_intro/
- | #s #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
- | #K2 #V #V2 #HV2 #HVT2 #H1 #H2 destruct
- elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #V1 #HK12 #HV1 #H destruct
- elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
- [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
- elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
- lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
- /3 width=3 by cpm_delta, ex2_intro/
- | #n2 #K2 #W #W2 #HW2 #HWT2 #H1 #H2 #H3 destruct
- elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #W1 #HK12 #HW1 #H destruct
- elim (IH … HW1 … HK12 … HW2) -K2 -W -IH
- [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #W0 #HW10 #HW02
- elim (lifts_total W0 (𝐔❴1❵)) #T0 #HWT0
- lapply (cpms_lifts_bi … HW02 (Ⓣ) … (K1.ⓛW1) … HWT0 … HWT2) -W2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
- /3 width=3 by cpm_ell, ex2_intro/
- | #I2 #K2 #T2 #i #HT2 #HTU2 #H1 #H2 destruct
- elim (lpr_inv_bind_dx … HL12) -HL12 #I1 #K1 #HK12 #_ #H destruct
- elim (IH … (#i) … HK12 … HT2) -I2 -K2 -IH
- [|*: /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
- elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
- lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
- /3 width=3 by cpm_lref, ex2_intro/
- ]
- | #K1 #V1 #V #HV1 #HVT #H1 #H2 destruct
- elim (lpr_inv_pair_sn … HL12) -HL12 #K2 #V0 #HK12 #_ #H destruct
- elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HVT) -X
- [|*: /3 width=2 by drops_refl, drops_drop/ ] -V0 #V2 #HVT2 #HV2
- elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
- [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
- elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
- lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
- /3 width=3 by cpm_delta, ex2_intro/
- | #I1 #K1 #T #i #HT1 #HTU #H1 #H2 destruct
- elim (lpr_inv_bind_sn … HL12) -HL12 #I2 #K2 #HK12 #_ #H destruct
- elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HTU) -X
- [|*: /3 width=2 by drops_refl, drops_drop/ ] -I2 #T2 #HTU2 #HT2
- elim (IH … HT1 … HK12 … HT2) -K2 -T -IH
- [| /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
- elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
- lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
- /3 width=3 by cpm_lref, ex2_intro/
- ]
-*)
-| (*
- #p #I #V1 #T1 #HG #HL #HT #X #H1 #L2 #HL12 #n2 #X2 #H2
- elim (cpm_inv_bind1 … H1) -H1 *
- [ #V #T #HV1 #HT1 #H destruct
- elim (cpm_inv_bind1 … H2) -H2 *
- [ #V2 #T2 #HV2 #HT2 #H destruct
- elim (IH … HT1 … HT2) -T
- [|*: /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
- elim (IH … HV1 … HL12 … HV2) -L2 -V -IH
- [| // ] #V0 #HV10 #HV02
- /4 width=7 by cpms_bind, cpms_step_sn, cpm_bind, ex2_intro/
- | #X #HXT #HX2 #H1 #H2 destruct
- elim (cpm_lifts_sn … HX2 (Ⓣ) … (L2.ⓓV) … HXT) -HX2
- [| /3 width=2 by drops_refl, drops_drop/ ] #T2 #HXT2 #HT2
- elim (IH … HT1 … HT2) -HT2 -IH
- [|*: /2 width=1 by lpr_pair/ ] -L2 #T0 #HT10 #HT02
- /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/
- ]
- | #X1 #HXT1 #HX1 #H1 #H2 destruct
- elim (IH … HX1 … HL12 … H2) -L2 -X -IH
- [| /2 width=1 by fqup_zeta/ ] #X0 #HX10 #HX02
- /3 width=3 by cpm_zeta, ex2_intro/
- ]
-*)
-| #V1 #T1 #HG #HL #HT #X #H1 #L #HL1 #L2 #HL2 #m2 #X2 #H2 destruct
- elim (cpm_inv_appl1 … H1) -H1 *
- [ (*
- #V #T #HV1 #HT1 #H destruct
- elim (cpm_inv_appl1 … H2) -H2 *
- [ #V2 #T2 #HV2 #HT2 #H destruct
- elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
- elim (IH … HT1 … HL12 … HT2) -L2 -T -IH [| // ] #T0 #HT10 #HT02
- /3 width=5 by cpms_appl, cpm_appl, ex2_intro/
- | #q #V2 #WX #W2 #TX #T2 #HV2 #HW2 #HT2 #H1 #H2 destruct
- elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
- elim (IH … HT1 … HL12 m2 (ⓛ{q}W2.T2)) -IH -HT1
- [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
- /4 width=9 by cprs_step_dx, cpms_appl, cpm_beta, cpm_appl, ex2_intro/
- | #q #V2 #U2 #WX #W2 #TX #T2 #HV2 #HVU2 #HW2 #HT2 #H1 #H2 destruct
- elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
- elim (IH … HT1 … HL12 m2 (ⓓ{q}W2.T2)) -IH -HT1
- [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
- /4 width=11 by cprs_step_dx, cpms_appl, cpm_theta, cpm_appl, ex2_intro/
- ]
- *)
- | #p #V #W1 #W #TX1 #T #HV1 #HW1 #HT1 #H1 #H3 destruct
- elim (cpm_inv_abbr1 … H2) -H2 *
- [ #X3 #T2 #H2 #HT2 #H destruct
- elim (cpr_inv_cast1 … H2) -H2 [ * ]
- [ #W2 #V2 #HW2 #HV2 #H destruct
- elim (IH … HT1 (L.ⓓⓝW1.V1) … HT2) -T
- [|*: /4 width=3 by lsubr_beta, lpr_pair, cpm_cast, lsubr_cpm_trans/ ] #T0 #HT10 #HT02
- elim (IH … HV1 … HL1 … HL2 … HV2) -V [| // ] #V0 #HV10 #HV02
- elim (IH … HW1 … HL1 … HL2 … HW2) -L2 -W -IH [| // ] #W0 #HW10 #HW02
- @(ex2_intro … (ⓓ{p}ⓝW1.V1.T0))
- [ @cpm_beta //
-
- /2 width=1 by cpm_beta/
- | /3 width=7 by cprs_step_dx, cpms_appl, cpm_beta/
-
- @cprs_step_dx [| @(cpms_appl … HT02 … HV02) | /2 width=1 by cpm_beta/
- @cpms_beta
-*)
+++ /dev/null
- D I
-sort * *
-lref ldef * *
-lref ldec * *
-lref lref * *
-lref ldef drops * *
-lref ldec drops * *
-gref *
-bind * *
-appl appl * *
-appl beta *
-appl pure *
-cast new * *
-cast old * *
-conv *
(* Properties with rt_computation for terms *********************************)
(* Basic_2A1: was by definition nta_appl ntaa_appl *)
-lemma nta_beta (a) (h) (p) (G) (L):
- ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W →
- ∀T,U. ⦃G,L⦄ ⊢ ⓛ{p}W.T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U.
-#a #h #p #G #L #V #W #H1 #T #U #H2
+lemma nta_beta (a) (h) (p) (G) (K):
+ ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
+ ∀T,U. ⦃G,K.ⓛW⦄ ⊢ T :[a,h] U → ⦃G,K⦄ ⊢ ⓐV.ⓛ{p}W.T :[a,h] ⓐV.ⓛ{p}W.U.
+#a #h #p #G #K #V #W #H1 #T #U #H2
elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
-/4 width=7 by cnv_cast, cnv_appl, cpms_bind, cpms_appl_dx/
+/4 width=7 by cnv_bind, cnv_appl, cnv_cast, cpms_appl_dx, cpms_bind_dx/
qed.
(* Basic_1: was by definition: ty3_appl *)
(* Basic_2A1: was nta_appl_old *)
-lemma nta_appl (h) (p) (G) (L):
- ∀V,W. ⦃G,L⦄ ⊢ V :[h] W →
- ∀T,U. ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[h] ⓐV.ⓛ{p}W.U.
-#h #p #G #L #V #W #H1 #T #U #H2
+lemma nta_appl (a) (h) (p) (G) (L):
+ ∀V,W. ⦃G,L⦄ ⊢ V :[a,h] W →
+ ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T :[a,h] ⓐV.ⓛ{p}W.U.
+#a #h #p #G #L #V #W #H1 #T #U #H2
elim (cnv_inv_cast … H1) -H1 #X1 #HW #HV #HWX1 #HVX1
elim (cnv_inv_cast … H2) -H2 #X2 #HU #HT #HUX2 #HTX2
elim (cpms_inv_abst_sn … HUX2) #W0 #U0 #HW0 #HU0 #H destruct
+++ /dev/null
-(*
-(* Advanced forvard lemmas **************************************************)
-
-lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
- ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
-/2 width=3/ qed-.
-
-*)
/4 width=4 by nta_cast/
]
qed-.
+
+lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
+ (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+ (∀G,K,V,W,U.
+ ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
+ Q G K V W → Q G (K.ⓓV) (#0) U
+ ) →
+ (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (∀I,G,K,W,U,i.
+ ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U →
+ Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
+ ) →
+ (∀p,I,G,K,V,T,U.
+ ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U →
+ Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
+ ) →
+ (∀p,G,L,V,W,T,U.
+ ⦃G,L⦄ ⊢ V :*[h] W → ⦃G,L⦄ ⊢ T :*[h] ⓛ{p}W.U →
+ Q G L V W → Q G L T (ⓛ{p}W.U) → Q G L (ⓐV.T) (ⓐV.ⓛ{p}W.U)
+ ) →
+ (∀G,L,V,T,U.
+ ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] →
+ Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
+ ) →
+ (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U
+ ) →
+ (∀G,L,T,U1,U2.
+ ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] →
+ Q G L T U1 → Q G L T U2
+ ) →
+ ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T
+@(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ]
+[ #s #HG #HL #HT #X #H destruct -IH
+ elim (nta_inv_sort_sn … H) -H #HUX #HX
+ /2 width=4 by/
+| * [| #i ] #HG #HL #HT #X #H destruct
+ [ elim (nta_inv_lref_sn_drops_cnv … H) -H *
+ [ #K #V #W #U #H #HVW #HWU #HUX #HX
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /5 width=7 by nta_ldef, fqu_fqup, fqu_lref_O/
+ | #K #W #U #H #HW #HWU #HUX #HX
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /3 width=4 by nta_ldec_cnv/
+ ]
+ | elim (nta_inv_lref_sn … H) -H #I #K #T #U #HT #HTU #HUX #HX #H destruct
+ /5 width=7 by nta_lref, fqu_fqup/
+ ]
+| #l #HG #HL #HT #U #H destruct -IH
+ elim (nta_inv_gref_sn … H)
+| #p #I #V #T #HG #HL #HT #X #H destruct
+ elim (nta_inv_bind_sn_cnv … H) -H #U #HV #HTU #HUX #HX
+ /4 width=5 by nta_bind_cnv/
+| #V #T #HG #HL #HT #X #H destruct
+ elim (nta_inv_pure_sn_cnv … H) -H *
+ [ #p #W #U #HVW #HTU #HUX #HX
+ /4 width=9 by nta_appl/
+ | #U #HTU #HVU #HUX #HX
+ /4 width=6 by nta_pure_cnv/
+ ]
+| #U #T #HG #HL #HT #X #H destruct
+ elim (nta_inv_cast_sn … H) -H #HTU #HUX #HX
+ /4 width=4 by nta_cast/
+]
+qed-.
+
+lemma nta_ind_ext_cnv (h) (Q:relation4 …):
+ (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
+ (∀G,K,V,W,U.
+ ⦃G,K⦄ ⊢ V :*[h] W → ⬆*[1] W ≘ U →
+ Q G K V W → Q G (K.ⓓV) (#0) U
+ ) →
+ (∀G,K,W,U. ⦃G,K⦄ ⊢ W !*[h] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+ (∀I,G,K,W,U,i.
+ ⦃G,K⦄ ⊢ #i :*[h] W → ⬆*[1] W ≘ U →
+ Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
+ ) →
+ (∀p,I,G,K,V,T,U.
+ ⦃G,K⦄ ⊢ V !*[h] → ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h] U →
+ Q G (K.ⓑ{I}V) T U → Q G K (ⓑ{p,I}V.T) (ⓑ{p,I}V.U)
+ ) →
+ (∀p,G,K,V,W,T,U.
+ ⦃G,K⦄ ⊢ V :*[h] W → ⦃G,K.ⓛW⦄ ⊢ T :*[h] U →
+ Q G K V W → Q G (K.ⓛW) T U → Q G K (ⓐV.ⓛ{p}W.T) (ⓐV.ⓛ{p}W.U)
+ ) →
+ (∀G,L,V,T,U.
+ ⦃G,L⦄ ⊢ T :*[h] U → ⦃G,L⦄ ⊢ ⓐV.U !*[h] →
+ Q G L T U → Q G L (ⓐV.T) (ⓐV.U)
+ ) →
+ (∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U → Q G L (ⓝU.T) U
+ ) →
+ (∀G,L,T,U1,U2.
+ ⦃G,L⦄ ⊢ T :*[h] U1 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 !*[h] →
+ Q G L T U1 → Q G L T U2
+ ) →
+ ∀G,L,T,U. ⦃G,L⦄ ⊢ T :*[h] U → Q G L T U.
+#h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #IH8 #IH9 #G #L #T #U #H
+@(nta_ind_ext_cnv_mixed … IH1 IH2 IH3 IH4 IH5 … IH7 IH8 IH9 … H) -G -L -T -U -IH1 -IH2 -IH3 -IH4 -IH5 -IH6 -IH8 -IH9
+#p #G #L #V #W #T #U #HVW #HTU #_ #IHTU
+lapply (nta_fwd_cnv_dx … HTU) #H
+elim (cnv_inv_bind … H) -H #_ #HU
+elim (cnv_nta_sn … HU) -HU #X #HUX
+/4 width=2 by nta_beta, nta_fwd_cnv_sn/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_equivalence/cpcs_cprs.ma".
-include "basic_2/dynamic/cnv_preserve.ma".
+include "basic_2/rt_equivalence/cpcs_cpcs.ma".
+include "basic_2/dynamic/cnv_cpcs.ma".
include "basic_2/dynamic/nta.ma".
(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
lapply (cpms_step_dx … HTU 1 (ⓛ{p}W.U0) ?) -HTU [ /2 width=1 by cpm_bind/ ] #HTU
| lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Hn #H destruct
]
-lapply (cpms_appl_dx … V V … HTU) [1,3: // ] #HVTU
-elim (cnv_cpms_conf … H1 … H2 … HVTU) -H1 -H2 -HVTU <minus_n_n #X0 #HX0 #HUX0
-@ex4_3_intro [6,13: |*: /2 width=5 by cnv_cpms_nta/ ]
-/3 width=5 by cprs_div, cprs_trans/
+/5 width=11 by cnv_cpms_nta, cnv_cpms_conf_eq, cpcs_cprs_div, cpms_appl_dx, ex4_3_intro/
qed-.
-(*
- (ltc_ind
- :∀A: Type \sub 0
- .(A→A→A)
- →∀B: Type \sub 0
- .relation3 A B B
- →∀Q_:∀x_3:A.∀x_2:B.∀x_1:B.ltc A __6 B __4 x_3 x_2 x_1→Prop
- .(∀a:A
- .∀b1:B
- .∀b2:B.∀x_5:__5 a b1 b2.Q_ a b1 b2 (ltc_rc A __8 B __6 a b1 b2 x_5))
- →(∀a1:A
- .∀a2:A
- .∀b1:B
- .∀b:B
- .∀b2:B
- .∀x_7:ltc A __10 B __8 a1 b1 b
- .∀x_6:ltc A __11 B __9 a2 b b2
- .Q_ a1 b1 b x_7
- →Q_ a2 b b2 x_6
- →Q_ (__14 a1 a2) b1 b2
- (ltc_trans A __14 B __12 a1 a2 b1 b b2 x_7 x_6))
- →∀x_3:A
- .∀x_2:B.∀x_1:B.∀x_4:ltc A __9 B __7 x_3 x_2 x_1.Q_ x_3 x_2 x_1 x_4)
+(* Basic_2A1: uses: nta_fwd_pure1 *)
lemma nta_inv_pure_sn_cnv (h) (G) (L) (X2):
∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :*[h] X2 →
- ∨∨ ∃∃p,W,T0,U0. ⦃G,L⦄ ⊢ V :*[h] W & ⦃G,L⦄ ⊢ ⓛ{p}W.T0 :*[h] ⓛ{p}W.U0 & ⦃G,L⦄ ⊢ T ➡*[h] ⓛ{p}W.T0 & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U0 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h]
+ ∨∨ ∃∃p,W,U. ⦃G,L⦄ ⊢ V :*[h] W & ⦃G,L⦄ ⊢ T :*[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h]
| ∃∃U. ⦃G,L⦄ ⊢ T :*[h] U & ⦃G,L⦄ ⊢ ⓐV.U !*[h] & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h].
#h #G #L #X2 #V #T #H
elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H
-elim (cnv_inv_appl … H1) -H1 * [| #n ] #p #W0 #T0 #_ #HV #HT #HW0 #HT0
-lapply (cnv_cpms_trans … HT … HT0) #H
-elim (cnv_inv_bind … H) -H #_ #H1T0
-[ elim (cpms_inv_appl_sn_decompose … H) -H #U #HTU #HUX1
-
-
- [ #V0 #U0 #HV0 #HU0 #H destruct
- elim (cnv_cpms_conf … HT … HT0 … HU0)
- <minus_O_n <minus_n_O #X #H #HU0X
- elim (cpms_inv_abst_sn … H) -H #W1 #U1 #HW01 #HU01 #H destruct
- @or_introl
- @(ex5_4_intro … U1 … HT0 … HX2) -HX2
- [ /2 width=1 by cnv_cpms_nta/
- | @nta_bind_cnv /2 width=4 by cnv_cpms_trans/ /2 width=3 by cnv_cpms_nta/
- | @(cpcs_cprs_div … HX21) -HX21
- @(cprs_div … (ⓐV0.ⓛ{p}W1.U1))
- /3 width=1 by cpms_appl, cpms_appl_dx, cpms_bind/
- ]
-*)
+elim (cnv_inv_appl … H1) * [| #n ] #p #W0 #T0 #Hn #HV #HT #HW0 #HT0
+[ lapply (cnv_cpms_trans … HT … HT0) #H0
+ elim (cnv_inv_bind … H0) -H0 #_ #HU
+ elim (cnv_fwd_cpm_SO … HU) #U0 #HU0 -HU
+ lapply (cpms_step_dx … HT0 1 (ⓛ{p}W0.U0) ?) -HT0 [ /2 width=1 by cpm_bind/ ] #HT0
+ lapply (cpms_appl_dx … V V … HT0) [ // ] #HTU0
+ lapply (cnv_cpms_conf_eq … H1 … HTU0 … H) -H1 -H -HTU0 #HU0X1
+ /4 width=8 by cnv_cpms_nta, cpcs_cprs_div, ex4_3_intro, or_introl/
+| elim (cnv_cpms_fwd_appl_sn_decompose … H1 … H) -H1 -H #X0 #_ #H #HX01
+ elim (cpms_inv_plus … 1 n … HT0) #U #HTU #HUT0
+ lapply (cnv_cpms_trans … HT … HTU) #HU
+ lapply (cnv_cpms_conf_eq … HT … HTU … H) -H #HUX0
+ @or_intror @(ex4_intro … U … HX2) -HX2
+ [ /2 width=1 by cnv_cpms_nta/
+ | /4 width=7 by cnv_appl, lt_to_le/
+ | /4 width=3 by cpcs_trans, cpcs_cprs_div, cpcs_flat/
+ ]
+]
+qed-.
+
(* Basic_2A1: uses: nta_inv_cast1 *)
lemma nta_inv_cast_sn (a) (h) (G) (L) (X2):
∀U,T. ⦃G,L⦄ ⊢ ⓝU.T :[a,h] X2 →
elim (cnv_inv_cast … H1) #X #HU #HT #HUX #HTX
elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
[ #U0 #T0 #HU0 #HT0 #H destruct -HU -HU0
- elim (cnv_cpms_conf … HT … HTX … HT0) -HT -HTX -HT0
- <minus_n_n #T1 #HXT1 #HT01
- @and3_intro // @(cprs_div … T1) /3 width=4 by cprs_trans, cpms_eps/ (**) (* full auto too slow *)
+ lapply (cnv_cpms_conf_eq … HT … HTX … HT0) -HT -HT0 -HTX #HXT0
+ lapply (cprs_step_dx … HX20 T0 ?) -HX20 [ /2 width=1 by cpm_eps/ ] #HX20
| #HTX0 -HU
- elim (cnv_cpms_conf … HT … HTX … HTX0) -HT -HTX -HTX0
- <minus_n_n #T1 #HXT1 #HXT01
- @and3_intro // @(cprs_div … T1) /2 width=3 by cprs_trans/ (**) (* full auto too slow *)
+ lapply (cnv_cpms_conf_eq … HT … HTX … HTX0) -HT -HTX -HTX0 #HX0
| #m #HUX0 #H destruct -HT -HTX
- elim (cnv_cpms_conf … HU … HUX … HUX0) -HU -HUX0
- <minus_n_n #U1 #HXU1 #HXU01
- @and3_intro // @(cprs_div … U1) /2 width=3 by cprs_trans/ (**) (* full auto too slow *)
+ lapply (cnv_cpms_conf_eq … HU … HUX … HUX0) -HU -HUX0 #HX0
]
+/4 width=3 by cpcs_cprs_div, cpcs_cprs_step_sn, and3_intro/
qed-.
(* Basic_1: uses: ty3_gen_cast *)
elim (cnv_inv_cast … H1) #X #HT1 #HT0 #HT1X #HT0X
elim (cpms_inv_cast1 … H2) -H2 [ * || * ]
[ #U1 #U0 #HTU1 #HTU0 #H destruct
- elim (cnv_cpms_conf … HT0 … HT0X … HTU0) -HT0 -HT0X -HTU0
- <minus_n_n #X0 #HX0 #HUX0
- lapply (cprs_trans … HT1X … HX0) -X #HT1X0
- /5 width=7 by cnv_cpms_nta, cpcs_cprs_div, cprs_div, cpms_cast, ex4_intro/
+ lapply (cnv_cpms_conf_eq … HT0 … HT0X … HTU0) -HT0 -HT0X -HTU0 #HXU0
+ /5 width=5 by cnv_cpms_nta, cpcs_cprs_div, cpcs_cprs_step_sn, cpcs_flat, ex4_intro/
| #HTX0
- elim (cnv_cpms_conf … HT0 … HT0X … HTX0) -HT0 -HT0X -HTX0
- <minus_n_n #X1 #HX1 #HX01
elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1
- lapply (cprs_trans … HT1X … HX1) -X #HTX1
- lapply (cprs_trans … HX20 … HX01) -X0 #HX21
- /4 width=5 by cprs_div, cpms_eps, ex4_intro/
+ lapply (cnv_cpms_conf_eq … HT0 … HT0X … HTX0) -HT0 -HT0X -HTX0 #HX0
+ lapply (cprs_step_sn … (ⓝU1.T1) … HT1X) -HT1X [ /2 width=1 by cpm_eps/ ] #HT1X
+ /4 width=5 by cpcs_cprs_div, cpcs_cprs_step_sn, ex4_intro/
| #n #HT1X0 #H destruct -X -HT0
elim (cnv_nta_sn … HT1) -HT1 #U1 #HTU1
/4 width=5 by cprs_div, cpms_eps, ex4_intro/
#a #h #G #L #T #U1 #H1 #U2 #H2
elim (cnv_inv_cast … H1) -H1 #X1 #_ #_ #HUX1 #HTX1
elim (cnv_inv_cast … H2) -H2 #X2 #_ #HT #HUX2 #HTX2
-elim (cnv_cpms_conf … HT … HTX1 … HTX2) -T <minus_n_n #X #HX1 #HX2
-/3 width=5 by cprs_div, cprs_trans/
+lapply (cnv_cpms_conf_eq … HT … HTX1 … HTX2) -T #HX12
+/3 width=3 by cpcs_cprs_div, cpcs_cprs_step_sn/
qed-.
--- /dev/null
+lemma nta_inv_pure_sn_cnv (h) (G) (L) (X2):
+ ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :*[h] X2 →
+ ∨∨ ∃∃p,W,T0,U0. ⦃G,L⦄ ⊢ V :*[h] W & ⦃G,L.ⓛW⦄ ⊢ T0 :*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[h] ⓛ{p}W.T0 & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U0 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h]
+ | ∃∃U. ⦃G,L⦄ ⊢ T :*[h] U & ⦃G,L⦄ ⊢ ⓐV.U !*[h] & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 !*[h].
+#h #G #L #X2 #V #T #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H
+elim (cnv_inv_appl … H1) * [| #n ] #p #W0 #T0 #Hn #HV #HT #HW0 #HT0
+[ lapply (cpms_appl_dx … V V … HT0) // #H0
+ lapply (cnv_cpms_trans … H1 … H0) #H2
+ elim (cnv_cpms_conf … H1 … H … H0) -H1 -H -H0
+ <minus_O_n <minus_n_O #X #HX #HT0X
+ lapply (cprs_trans … HX21 … HX) -X1 #H1X2
+ elim (cnv_cpms_fwd_appl_sn_decompose … H2 … HT0X) -H2 -HT0X #X0 #H #HTX0 #HX0
+ elim (cnv_inv_bind … H) -H #_ #H1T0
+ elim (cpms_inv_abst_sn_cprs … HTX0) -HTX0 #U0 #HTU0 #HUX0
+ @or_introl @(ex5_4_intro … U0 … HT0 … HX2)
+ [ /2 width=1 by cnv_cpms_nta/
+ | /3 width=1 by cnv_cpms_nta/
+ | /4 width=3 by cpcs_cprs_div, cpcs_cprs_step_sn, cpms_appl_dx/
+ ]
+| elim (cnv_cpms_fwd_appl_sn_decompose … H1 … H) -H1 -H #X0 #_ #H #HX01
+ elim (cpms_inv_plus … 1 n … HT0) #U #HTU #HUT0
+ lapply (cnv_cpms_trans … HT … HTU) #HU
+ lapply (cnv_cpms_conf_eq … HT … HTU … H) -H #HUX0
+ @or_intror @(ex4_intro … U … HX2) -HX2
+ [ /2 width=1 by cnv_cpms_nta/
+ | /4 width=7 by cnv_appl, lt_to_le/
+ | /4 width=3 by cpcs_trans, cpcs_cprs_div, cpcs_flat/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
+include "basic_2/rt_transition/cpm_aaa.ma".
include "basic_2/rt_computation/cpxs_aaa.ma".
include "basic_2/rt_computation/cpms_cpxs.ma".
(* Basic_2A1: includes: cprs_aaa_conf *)
lemma cpms_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpms h G L n).
/3 width=5 by cpms_fwd_cpxs, cpxs_aaa_conf/ qed-.
+
+lemma aaa_cpms_total (h) (G) (L) (n) (A):
+ ∀T. ⦃G, L⦄ ⊢ T ⁝ A → ∃U. ⦃G,L⦄ ⊢ T ➡*[n,h] U.
+#h #G #L #n elim n -n
+[ /2 width=3 by ex_intro/
+| #n #IH #A #T1 #HT1 <plus_SO
+ elim (IH … HT1) -IH #T0 #HT10
+ lapply (cpms_aaa_conf … HT1 … HT10) -HT1 #HT0
+ elim (aaa_cpm_SO h … HT0) -HT0 #T2 #HT02
+ /3 width=4 by cpms_step_dx, ex_intro/
+]
+qed-.
lapply (cpms_trans … HT1 … HT2) -T <commutative_plus #HT12
/2 width=1 by cpms_inv_plus/
qed-.
-
-(* More advanced inversion lemmas *******************************************)
-(*
-lemma cpms_inv_appl_sn_decompose (h) (n) (G) (L) (V1) (T1):
- ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ➡*[n,h] X2 →
- ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 & ⦃G,L⦄ ⊢ ⓐV1.T2 ➡*[h] X2.
-#h #n #G #L #V1 #T1 #X2 #H
-@(cpms_ind_dx … H) -n -X2
-[ /2 width=3 by ex2_intro/
-| #n1 #n2 #X #X2 #_ * #X1 #HTX1 #HX1 #HX2
- elim (pippo … HX1 … HX2) -X #X #HX1 #HX2
- elim (cpm_inv_appl_sn_decompose … HX1) -HX1 #U1 #HXU1 #HU1X
- /3 width=5 by cprs_step_sn, cpms_step_dx, ex2_intro/
-]
-qed-.
-*)
/5 width=7 by lprs_cpm_trans, lprs_pair, cprs_step_dx, cpms_trans, ex3_2_intro/
qed-.
+lemma cpms_inv_abst_sn_cprs (h) (n) (p) (G) (L) (W):
+ ∀T,X. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡*[n,h] X →
+ ∃∃U. ⦃G,L.ⓛW⦄⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓛ{p}W.U ➡*[h] X.
+#h #n #p #G #L #W #T #X #H
+elim (cpms_inv_abst_sn … H) -H #W0 #U #HW0 #HTU #H destruct
+@(ex2_intro … HTU) /2 width=1 by cpms_bind/
+qed-.
+
(* Basic_2A1: includes: cprs_inv_abst *)
lemma cpms_inv_abst_bi (n) (h) (G) (L):
∀p,W1,W2,T1,T2. ⦃G, L⦄ ⊢ ⓛ{p}W1.T1 ➡*[n, h] ⓛ{p}W2.T2 →
]
qed-.
-(* Advanced inversion lemmas ************************************************)
-
-lemma cpm_inv_appl_sn_decompose (h) (n) (G) (L) (V1) (T1):
- ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ➡[n,h] X2 →
- ∃∃T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 & ⦃G,L⦄ ⊢ ⓐV1.T2 ➡[h] X2.
-#h #n #G #L #V1 #T1 #X2 #H
-elim (cpm_inv_appl1 … H) -H *
-[ #V2 #T2 #HV12 #HT12 #H destruct
- /3 width=3 by cpm_appl, ex2_intro/
-| #p #V2 #W1 #W2 #U1 #U2 #HV12 #HW12 #HU12 #H1 #H2 destruct
- /3 width=5 by cpm_beta, cpm_bind, ex2_intro/
-| #p #V2 #V0 #W1 #W2 #U1 #U2 #HV12 #HV20 #HW12 #HU12 #H1 #H2 destruct
- /3 width=5 by cpm_theta, cpm_bind, ex2_intro/
-]
-qed-.
-
(* Basic forward lemmas *****************************************************)
(* Basic_2A1: includes: cpr_fwd_bind1_minus *)
for native type assignment.
</news>
-->
+ <news class="alpha" date="2018 November 1.">
+ Extended (λδ-2) and restricted (λδ-1) type rules justified.
+ </news>
<news class="alpha" date="2018 September 21.">
λδ-2A completed with
confluence of rt-computation and
]
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_preserve_sub" + "cnv_preserve" * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" * ]
}
]
}
projects / helm.git / commitdiff