--- /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
+*)
D I
sort * *
-lref ldef *
-lref ldec *
-lref lref *
-lref ldef drops *
-lref ldec drops *
+lref ldef * *
+lref ldec * *
+lref lref * *
+lref ldef drops * *
+lref ldec drops * *
+gref *
bind * *
appl appl * *
appl beta *
/3 width=3 by cnv_cast, cpms_eps/
qed.
+(* Basic inversion lemmas ***************************************************)
+
+lemma nta_inv_gref_sn (a) (h) (G) (L):
+ ∀X2,l. ⦃G,L⦄ ⊢ §l :[a,h] X2 → ⊥.
+#a #h #G #L #X2 #l #H
+elim (cnv_inv_cast … H) -H #X #_ #H #_ #_
+elim (cnv_inv_gref … H)
+qed-.
+
(* Basic_forward lemmas *****************************************************)
lemma nta_fwd_cnv_sn (a) (h) (G) (L):
(* Basic_1: was: ty3_gen_sort *)
(* Basic_2A1: was: nta_inv_sort1 *)
lemma nta_inv_sort_sn (a) (h) (G) (L) (X2):
- ∀s. ⦃G,L⦄ ⊢ ⋆s :[a,h] X2 → ⦃G,L⦄ ⊢ ⋆(next h s) ⬌*[h] X2.
+ ∀s. ⦃G,L⦄ ⊢ ⋆s :[a,h] X2 →
+ ∧∧ ⦃G,L⦄ ⊢ ⋆(next h s) ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
#a #h #G #L #X2 #s #H
elim (cnv_inv_cast … H) -H #X1 #HX2 #_ #HX21 #H
lapply (cpms_inv_sort1 … H) -H #H destruct
-/2 width=1 by cpcs_cprs_sn/
+/3 width=1 by cpcs_cprs_sn, conj/
+qed-.
+
+lemma nta_inv_ldec_sn_cnv (a) (h) (G) (K) (V):
+ ∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 :[a,h] X2 →
+ ∃∃U. ⦃G,K⦄ ⊢ V ![a,h] & ⬆*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![a,h].
+#a #h #G #Y #X #X2 #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
+elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct
+elim (cpms_inv_ell_sn … H2) -H2 *
+[ #_ #H destruct
+| #m #W #HVW #HWX1 #H destruct
+ elim (lifts_total V (𝐔❴1❵)) #U #HVU
+ lapply (cpms_lifts_bi … HVW (Ⓣ) … (K.ⓛV) … HVU … HWX1) -W
+ [ /3 width=1 by drops_refl, drops_drop/ ] #HUX1
+ /3 width=5 by cprs_div, ex4_intro/
+]
qed-.
(*
-(* Advanced inversion lemmas ************************************************)
-
-
-(* Basic_1: was ty3_gen_lref *)
-lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
- (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
- ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ) ∨
- (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
- ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ).
-/2 width=3/ qed-.
-
(* 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-.
-lemma nta_ind_alt: ∀h. ∀R:lenv→relation term.
- (∀L,k. R L ⋆k ⋆(next h k)) →
- (∀L,K,V,W,U,i.
- ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
- R K V W → R L (#i) U
- ) →
- (∀L,K,W,V,U,i.
- ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
- R K W V → R L (#i) U
- ) →
- (∀I,L,V,W,T,U.
- ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
- R L V W → R (L.ⓑ{I}V) T U → R L (ⓑ{I}V.T) (ⓑ{I}V.U)
- ) →
- (∀L,V,W,T,U.
- ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
- R L V W →R L (ⓛW.T) (ⓛW.U) →R L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
- ) →
- (∀L,V,W,T,U.
- ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
- R L T U → R L (ⓐV.U) W → R L (ⓐV.T) (ⓐV.U)
- ) →
- (∀L,T,U,W.
- ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
- R L T U → R L U W → R L (ⓝU.T) U
- ) →
- (∀L,T,U1,U2,V2.
- ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
- R L T U1 →R L U2 V2 →R L T U2
- ) →
- ∀L,T,U. ⦃h, L⦄ ⊢ T : U → R L T U.
-#h #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #L #T #U #H elim (nta_ntaa … H) -L -T -U
-// /3 width=1 by ntaa_nta/ /3 width=3 by ntaa_nta/ /3 width=4 by ntaa_nta/
-/3 width=7 by ntaa_nta/
-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/dynamic/nta_drops.ma".
+include "basic_2/dynamic/nta_cpms.ma".
+include "basic_2/dynamic/nta_cpcs.ma".
+include "basic_2/dynamic/nta_preserve.ma".
+
+(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
+
+(* Advanced eliminators *****************************************************)
+
+lemma nta_ind_rest_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,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,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 #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_appl_sn … H) -H #p #W #U #HVW #HTU #HUX #HX
+ /4 width=9 by nta_appl/
+| #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-.
(* Inversion lemmas based on preservation ***********************************)
+lemma nta_inv_ldef_sn (a) (h) (G) (K) (V):
+ ∀X2. ⦃G,K.ⓓV⦄ ⊢ #0 :[a,h] X2 →
+ ∃∃W,U. ⦃G,K⦄ ⊢ V :[a,h] W & ⬆*[1] W ≘ U & ⦃G,K.ⓓV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓓV⦄ ⊢ X2 ![a,h].
+#a #h #G #Y #X #X2 #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
+elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct
+elim (cpms_inv_delta_sn … H2) -H2 *
+[ #_ #H destruct
+| #W #HVW #HWX1
+ /3 width=5 by cnv_cpms_nta, cpcs_cprs_sn, ex4_2_intro/
+]
+qed-.
+
+lemma nta_inv_lref_sn (a) (h) (G) (L):
+ ∀X2,i. ⦃G,L⦄ ⊢ #↑i :[a,h] X2 →
+ ∃∃I,K,T2,U2. ⦃G,K⦄ ⊢ #i :[a,h] T2 & ⬆*[1] T2 ≘ U2 & ⦃G,K.ⓘ{I}⦄ ⊢ U2 ⬌*[h] X2 & ⦃G,K.ⓘ{I}⦄ ⊢ X2 ![a,h] & L = K.ⓘ{I}.
+#a #h #G #L #X2 #i #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
+elim (cnv_inv_lref … H1) -H1 #I #K #Hi #H destruct
+elim (cpms_inv_lref_sn … H2) -H2 *
+[ #_ #H destruct
+| #X #HX #HX1
+ /3 width=9 by cnv_cpms_nta, cpcs_cprs_sn, ex5_4_intro/
+]
+qed-.
+
+lemma nta_inv_lref_sn_drops_cnv (a) (h) (G) (L):
+ ∀X2, i. ⦃G,L⦄ ⊢ #i :[a,h] X2 →
+ ∨∨ ∃∃K,V,W,U. ⬇*[i] L ≘ K.ⓓV & ⦃G,K⦄ ⊢ V :[a,h] W & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h]
+ | ∃∃K,W,U. ⬇*[i] L ≘ K. ⓛW & ⦃G,K⦄ ⊢ W ![a,h] & ⬆*[↑i] W ≘ U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
+#a #h #G #L #X2 #i #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
+elim (cnv_inv_lref_drops … H1) -H1 #I #K #V #HLK #HV
+elim (cpms_inv_lref1_drops … H2) -H2 *
+[ #_ #H destruct
+| #Y #X #W #H #HVW #HUX1
+ lapply (drops_mono … H … HLK) -H #H destruct
+ /4 width=8 by cnv_cpms_nta, cpcs_cprs_sn, ex5_4_intro, or_introl/
+| #n #Y #X #U #H #HVU #HUX1 #H0 destruct
+ lapply (drops_mono … H … HLK) -H #H destruct
+ elim (lifts_total V (𝐔❴↑i❵)) #W #HVW
+ lapply (cpms_lifts_bi … HVU (Ⓣ) … L … HVW … HUX1) -U
+ [ /2 width=2 by drops_isuni_fwd_drop2/ ] #HWX1
+ /4 width=9 by cprs_div, ex5_3_intro, or_intror/
+]
+qed-.
+
lemma nta_inv_bind_sn_cnv (a) (h) (p) (I) (G) (K) (X2):
∀V,T. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] X2 →
∃∃U. ⦃G,K⦄ ⊢ V ![a,h] & ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U & ⦃G,K⦄ ⊢ ⓑ{p,I}V.U ⬌*[h] X2 & ⦃G,K⦄ ⊢ X2 ![a,h].
@ex4_3_intro [6,13: |*: /2 width=5 by cnv_cpms_nta/ ]
/3 width=5 by cprs_div, cprs_trans/
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)
lemma nta_inv_pure_sn_cnv (h) (G) (L) (X2):
∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :*[h] X2 →
@(cprs_div … (ⓐV0.ⓛ{p}W1.U1))
/3 width=1 by cpms_appl, cpms_appl_dx, cpms_bind/
]
-
+*)
(* 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 →
(* Basic_2A1: was by definition: nta_ldec *)
lemma nta_ldec_drops
+(* Basic_1: was: ty3_gen_lref *)
+(* Basic_2A1: was: nta_inv_lref1 *)
+lemma nta_inv_lref_sn_drops
+
(* Advanced properties ******************************************************)
| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
lapply (nta_mono … HTW … HTU) #HWU
elim (nta_fwd_correct … HTU) -HTU /3 width=3/
qed.
+
+lemma nta_ind_alt: ∀h. ∀Q:lenv→relation term.
+ (∀L,k. Q L ⋆k ⋆(next h k)) →
+ (∀L,K,V,W,U,i.
+ ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
+ Q K V W → Q L (#i) U
+ ) →
+ (∀L,K,W,V,U,i.
+ ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
+ Q K W V → Q L (#i) U
+ ) →
+ (∀I,L,V,W,T,U.
+ ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
+ Q L V W → Q (L.ⓑ{I}V) T U → Q L (ⓑ{I}V.T) (ⓑ{I}V.U)
+ ) →
+ (∀L,V,W,T,U.
+ ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
+ Q L V W →Q L (ⓛW.T) (ⓛW.U) →Q L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
+ ) →
+ (∀L,V,W,T,U.
+ ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
+ Q L T U → Q L (ⓐV.U) W → Q L (ⓐV.T) (ⓐV.U)
+ ) →
+ (∀L,T,U,W.
+ ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
+ Q L T U → Q L U W → Q L (ⓝU.T) U
+ ) →
+ (∀L,T,U1,U2,V2.
+ ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
+ Q L T U1 →Q L U2 V2 →Q L T U2
+ ) →
+ ∀L,T,U. ⦃h, L⦄ ⊢ T : U → Q L T U.
+++ /dev/null
-
-include "basic_2/rt_computation/cpms_lpr.ma".
-
-theorem cpr_cpm_trans_swap_lpr (h) (G) (L1) (T1):
- ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 →
- ∃∃T0. ⦃G,L1⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L1⦄ ⊢ T0 ➡*[h] T2.
-#h #G #L1 #T1 #T #H
-@(cpr_ind … H) -G -L1 -T1 -T
-[ (* #I #G #L1 #L2 #HL12 #n2 #T2 #HT2 /2 width=3 by ex2_intro/ *)
-| (*
- #G #K #V1 #V #W #_ #IH #HVW #n2 #T2 #HT2
- elim (cpm_inv_lifts_sn … HT2 (Ⓣ) … HVW) -W
- [|*: /3 width=2 by drops_refl, drops_drop/ ] #V2 #HVT2 #HV2
- elim (IH … HV2) -V #V0 #HV10 #HV02
- elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
- lapply (cpm_lifts_bi … HV02 (Ⓣ) … (K.ⓓV1) … HVT0 … HVT2) -V2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
- /3 width=3 by cpm_delta, ex2_intro/
-*)
-| (*
- #I #G #K #T #U #i #_ #IH #HTU #n2 #U2 #HU2
- elim (cpm_inv_lifts_sn … HU2 (Ⓣ) … HTU) -U
- [|*: /3 width=2 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT2
- elim (IH … HT2) -T #T0 #HT0 #HT02
- elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
- lapply (cpm_lifts_bi … HT02 (Ⓣ) … (K.ⓘ{I}) … HTU0 … HTU2) -T2
- [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
- /3 width=3 by cpm_lref, ex2_intro/
-*)
-| #p #I #G #L1 #V1 #V #T1 #T #HV1 #_ #_ #IHT #L2 #HL12 #n2 #X2 #H
- elim (cpm_inv_bind1 … H) -H *
- [ #V2 #T2 #HV2 #HT2 #H destruct
- elim (IHT … HT2) -T [| /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
- lapply (lpr_cpm_trans … HV2 … HL12) -L2 #HV2
- /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 (IHT … HT2) -HT2 -IHT [| /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
- /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/
- ]
-|
\ No newline at end of file
]
qed-.
+lemma cpms_inv_delta_sn (n) (h) (G) (K) (V):
+ ∀T2. ⦃G,K.ⓓV⦄ ⊢ #0 ➡*[n,h] T2 →
+ ∨∨ ∧∧ T2 = #0 & n = 0
+ | ∃∃V2. ⦃G,K⦄ ⊢ V ➡*[n,h] V2 & ⬆*[1] V2 ≘ T2.
+#n #h #G #K #V #T2 #H
+elim (cpms_inv_lref1_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #Y #X #V2 #H #HV2 #HVT2
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /3 width=3 by ex2_intro, or_intror/
+| #m #Y #X #V2 #H #HV2 #HVT2
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+]
+qed-.
+
+lemma cpms_inv_ell_sn (n) (h) (G) (K) (V):
+ ∀T2. ⦃G,K.ⓛV⦄ ⊢ #0 ➡*[n,h] T2 →
+ ∨∨ ∧∧ T2 = #0 & n = 0
+ | ∃∃m,V2. ⦃G,K⦄ ⊢ V ➡*[m,h] V2 & ⬆*[1] V2 ≘ T2 & n = ↑m.
+#n #h #G #K #V #T2 #H
+elim (cpms_inv_lref1_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #Y #X #V2 #H #HV2 #HVT2
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+| #m #Y #X #V2 #H #HV2 #HVT2 #H0 destruct
+ lapply (drops_fwd_isid … H ?) -H [ // ] #H destruct
+ /3 width=5 by ex3_2_intro, or_intror/
+]
+qed-.
+
+lemma cpms_inv_lref_sn (n) (h) (G) (I) (K):
+ ∀U2,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ➡*[n,h] U2 →
+ ∨∨ ∧∧ U2 = #↑i & n = 0
+ | ∃∃T2. ⦃G,K⦄ ⊢ #i ➡*[n,h] T2 & ⬆*[1] T2 ≘ U2.
+#n #h #G #I #K #U2 #i #H
+elim (cpms_inv_lref1_drops … H) -H *
+[ /3 width=1 by or_introl, conj/
+| #L #V #V2 #H #HV2 #HVU2
+ lapply (drops_inv_drop1 … H) -H #HLK
+ elim (lifts_split_trans … HVU2 (𝐔❴↑i❵) (𝐔❴1❵)) -HVU2
+ [| // ] #T2 #HVT2 #HTU2
+ /4 width=6 by cpms_delta_drops, ex2_intro, or_intror/
+| #m #L #V #V2 #H #HV2 #HVU2 #H0 destruct
+ lapply (drops_inv_drop1 … H) -H #HLK
+ elim (lifts_split_trans … HVU2 (𝐔❴↑i❵) (𝐔❴1❵)) -HVU2
+ [| // ] #T2 #HVT2 #HTU2
+ /4 width=6 by cpms_ell_drops, ex2_intro, or_intror/
+]
+qed-.
+
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.
class "magenta"
[ { "dynamic typing" * } {
[ { "context-sensitive native type assignment" * } {
- [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_cpms" + "nta_cpcs" + "nta_preserve" * ]
+ [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_ind" * ]
}
]
[ { "context-sensitive native validity" * } {
projects / helm.git / commitdiff