(* *)
(**************************************************************************)
-include "ground_2/ynat/ynat_lt.ma".
+include "ground_2/xoa/ex_2_3.ma".
+include "static_2/syntax/ac.ma".
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 ******************************)
(* activate genv *)
(* Basic_2A1: uses: snv *)
-inductive cnv (a:ynat) (h): relation3 genv lenv term ≝
-| cnv_sort: ∀G,L,s. cnv a h G L (⋆s)
-| cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
-| cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
-| cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)
-| cnv_appl: ∀n,p,G,L,V,W0,T,U0. yinj n < a → cnv a h G L V → cnv a h G L T →
- â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0 â\86\92 cnv a h G L (ⓐV.T)
-| cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T →
- â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[1,h] U0 â\86\92 cnv a h G L (ⓝU.T)
+inductive cnv (h) (a): relation3 genv lenv term ≝
+| cnv_sort: ∀G,L,s. cnv h a G L (⋆s)
+| cnv_zero: ∀I,G,K,V. cnv h a G K V → cnv h a G (K.ⓑ[I]V) (#0)
+| cnv_lref: ∀I,G,K,i. cnv h a G K (#i) → cnv h a G (K.ⓘ[I]) (#↑i)
+| cnv_bind: ∀p,I,G,L,V,T. cnv h a G L V → cnv h a G (L.ⓑ[I]V) T → cnv h a G L (ⓑ[p,I]V.T)
+| cnv_appl: ∀n,p,G,L,V,W0,T,U0. ad a n → cnv h a G L V → cnv h a G L T →
+ â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] W0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W0.U0 â\86\92 cnv h a G L (ⓐV.T)
+| cnv_cast: ∀G,L,U,T,U0. cnv h a G L U → cnv h a G L T →
+ â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[1,h] U0 â\86\92 cnv h a G L (ⓝU.T)
.
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 (yinj (S (S O))) h G L T).
-
-interpretation "context-sensitive extended native validity (term)"
- 'ExclaimStar h G L T = (cnv Y h G L T).
+ 'Exclaim h a G L T = (cnv h a G L T).
(* Basic inversion lemmas ***************************************************)
-fact cnv_inv_zero_aux (a) (h):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 â\8a¢ X ![a,h] → X = #0 →
- â\88\83â\88\83I,K,V. â¦\83G,Kâ¦\84 â\8a¢ V ![a,h] & L = K.â\93\91{I}V.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_zero_aux (h) (a):
+ â\88\80G,L,X. â\9dªG,Lâ\9d« â\8a¢ X ![h,a] → X = #0 →
+ â\88\83â\88\83I,K,V. â\9dªG,Kâ\9d« â\8a¢ V ![h,a] & L = K.â\93\91[I]V.
+#h #a #G #L #X * -G -L -X
[ #G #L #s #H destruct
| #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/
| #I #G #K #i #_ #H destruct
]
qed-.
-lemma cnv_inv_zero (a) (h):
- â\88\80G,L. â¦\83G,Lâ¦\84 â\8a¢ #0 ![a,h] →
- â\88\83â\88\83I,K,V. â¦\83G,Kâ¦\84 â\8a¢ V ![a,h] & L = K.â\93\91{I}V.
+lemma cnv_inv_zero (h) (a):
+ â\88\80G,L. â\9dªG,Lâ\9d« â\8a¢ #0 ![h,a] →
+ â\88\83â\88\83I,K,V. â\9dªG,Kâ\9d« â\8a¢ V ![h,a] & L = K.â\93\91[I]V.
/2 width=3 by cnv_inv_zero_aux/ qed-.
-fact cnv_inv_lref_aux (a) (h):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 â\8a¢ X ![a,h] → ∀i. X = #(↑i) →
- â\88\83â\88\83I,K. â¦\83G,Kâ¦\84 â\8a¢ #i ![a,h] & L = K.â\93\98{I}.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_lref_aux (h) (a):
+ â\88\80G,L,X. â\9dªG,Lâ\9d« â\8a¢ X ![h,a] → ∀i. X = #(↑i) →
+ â\88\83â\88\83I,K. â\9dªG,Kâ\9d« â\8a¢ #i ![h,a] & L = K.â\93\98[I].
+#h #a #G #L #X * -G -L -X
[ #G #L #s #j #H destruct
| #I #G #K #V #_ #j #H destruct
| #I #G #L #i #Hi #j #H destruct /2 width=4 by ex2_2_intro/
]
qed-.
-lemma cnv_inv_lref (a) (h):
- â\88\80G,L,i. â¦\83G,Lâ¦\84 â\8a¢ #â\86\91i ![a,h] →
- â\88\83â\88\83I,K. â¦\83G,Kâ¦\84 â\8a¢ #i ![a,h] & L = K.â\93\98{I}.
+lemma cnv_inv_lref (h) (a):
+ â\88\80G,L,i. â\9dªG,Lâ\9d« â\8a¢ #â\86\91i ![h,a] →
+ â\88\83â\88\83I,K. â\9dªG,Kâ\9d« â\8a¢ #i ![h,a] & L = K.â\93\98[I].
/2 width=3 by cnv_inv_lref_aux/ qed-.
-fact cnv_inv_gref_aux (a) (h): ∀G,L,X. ⦃G,L⦄ ⊢ X ![a,h] → ∀l. X = §l → ⊥.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_gref_aux (h) (a): ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀l. X = §l → ⊥.
+#h #a #G #L #X * -G -L -X
[ #G #L #s #l #H destruct
| #I #G #K #V #_ #l #H destruct
| #I #G #K #i #_ #l #H destruct
qed-.
(* Basic_2A1: uses: snv_inv_gref *)
-lemma cnv_inv_gref (a) (h): ∀G,L,l. ⦃G,L⦄ ⊢ §l ![a,h] → ⊥.
+lemma cnv_inv_gref (h) (a): ∀G,L,l. ❪G,L❫ ⊢ §l ![h,a] → ⊥.
/2 width=8 by cnv_inv_gref_aux/ qed-.
-fact cnv_inv_bind_aux (a) (h):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 â\8a¢ X ![a,h] →
- ∀p,I,V,T. X = ⓑ{p,I}V.T →
- â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![a,h] & â¦\83G,L.â\93\91{I}Vâ¦\84 â\8a¢ T ![a,h].
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_bind_aux (h) (a):
+ â\88\80G,L,X. â\9dªG,Lâ\9d« â\8a¢ X ![h,a] →
+ ∀p,I,V,T. X = ⓑ[p,I]V.T →
+ â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ T ![h,a].
+#h #a #G #L #X * -G -L -X
[ #G #L #s #q #Z #X1 #X2 #H destruct
| #I #G #K #V #_ #q #Z #X1 #X2 #H destruct
| #I #G #K #i #_ #q #Z #X1 #X2 #H destruct
qed-.
(* Basic_2A1: uses: snv_inv_bind *)
-lemma cnv_inv_bind (a) (h):
- â\88\80p,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\91{p,I}V.T ![a,h] →
- â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![a,h] & â¦\83G,L.â\93\91{I}Vâ¦\84 â\8a¢ T ![a,h].
+lemma cnv_inv_bind (h) (a):
+ â\88\80p,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â\93\91[p,I]V.T ![h,a] →
+ â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ T ![h,a].
/2 width=4 by cnv_inv_bind_aux/ qed-.
-fact cnv_inv_appl_aux (a) (h):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 â\8a¢ X ![a,h] → ∀V,T. X = ⓐV.T →
- ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
- â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0.
-#a #h #G #L #X * -L -X
+fact cnv_inv_appl_aux (h) (a):
+ â\88\80G,L,X. â\9dªG,Lâ\9d« â\8a¢ X ![h,a] → ∀V,T. X = ⓐV.T →
+ ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+ â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] W0 & â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W0.U0.
+#h #a #G #L #X * -L -X
[ #G #L #s #X1 #X2 #H destruct
| #I #G #K #V #_ #X1 #X2 #H destruct
| #I #G #K #i #_ #X1 #X2 #H destruct
qed-.
(* Basic_2A1: uses: snv_inv_appl *)
-lemma cnv_inv_appl (a) (h):
- â\88\80G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.T ![a,h] →
- ∃∃n,p,W0,U0. yinj n < a & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G,L⦄ ⊢ T ![a,h] &
- â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0.
+lemma cnv_inv_appl (h) (a):
+ â\88\80G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â\93\90V.T ![h,a] →
+ ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+ â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] W0 & â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W0.U0.
/2 width=3 by cnv_inv_appl_aux/ qed-.
-fact cnv_inv_cast_aux (a) (h):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 â\8a¢ X ![a,h] → ∀U,T. X = ⓝU.T →
- â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![a,h] & â¦\83G,Lâ¦\84 â\8a¢ T ![a,h] &
- â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G,Lâ¦\84 ⊢ T ➡*[1,h] U0.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_cast_aux (h) (a):
+ â\88\80G,L,X. â\9dªG,Lâ\9d« â\8a¢ X ![h,a] → ∀U,T. X = ⓝU.T →
+ â\88\83â\88\83U0. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] & â\9dªG,Lâ\9d« â\8a¢ T ![h,a] &
+ â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 & â\9dªG,Lâ\9d« ⊢ T ➡*[1,h] U0.
+#h #a #G #L #X * -G -L -X
[ #G #L #s #X1 #X2 #H destruct
| #I #G #K #V #_ #X1 #X2 #H destruct
| #I #G #K #i #_ #X1 #X2 #H destruct
qed-.
(* Basic_2A1: uses: snv_inv_cast *)
-lemma cnv_inv_cast (a) (h):
- â\88\80G,L,U,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\9dU.T ![a,h] →
- â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![a,h] & â¦\83G,Lâ¦\84 â\8a¢ T ![a,h] &
- â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G,Lâ¦\84 ⊢ T ➡*[1,h] U0.
+lemma cnv_inv_cast (h) (a):
+ â\88\80G,L,U,T. â\9dªG,Lâ\9d« â\8a¢ â\93\9dU.T ![h,a] →
+ â\88\83â\88\83U0. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] & â\9dªG,Lâ\9d« â\8a¢ T ![h,a] &
+ â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 & â\9dªG,Lâ\9d« ⊢ T ➡*[1,h] U0.
/2 width=3 by cnv_inv_cast_aux/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma cnv_fwd_flat (a) (h) (I) (G) (L):
- â\88\80V,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\95{I}V.T ![a,h] →
- â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![a,h] & â¦\83G,Lâ¦\84 â\8a¢ T ![a,h].
-#a #h * #G #L #V #T #H
+lemma cnv_fwd_flat (h) (a) (I) (G) (L):
+ â\88\80V,T. â\9dªG,Lâ\9d« â\8a¢ â\93\95[I]V.T ![h,a] →
+ â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,Lâ\9d« â\8a¢ T ![h,a].
+#h #a * #G #L #V #T #H
[ elim (cnv_inv_appl … H) #n #p #W #U #_ #HV #HT #_ #_
| elim (cnv_inv_cast … H) #U #HV #HT #_ #_
] -H /2 width=1 by conj/
qed-.
-lemma cnv_fwd_pair_sn (a) (h) (I) (G) (L):
- â\88\80V,T. â¦\83G,Lâ¦\84 â\8a¢ â\91¡{I}V.T ![a,h] â\86\92 â¦\83G,Lâ¦\84 â\8a¢ V ![a,h].
-#a #h * [ #p ] #I #G #L #V #T #H
+lemma cnv_fwd_pair_sn (h) (a) (I) (G) (L):
+ â\88\80V,T. â\9dªG,Lâ\9d« â\8a¢ â\91¡[I]V.T ![h,a] â\86\92 â\9dªG,Lâ\9d« â\8a¢ V ![h,a].
+#h #a * [ #p ] #I #G #L #V #T #H
[ elim (cnv_inv_bind … H) -H #HV #_
| elim (cnv_fwd_flat … H) -H #HV #_
] //
projects / helm.git / blobdiff