(* *)
(**************************************************************************)
+include "ground/xoa/ex_2_3.ma".
include "static_2/syntax/ac.ma".
include "basic_2/notation/relations/exclaim_5.ma".
include "basic_2/rt_computation/cpms.ma".
(* Basic_2A1: uses: snv *)
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_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 →
- â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0 → cnv h a G L (ⓐV.T)
+ â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡*[h,1] W0 â\86\92 â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] â\93\9b[p]W0.U0 → 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 →
- â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[1,h] U0 → cnv h a G L (ⓝU.T)
+ â\9d¨G,Lâ\9d© â\8a¢ U â\9e¡*[h,0] U0 â\86\92 â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,1] U0 → cnv h a G L (ⓝU.T)
.
interpretation "context-sensitive native validity (term)"
(* Basic inversion lemmas ***************************************************)
fact cnv_inv_zero_aux (h) (a):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → X = #0 →
- â\88\83â\88\83I,K,V. â¦\83G,Kâ¦\84 â\8a¢ V ![h,a] & L = K.â\93\91{I}V.
+ â\88\80G,L,X. â\9d¨G,Lâ\9d© ⊢ 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/
qed-.
lemma cnv_inv_zero (h) (a):
- â\88\80G,L. â¦\83G,Lâ¦\84 ⊢ #0 ![h,a] →
- â\88\83â\88\83I,K,V. â¦\83G,Kâ¦\84 â\8a¢ V ![h,a] & L = K.â\93\91{I}V.
+ â\88\80G,L. â\9d¨G,Lâ\9d© ⊢ #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 (h) (a):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀i. X = #(↑i) →
- â\88\83â\88\83I,K. â¦\83G,Kâ¦\84 â\8a¢ #i ![h,a] & L = K.â\93\98{I}.
+ â\88\80G,L,X. â\9d¨G,Lâ\9d© ⊢ 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
qed-.
lemma cnv_inv_lref (h) (a):
- â\88\80G,L,i. â¦\83G,Lâ¦\84 ⊢ #↑i ![h,a] →
- â\88\83â\88\83I,K. â¦\83G,Kâ¦\84 â\8a¢ #i ![h,a] & L = K.â\93\98{I}.
+ â\88\80G,L,i. â\9d¨G,Lâ\9d© ⊢ #↑i ![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 (h) (a): â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀l. X = §l → ⊥.
+fact cnv_inv_gref_aux (h) (a): â\88\80G,L,X. â\9d¨G,Lâ\9d© ⊢ 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
qed-.
(* Basic_2A1: uses: snv_inv_gref *)
-lemma cnv_inv_gref (h) (a): â\88\80G,L,l. â¦\83G,Lâ¦\84 ⊢ §l ![h,a] → ⊥.
+lemma cnv_inv_gref (h) (a): â\88\80G,L,l. â\9d¨G,Lâ\9d© ⊢ §l ![h,a] → ⊥.
/2 width=8 by cnv_inv_gref_aux/ qed-.
fact cnv_inv_bind_aux (h) (a):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] →
- ∀p,I,V,T. X = ⓑ{p,I}V.T →
- â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,L.â\93\91{I}Vâ¦\84 ⊢ T ![h,a].
+ â\88\80G,L,X. â\9d¨G,Lâ\9d© ⊢ 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© ⊢ 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
(* Basic_2A1: uses: snv_inv_bind *)
lemma cnv_inv_bind (h) (a):
- â\88\80p,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\91{p,I}V.T ![h,a] →
- â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,L.â\93\91{I}Vâ¦\84 ⊢ T ![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© ⊢ T ![h,a].
/2 width=4 by cnv_inv_bind_aux/ qed-.
fact cnv_inv_appl_aux (h) (a):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
- â\88\83â\88\83n,p,W0,U0. ad a n & â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
- â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0.
+ â\88\80G,L,X. â\9d¨G,Lâ\9d© ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
+ â\88\83â\88\83n,p,W0,U0. ad a n & â\9d¨G,Lâ\9d© â\8a¢ V ![h,a] & â\9d¨G,Lâ\9d© ⊢ T ![h,a] &
+ â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡*[h,1] W0 & â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] â\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
(* Basic_2A1: uses: snv_inv_appl *)
lemma cnv_inv_appl (h) (a):
- â\88\80G,L,V,T. â¦\83G,Lâ¦\84 ⊢ ⓐV.T ![h,a] →
- â\88\83â\88\83n,p,W0,U0. ad a n & â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
- â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0.
+ â\88\80G,L,V,T. â\9d¨G,Lâ\9d© ⊢ ⓐV.T ![h,a] →
+ â\88\83â\88\83n,p,W0,U0. ad a n & â\9d¨G,Lâ\9d© â\8a¢ V ![h,a] & â\9d¨G,Lâ\9d© ⊢ T ![h,a] &
+ â\9d¨G,Lâ\9d© â\8a¢ V â\9e¡*[h,1] W0 & â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] â\93\9b[p]W0.U0.
/2 width=3 by cnv_inv_appl_aux/ qed-.
fact cnv_inv_cast_aux (h) (a):
- â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
- â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
- â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[1,h] U0.
+ â\88\80G,L,X. â\9d¨G,Lâ\9d© ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
+ â\88\83â\88\83U0. â\9d¨G,Lâ\9d© â\8a¢ U ![h,a] & â\9d¨G,Lâ\9d© ⊢ T ![h,a] &
+ â\9d¨G,Lâ\9d© â\8a¢ U â\9e¡*[h,0] U0 & â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,1] U0.
#h #a #G #L #X * -G -L -X
[ #G #L #s #X1 #X2 #H destruct
| #I #G #K #V #_ #X1 #X2 #H destruct
(* Basic_2A1: uses: snv_inv_cast *)
lemma cnv_inv_cast (h) (a):
- â\88\80G,L,U,T. â¦\83G,Lâ¦\84 ⊢ ⓝU.T ![h,a] →
- â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
- â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[1,h] U0.
+ â\88\80G,L,U,T. â\9d¨G,Lâ\9d© ⊢ ⓝU.T ![h,a] →
+ â\88\83â\88\83U0. â\9d¨G,Lâ\9d© â\8a¢ U ![h,a] & â\9d¨G,Lâ\9d© ⊢ T ![h,a] &
+ â\9d¨G,Lâ\9d© â\8a¢ U â\9e¡*[h,0] U0 & â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,1] U0.
/2 width=3 by cnv_inv_cast_aux/ qed-.
(* Basic forward lemmas *****************************************************)
lemma cnv_fwd_flat (h) (a) (I) (G) (L):
- â\88\80V,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\95{I}V.T ![h,a] →
- â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a].
+ â\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© ⊢ 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 #_ #_
qed-.
lemma cnv_fwd_pair_sn (h) (a) (I) (G) (L):
- â\88\80V,T. â¦\83G,Lâ¦\84 â\8a¢ â\91¡{I}V.T ![h,a] â\86\92 â¦\83G,Lâ¦\84 ⊢ V ![h,a].
+ â\88\80V,T. â\9d¨G,Lâ\9d© â\8a¢ â\91¡[I]V.T ![h,a] â\86\92 â\9d¨G,Lâ\9d© ⊢ 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 #_