(**************************************************************************)
include "basic_2/notation/relations/exclaim_5.ma".
+include "basic_2/notation/relations/exclaim_4.ma".
+include "basic_2/notation/relations/exclaimstar_4.ma".
include "basic_2/rt_computation/cpms.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
interpretation "context-sensitive native validity (term)"
'Exclaim a h G L T = (cnv a h G L T).
+interpretation "context-sensitive restricted native validity (term)"
+ 'Exclaim h G L T = (cnv true h G L T).
+
+interpretation "context-sensitive extended native validity (term)"
+ 'ExclaimStar h G L T = (cnv false h G L T).
+
(* Basic inversion lemmas ***************************************************)
fact cnv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 →
(* *)
(**************************************************************************)
+include "basic_2/rt_transition/cpm_aaa.ma".
include "basic_2/rt_computation/cpms_aaa.ma".
include "basic_2/dynamic/cnv.ma".
/3 width=3 by aaa_cast, ex_intro/
]
qed-.
+
+(* Forward lemmas with t_bound rt_transition for terms **********************)
+
+lemma cnv_fwd_cpm_SO (a) (h) (G) (L):
+ ∀T. ⦃G, L⦄ ⊢ T ![a, h] → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U.
+#a #h #G #L #T #H
+elim (cnv_fwd_aaa … H) -H #A #HA
+/2 width=2 by aaa_cpm_SO/
+qed-.
[ #H1 #H2 destruct /2 width=4 by ex3_intro/
| #s #H1 #H2 #H3 #Hs destruct
elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
- /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
+ /5 width=6 by cpm_sort, tdeq_sort, deg_iter, deg_next, ex3_intro/
]
| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #_ #H0T1 #H1T1 #H2T1 #H destruct
(* Advanced preservation properties *****************************************)
+lemma cnv_cpms_conf (a) (h) (G) (L):
+ ∀T0. ⦃G,L⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G,L⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T0 ➡*[n2,h] T2 →
+ ∃∃T. ⦃G,L⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L⦄ ⊢ T2 ➡*[n1-n2,h] T.
+/2 width=8 by cnv_cpms_conf_lpr/ qed-.
+
(* Basic_2A1: uses: snv_cprs_lpr *)
lemma cnv_cpms_trans_lpr (a) (h) (G) (L) (T): IH_cnv_cpms_trans_lpr a h G L T.
#a #h #G #L1 #T1 #HT1 #n #T2 #H
@(cpms_ind_dx … H) -n -T2 /3 width=6 by cnv_cpm_trans_lpr/
qed-.
+
+lemma cnv_cpms_trans (a) (h) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
+/2 width=6 by cnv_cpms_trans_lpr/ 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/notation/relations/colon_6.ma".
+include "basic_2/notation/relations/colon_5.ma".
+include "basic_2/notation/relations/colonstar_5.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
+
+definition nta (a) (h): relation4 genv lenv term term ≝
+ λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
+
+interpretation "native type assignment (term)"
+ 'Colon a h G L T U = (nta a h G L T U).
+
+interpretation "restricted native type assignment (term)"
+ 'Colon h G L T U = (nta true h G L T U).
+
+interpretation "extended native type assignment (term)"
+ 'ColonStar h G L T U = (nta false h G L T U).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was by definition: ty3_sort *)
+(* Basic_2A1: was by definition: nta_sort ntaa_sort *)
+lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(next h s).
+#a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
+qed.
+
+lemma nta_bind_cnv (a) (h) (G) (K):
+ ∀V. ⦃G,K⦄ ⊢ V ![a,h] →
+ ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U →
+ ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] ⓑ{p,I}V.U.
+#a #h #G #K #V #HV #I #T #U #H #p
+elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX
+/3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/
+qed.
+
+(* Basic_2A1: was by definition: nta_cast *)
+lemma nta_cast (a) (h) (G) (L):
+ ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ ⓝU.T :[a,h] U.
+#a #h #G #L #T #U #H
+elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX
+/3 width=3 by cnv_cast, cpms_eps/
+qed.
+
+(* Basic_1: was by definition: ty3_cast *)
+lemma nta_cast_old (a) (h) (G) (L):
+ ∀T0,T1. ⦃G,L⦄ ⊢ T0 :[a,h] T1 →
+ ∀T2. ⦃G,L⦄ ⊢ T1 :[a,h] T2 → ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] ⓝT2.T1.
+#a #h #G #L #T0 #T1 #H1 #T2 #H2
+elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01
+elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12
+/3 width=3 by cnv_cast, cpms_eps/
+qed.
+
+(* Basic_forward lemmas *****************************************************)
+
+lemma nta_fwd_cnv_sn (a) (h) (G) (L):
+ ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
+#a #h #G #L #T #U #H
+elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
+qed-.
+
+(* Note: this is nta_fwd_correct_cnv *)
+lemma nta_fwd_cnv_dx (a) (h) (G) (L):
+ ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h].
+#a #h #G #L #T #U #H
+elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
+qed-.
+
+(*
+
+| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
+ ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
+ ⇧[0, i + 1] W ≡ U → nta h L (#i) U
+.
+
+(* Basic properties *********************************************************)
+
+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-.
+
+*)
+
+(* Basic_1: removed theorems 4:
+ ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
+*)
+(* Basic_2A1: removed theorems 2:
+ ntaa_nta nta_ntaa
+*)
--- /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/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
+
+(* Properties with r-equivalence for terms **********************************)
+
+lemma nta_conv_cnv (a) (h) (G) (L) (T):
+ ∀U1. ⦃G,L⦄ ⊢ T :[a,h] U1 →
+ ∀U2. ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 → ⦃G,L⦄ ⊢ U2 ![a,h] → ⦃G,L⦄ ⊢ T :[a,h] U2.
+#a #h #G #L #T #U1 #H1 #U2 #HU12 #HU2
+elim (cnv_inv_cast … H1) -H1 #X1 #HU1 #HT #HUX1 #HTX1
+lapply (cpcs_cprs_conf … HUX1 … HU12) -U1 #H
+elim (cpcs_inv_cprs … H) -H #X2 #HX12 #HU12
+/3 width=5 by cnv_cast, cpms_cprs_trans/
+qed-.
+
+(* Basic_1: was by definition: ty3_conv *)
+(* Basic_2A1: was by definition: nta_conv ntaa_conv *)
+lemma nta_conv (a) (h) (G) (L) (T):
+ ∀U1. ⦃G,L⦄ ⊢ T :[a,h] U1 →
+ ∀U2. ⦃G,L⦄ ⊢ U1 ⬌*[h] U2 →
+ ∀W2. ⦃G,L⦄ ⊢ U2 :[a,h] W2 → ⦃G,L⦄ ⊢ T :[a,h] U2.
+#a #h #G #L #T #U1 #H1 #U2 #HU12 #W2 #H2
+/3 width=3 by nta_conv_cnv, nta_fwd_cnv_sn/
+qed-.
+
+(* Inversion lemmas with r-equivalence for terms ***************************)
+
+(* 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.
+#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/
+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_computation/cprs_cprs.ma".
+include "basic_2/rt_computation/lprs_cpms.ma".
+include "basic_2/dynamic/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
+
+(* 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
+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/
+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
+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
+elim (cprs_conf … HWX1 … HW0) -HW0 #X0 #HX10 #HWX0
+@(cnv_cast … (ⓐV.ⓛ{p}W0.U0)) (**) (* full auto too slow *)
+[ /3 width=7 by cnv_appl, cpms_bind/
+| /4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
+| /2 width=1 by cpms_appl_dx/
+| /2 width=1 by cpms_appl_dx/
+]
+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_alt.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
+ (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+ ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ) ∨
+ (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+ ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+ ).
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #j #H destruct
+| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
+| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
+| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
+| #L #T #U #_ #_ #j #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
+ elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
+ lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
+]
+qed.
+
+(* 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 **************************************************)
+
+fact nta_fwd_pure1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
+ ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
+#h #L #T #U #H elim H -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #T #U #HVW #HTU #_ #_ #X #Y #H destruct /2 width=3/
+| #L #V #W #T #U #HTU #_ #_ #IHUW #X #Y #H destruct
+ elim (IHUW U Y ?) -IHUW // /2 width=3/
+| #L #T #U #_ #_ #X #Y #H destruct
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+ elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #HYW #HXV #HU1
+ lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
+]
+qed.
+
+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-.
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: ty3_lift *)
+(* Basic_2A1: was: ntaa_lift *)
+lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
+/4 width=9 by ntaa_nta, nta_ntaa, ntaa_lift/ 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".
+include "basic_2/dynamic/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
+
+(* Properties based on preservation *****************************************)
+
+lemma cnv_cpms_nta (a) (h) (G) (L):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀U.⦃G,L⦄ ⊢ T ➡*[1,h] U → ⦃G,L⦄ ⊢ T :[a,h] U.
+/3 width=4 by cnv_cast, cnv_cpms_trans/ qed.
+
+lemma cnv_nta_sn (a) (h) (G) (L):
+ ∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∃U. ⦃G,L⦄ ⊢ T :[a,h] U.
+#a #h #G #L #T #HT
+elim (cnv_fwd_cpm_SO … HT) #U #HTU
+/4 width=2 by cnv_cpms_nta, cpm_cpms, ex_intro/
+qed-.
+
+lemma nta_pure_cnv (h) (G) (L):
+ ∀T,U. ⦃G,L⦄ ⊢ T :*[h] U →
+ ∀V. ⦃G,L⦄ ⊢ ⓐV.U !*[h] → ⦃G,L⦄ ⊢ ⓐV.T :*[h] ⓐV.U.
+#h #G #L #T #U #H1 #V #H2
+elim (cnv_inv_cast … H1) -H1 #X0 #HU #HT #HUX0 #HTX0
+elim (cnv_inv_appl … H2) #n #p #X1 #X2 #_ #HV #_ #HVX1 #HUX2
+elim (cnv_cpms_conf … HU … HUX0 … HUX2) -HU -HUX2
+<minus_O_n <minus_n_O #X #HX0 #H
+elim (cpms_inv_abst_sn … H) -H #X3 #X4 #HX13 #HX24 #H destruct
+@(cnv_cast … (ⓐV.X0)) [2:|*: /2 width=1 by cpms_appl_dx/ ]
+@(cnv_appl … X3) [4: |*: /2 width=7 by cpms_trans, cpms_cprs_trans/ ]
+#H destruct
+qed.
+
+(* Inversion lemmas based on preservation ***********************************)
+
+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].
+#a #h #p * #G #K #X2 #V #T #H
+elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
+elim (cnv_inv_bind … H1) -H1 #HV #HT
+[ elim (cpms_inv_abbr_sn_dx … H2) -H2 *
+ [ #V0 #U #HV0 #HTU #H destruct
+ /4 width=5 by cnv_cpms_nta, cprs_div, cpms_bind, ex4_intro/
+ | #U #HTU #HX1U #H destruct
+ /4 width=5 by cnv_cpms_nta, cprs_div, cpms_zeta, ex4_intro/
+ ]
+| elim (cpms_inv_abst_sn … H2) -H2 #V0 #U #HV0 #HTU #H destruct
+ /4 width=5 by cnv_cpms_nta, cprs_div, cpms_bind, ex4_intro/
+]
+qed-.
+
+(* Basic_1: uses: ty3_gen_appl *)
+lemma nta_inv_appl_sn (h) (G) (L) (X2):
+ ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T :[h] X2 →
+ ∃∃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].
+#h #G #L #X2 #V #T #H
+elim (cnv_inv_cast … H) -H #X #HX2 #H1 #HX2 #H2
+elim (cnv_inv_appl … H1) * [ | #n ] #p #W #U #Hn #HV #HT #HVW #HTU
+[ lapply (cnv_cpms_trans … HT … HTU) #H
+ elim (cnv_inv_bind … H) -H #_ #HU
+ elim (cnv_fwd_cpm_SO … HU) #U0 #HU0 -HU
+ 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/
+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 →
+ ∧∧ ⦃G,L⦄ ⊢ T :[a,h] U & ⦃G,L⦄ ⊢ U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
+#a #h #G #L #X2 #U #T #H
+elim (cnv_inv_cast … H) -H #X0 #HX2 #H1 #HX20 #H2
+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 *)
+| #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 *)
+| #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 *)
+]
+qed-.
+
+(* Forward lemmas based on preservation *************************************)
+
+(* Basic_1: was: ty3_unique *)
+theorem nta_mono (a) (h) (G) (L) (T):
+ ∀U1. ⦃G,L⦄ ⊢ T :[a,h] U1 → ∀U2. ⦃G,L⦄ ⊢ T :[a,h] U2 → ⦃G,L⦄ ⊢ U1 ⬌*[h] U2.
+#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/
+qed-.
notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
non associative with precedence 45
for @{ 'PConvSnStar $L1 $L2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
- non associative with precedence 45
- for @{ 'NativeType $h $L $T1 $T2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )"
- non associative with precedence 45
- for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
-
-notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )"
- non associative with precedence 45
- for @{ 'NativeTypeStar $h $L $T1 $T2 }.
--- /dev/null
+(* Basic_1: was by definition: ty3_bind *)
+(* Basic_2A1: was by definition: nta_bind ntaa_bind *)
+lemma nta_bind
+
+(* Basic_2A1: was by definition: nta_pure ntaa_pure *)
+lemma nta_pure
+
+(* Basic_1: was: ty3_gen_bind *)
+(* Basic_2A1: was: nta_inv_bind1 ntaa_inv_bind1 *)
+lemma nta_inv_bind_sn
+
+| ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
+
+(* Advanced properties ******************************************************)
+
+lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T : W → ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ ⓝW.T : U.
+#h #L #T #W #U #HTW #HTU
+lapply (nta_mono … HTW … HTU) #HWU
+elim (nta_fwd_correct … HTU) -HTU /3 width=3/
+qed.
+
+lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+/2 width=3/ qed-.
+
+(* Basic_1: uses: ty3_gen_cast *)
+lemma nta_inv_cast_sn_old (a) (h) (G) (L) (X2):
+ ∀T0,T1. ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] X2 →
+ ∃∃T2. ⦃G,L⦄ ⊢ T0 :[a,h] T1 & ⦃G,L⦄ ⊢ T1 :[a,h] T2 & ⦃G,L⦄ ⊢ ⓝT2.T1 ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![a,h].
+
+(* Basic_1: was: ty3_typecheck *)
+lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓝU.T : T0.
+/3 width=2/ qed.
+
+(* Basic_1: was: ty3_correct *)
+(* Basic_2A1: was: ntaa_fwd_correct *)
+lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
+#h #L #T #U #H
+elim (ntaa_fwd_correct … (nta_ntaa … H)) -H /3 width=2 by ntaa_nta, ex_intro/
+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/static/sh.ma".
-include "basic_2/equivalence/cpcs.ma".
-
-(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
-
-inductive nta (h:sh): lenv → relation term ≝
-| nta_sort: ∀L,k. nta h L (⋆k) (⋆(next h k))
-| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
- ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
- ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-| nta_bind: ∀I,L,V,W,T,U. nta h L V W → nta h (L. ⓑ{I} V) T U →
- nta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
-| nta_appl: ∀L,V,W,T,U. nta h L V W → nta h L (ⓛW.T) (ⓛW.U) →
- nta h L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
-| nta_pure: ∀L,V,W,T,U. nta h L T U → nta h L (ⓐV.U) W →
- nta h L (ⓐV.T) (ⓐV.U)
-| nta_cast: ∀L,T,U. nta h L T U → nta h L (ⓝU. T) U
-| nta_conv: ∀L,T,U1,U2,V2. nta h L T U1 → L ⊢ U1 ⬌* U2 → nta h L U2 V2 →
- nta h L T U2
-.
-
-interpretation "native type assignment (term)"
- 'NativeType h L T U = (nta h L T U).
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: ty3_cast *)
-lemma nta_cast_old: ∀h,L,W,T,U.
- ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W → ⦃h, L⦄ ⊢ ⓝU.T : ⓝW.U.
-/4 width=3/ qed.
-
-(* Basic_1: was: ty3_typecheck *)
-lemma nta_typecheck: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ ⓝU.T : T0.
-/3 width=2/ qed.
-
-(* Basic_1: removed theorems 4:
- ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
-*)
+++ /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_alt.ma".
-
-(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-fact nta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
- L ⊢ ⋆(next h k0) ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #k0 #H destruct //
-| #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct
-| #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
-| #L #T #U #_ #_ #k0 #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
- lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0
- lapply (cpcs_trans … Hk0 … HU12) -U1 //
-]
-qed.
-
-(* Basic_1: was: ty3_gen_sort *)
-lemma nta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
-/2 width=3/ qed-.
-
-fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
- (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
- ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ) ∨
- (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
- ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
- ).
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #j #H destruct
-| #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
-| #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
-| #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
-| #L #T #U #_ #_ #j #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
- elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
- lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
-]
-qed.
-
-(* 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-.
-
-(* Basic_1: was: ty3_gen_bind *)
-lemma nta_inv_bind1: ∀h,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{I}Y.X : U →
- ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{I}Y⦄ ⊢ X : Z2 &
- L ⊢ ⓑ{I}Y.Z2 ⬌* U.
-#h #I #L #Y #X #U #H
-elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/
-qed-.
-
-fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓝY.X →
- ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #X #Y #H destruct
-| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
-| #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
-| #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
- elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
- lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
-]
-qed.
-
-(* Basic_1: was: ty3_gen_cast *)
-lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X : U → ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
-/2 width=3/ qed-.
-
-(* Advanced forvard lemmas **************************************************)
-
-fact nta_fwd_pure1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
- ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
-#h #L #T #U #H elim H -L -T -U
-[ #L #k #X #Y #H destruct
-| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
-| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
-| #L #V #W #T #U #HVW #HTU #_ #_ #X #Y #H destruct /2 width=3/
-| #L #V #W #T #U #HTU #_ #_ #IHUW #X #Y #H destruct
- elim (IHUW U Y ?) -IHUW // /2 width=3/
-| #L #T #U #_ #_ #X #Y #H destruct
-| #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
- elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #HYW #HXV #HU1
- lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
-]
-qed.
-
-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-.
-
-(* Basic_1: was: ty3_correct *)
-lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
-#h #L #T #U #H
-elim (ntaa_fwd_correct … (nta_ntaa … H)) -H /3 width=2 by ntaa_nta, ex_intro/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was: ty3_appl *)
-lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U →
- ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
-#h #L #V #W #T #U #HVW #HTU
-elim (nta_fwd_correct … HTU) #X #H
-elim (nta_inv_bind1 … H) -H /4 width=2/
-qed.
-
-(* Properties on relocation *************************************************)
-
-(* Basic_1: was: ty3_lift *)
-lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
-/4 width=9 by ntaa_nta, nta_ntaa, ntaa_lift/ 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_lift.ma".
-
-(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: ty3_unique *)
-theorem nta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T : U1 → ∀U2. ⦃h, L⦄ ⊢ T : U2 →
- L ⊢ U1 ⬌* U2.
-#h #L #T #U1 #H elim H -L -T -U1
-[ #L #k #X #H
- lapply (nta_inv_sort1 … H) -H //
-| #L #K #V #W11 #W12 #i #HLK #_ #HW112 #IHVW11 #X #H
- elim (nta_inv_lref1 … H) -H * #K0 #V0 #W21 #W22 #HLK0 #HVW21 #HW212 #HX
- lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
- @(cpcs_trans … HX) -X /3 width=9 by cpcs_lift/ (**) (* to slow without trace *)
-| #L #K #W #V1 #V #i #HLK #_ #HWV #_ #X #H
- elim (nta_inv_lref1 … H) -H * #K0 #W0 #V2 #V0 #HLK0 #_ #HWV0 #HX
- lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H destruct
- lapply (lift_mono … HWV0 … HWV) -HWV0 -HWV #H destruct //
-| #I #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
- elim (nta_inv_bind1 … H) -H #W2 #U2 #_ #HTU2 #H
- @(cpcs_trans … H) -X /3 width=1/
-| #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
- elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H
- @(cpcs_trans … H) -X /3 width=1/
-| #L #V #W1 #T #U1 #_ #_ #IHTU1 #_ #X #H
- elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H
- @(cpcs_trans … H) -X /3 width=1/
-| #L #T #U1 #_ #_ #X #H
- elim (nta_inv_cast1 … H) -H //
-| #L #T #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #_ #U2 #HTU2
- @(cpcs_canc_sn … HU112) -U12 /2 width=1/
-]
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma nta_cast_alt: ∀h,L,T,W,U. ⦃h, L⦄ ⊢ T : W → ⦃h, L⦄ ⊢ T : U →
- ⦃h, L⦄ ⊢ ⓝW.T : U.
-#h #L #T #W #U #HTW #HTU
-lapply (nta_mono … HTW … HTU) #HWU
-elim (nta_fwd_correct … HTU) -HTU /3 width=3/
-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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 :[ break term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'Colon $h $G $L $T1 $T2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 :[ break term 46 a, break term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'Colon $a $h $G $L $T1 $T2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 :*[ break term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'ColonStar $h $G $L $T1 $T2 }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T ![ break term 46 h ] )"
+ non associative with precedence 45
+ for @{ 'Exclaim $h $G $L $T }.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T !*[ break term 46 h ] )"
+ non associative with precedence 45
+ for @{ 'ExclaimStar $h $G $L $T }.
#h #G #L #T1 #Q @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 #H #_ destruct //
-qed-.
-
(* Basic properties *********************************************************)
(* Basic_1: includes: pr1_pr0 *)
lemma cprs_refl: ∀h,G,L. reflexive … (cpms h G L 0).
/2 width=1 by cpm_cpms/ qed.
+(* Advanced properties ******************************************************)
+
+lemma cpms_sort (h) (G) (L) (n):
+ ∀s. ⦃G,L⦄ ⊢ ⋆s ➡*[n,h] ⋆((next h)^n s).
+#h #G #L #n elim n -n [ // ]
+#n #IH #s <plus_SO
+/3 width=3 by cpms_step_dx, cpm_sort/
+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 #H #_ destruct //
+qed-.
+
+lemma cpms_inv_cast1 (h) (n) (G) (L):
+ ∀W1,T1,X2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡*[n,h] X2 →
+ ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡*[n,h] W2 & ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 & X2 = ⓝW2.T2
+ | ⦃G, L⦄ ⊢ T1 ➡*[n,h] X2
+ | ∃∃m. ⦃G, L⦄ ⊢ W1 ➡*[m,h] X2 & n = ↑m.
+#h #n #G #L #W1 #T1 #X2 #H @(cpms_ind_dx … H) -n -X2
+[ /3 width=5 by or3_intro0, ex3_2_intro/
+| #n1 #n2 #X #X2 #_ * [ * || * ]
+ [ #W #T #HW1 #HT1 #H #HX2 destruct
+ elim (cpm_inv_cast1 … HX2) -HX2 [ * || * ]
+ [ #W2 #T2 #HW2 #HT2 #H destruct
+ /4 width=5 by cpms_step_dx, ex3_2_intro, or3_intro0/
+ | #HX2 /3 width=3 by cpms_step_dx, or3_intro1/
+ | #m #HX2 #H destruct <plus_n_Sm
+ /4 width=3 by cpms_step_dx, ex2_intro, or3_intro2/
+ ]
+ | #HX #HX2 /3 width=3 by cpms_step_dx, or3_intro1/
+ | #m #HX #H #HX2 destruct
+ /4 width=3 by cpms_step_dx, ex2_intro, or3_intro2/
+ ]
+]
+qed-.
+
(* Basic_2A1: removed theorems 5:
sta_cprs_scpds lstas_scpds scpds_strap1 scpds_fwd_cprs
scpds_inv_lstas_eq
(* Basic_1: was: pr3_gen_cast *)
lemma cprs_inv_cast1 (h) (G) (L): ∀W1,T1,X2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡*[h] X2 →
- ∨∨ ⦃G, L⦄ ⊢ T1 ➡*[h] X2
- | ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L⦄ ⊢ T1 ➡*[h] T2 & X2 = ⓝW2.T2.
-#h #G #L #W1 #T1 #X2 #H @(cprs_ind_dx … H) -X2
-[ /3 width=5 by ex3_2_intro, or_intror/
-| #X #X2 #_ #HX2 * /3 width=3 by cprs_step_dx, or_introl/ *
- #W #T #HW1 #HT1 #H destruct
- elim (cpr_inv_cast1 … HX2) -HX2 /3 width=3 by cprs_step_dx, or_introl/ *
- #W2 #T2 #HW2 #HT2 #H destruct
- /4 width=5 by cprs_step_dx, ex3_2_intro, or_intror/
+ ∨∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡*[h] W2 & ⦃G, L⦄ ⊢ T1 ➡*[h] T2 & X2 = ⓝW2.T2
+ | ⦃G, L⦄ ⊢ T1 ➡*[h] X2.
+#h #G #L #W1 #T1 #X2 #H
+elim (cpms_inv_cast1 … H) -H
+[ /2 width=1 by or_introl/
+| /2 width=1 by or_intror/
+| * #m #_ #H destruct
]
qed-.
(* Advanced properties ******************************************************)
-lemma cpm_sort_iter (h) (G) (L):
- ∀n. n ≤ 1 →
- ∀s. ⦃G,L⦄ ⊢ ⋆s ➡ [n,h] ⋆((next h)^n s).
+lemma cpm_sort (h) (G) (L):
+ ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ➡[n,h] ⋆((next h)^n s).
#h #G #L * //
#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
qed.
(* Basic_2A1: includes: cpr_aaa_conf *)
lemma cpm_aaa_conf (n) (h): ∀G,L. Conf3 … (aaa G L) (cpm h G L n).
/3 width=5 by cpx_aaa_conf, cpm_fwd_cpx/ qed-.
+
+(* Note: one of these U is the inferred type of T *)
+lemma aaa_cpm_SO (h) (G) (L) (A):
+ ∀T. ⦃G, L⦄ ⊢ T ⁝ A → ∃U. ⦃G,L⦄ ⊢ T ➡[1,h] U.
+#h #G #L #A #T #H elim H -G -L -T -A
+[ /3 width=2 by ex_intro/
+| * #G #L #V #B #_ * #V0 #HV0
+ [ elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
+ /3 width=4 by cpm_delta, ex_intro/
+ | elim (lifts_total V (𝐔❴1❵)) #W #HVW -V0
+ /3 width=4 by cpm_ell, ex_intro/
+ ]
+| #I #G #L #A #i #_ * #T0 #HT0
+ elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+ /3 width=4 by cpm_lref, ex_intro/
+| #p #G #L #V #T #B #A #_ #_ #_ * #T0 #HT0
+ /3 width=2 by cpm_bind, ex_intro/
+| #p #G #L #V #T #B #A #_ #_ #_ * #T0 #HT0
+ /3 width=2 by cpm_bind, ex_intro/
+| #G #L #V #T #B #A #_ #_ #_ * #T0 #HT0
+ /3 width=2 by cpm_appl, ex_intro/
+| #G #L #U #T #A #_ #_ * #U0 #HU0 * #T0 #HT0
+ /3 width=2 by cpm_cast, ex_intro/
+]
+qed-.
]
}
]
+(*
class "wine"
[ { "iterated dynamic typing" * } {
[ { "" (* "higher order native type assignment" *) * } {
]
}
]
+*)
class "magenta"
[ { "dynamic typing" * } {
-(*
- [ { "local env. ref. for native type assignment" * } {
- [ [ "" ] "lsubn ( ? ⊢ ? :⫃ ? )" "lsubn_drop" "lsubn_cpcs" "lsubn_nta" * ]
- }
- ]
- [ { "native type assignment" * } {
- [ [ "" ] "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ]
+ [ { "context-sensitive native type assignment" * } {
+ [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_cpms" + "nta_cpcs" + "nta_preserve" * ]
}
]
-*)
[ { "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_preserve_sub" + "cnv_preserve" * ]
}
]
}
class "italic" { 2 }
(*
+
+ [ { "local env. ref. for native type assignment" * } {
+ [ [ "" ] "lsubn ( ? ⊢ ? :⫃ ? )" "lsubn_drop" "lsubn_cpcs" "lsubn_nta" * ]
+ }
+ ]
[ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
[ { "decomposed rt-equivalence" * } {
[ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
+
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ⬌η break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PConvEta $G $L $T1 $T2 }.
--- /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 "static_2/notation/relations/pconveta_4.ma".
+include "static_2/relocation/lifts.ma".
+include "static_2/static/aaa.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************)
+
+(* avtivate genv *)
+inductive cpce: relation4 genv lenv term term ≝
+| cpce_sort: ∀G,L,s. cpce G L (⋆s) (⋆s)
+| cpce_abbr: ∀G,K,V. cpce G (K.ⓓV) (#0) (#0)
+| cpce_abst: ∀G,K,W,B,A. ⦃G,K⦄ ⊢ W ⁝ ②B.A →
+ cpce G (K.ⓛW) (#0) (+ⓛW.ⓐ#0.#1)
+| cpce_lref: ∀I,G,K,T,U,i. cpce G K (#i) T →
+ ⬆*[1] T ≘ U → cpce G (K.ⓘ{I}) (#↑i) U
+| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
+ cpce G K V1 V2 → cpce G (K.ⓑ{I}V1) T1 T2 →
+ cpce G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+| cpce_flat: ∀I,G,L,V1,V2,T1,T2.
+ cpce G L V1 V2 → cpce G L T1 T2 →
+ cpce G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+.
+
+interpretation
+ "context-sensitive parallel eta-conversion (term)"
+ 'PConvEta G L T1 T2 = (cpce G L T1 T2).
]
class "green"
[ { "static typing" * } {
+ [ { "context-sensitive parallel eta-conversion" * } {
+ [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η ? )" * ]
+ }
+ ]
[ { "generic reducibility" * } {
[ [ "restricted refinement for lenvs" ] "lsubc" + "( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]
[ [ "candidates" ] "gcp_cr" + "( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
projects / helm.git / commitdiff