(* *)
(**************************************************************************)
+include "ground/xoa/ex_2_3.ma".
+include "ground/xoa/ex_3_2.ma".
include "static_2/notation/relations/atomicarity_4.ma".
include "static_2/syntax/aarity.ma".
include "static_2/syntax/lenv.ma".
(* activate genv *)
inductive aaa: relation4 genv lenv term aarity ≝
| aaa_sort: ∀G,L,s. aaa G L (⋆s) (⓪)
-| aaa_zero: ∀I,G,L,V,B. aaa G L V B → aaa G (L.ⓑ{I}V) (#0) B
-| aaa_lref: ∀I,G,L,A,i. aaa G L (#i) A → aaa G (L.ⓘ{I}) (#↑i) A
+| aaa_zero: ∀I,G,L,V,B. aaa G L V B → aaa G (L.ⓑ[I]V) (#0) B
+| aaa_lref: ∀I,G,L,A,i. aaa G L (#i) A → aaa G (L.ⓘ[I]) (#↑i) A
| aaa_abbr: ∀p,G,L,V,T,B,A.
- aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{p}V.T) A
+ aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ[p]V.T) A
| aaa_abst: ∀p,G,L,V,T,B,A.
- aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ{p}V.T) (②B.A)
+ aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ[p]V.T) (②B.A)
| aaa_appl: ∀G,L,V,T,B,A. aaa G L V B → aaa G L T (②B.A) → aaa G L (ⓐV.T) A
| aaa_cast: ∀G,L,V,T,A. aaa G L V A → aaa G L T A → aaa G L (ⓝV.T) A
.
(* Basic inversion lemmas ***************************************************)
-fact aaa_inv_sort_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 ⊢ T ⁝ A → ∀s. T = ⋆s → A = ⓪.
+fact aaa_inv_sort_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀s. T = ⋆s → A = ⓪.
#G #L #T #A * -G -L -T -A //
[ #I #G #L #V #B #_ #s #H destruct
| #I #G #L #A #i #_ #s #H destruct
]
qed-.
-lemma aaa_inv_sort: â\88\80G,L,A,s. â¦\83G,Lâ¦\84 ⊢ ⋆s ⁝ A → A = ⓪.
+lemma aaa_inv_sort: â\88\80G,L,A,s. â\9d¨G,Lâ\9d© ⊢ ⋆s ⁝ A → A = ⓪.
/2 width=6 by aaa_inv_sort_aux/ qed-.
-fact aaa_inv_zero_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 ⊢ T ⁝ A → T = #0 →
- ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G,K⦄ ⊢ V ⁝ A.
+fact aaa_inv_zero_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → T = #0 →
+ ∃∃I,K,V. L = K.ⓑ[I]V & ❨G,K❩ ⊢ V ⁝ A.
#G #L #T #A * -G -L -T -A /2 width=5 by ex2_3_intro/
[ #G #L #s #H destruct
| #I #G #L #A #i #_ #H destruct
]
qed-.
-lemma aaa_inv_zero: â\88\80G,L,A. â¦\83G,Lâ¦\84 ⊢ #0 ⁝ A →
- ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G,K⦄ ⊢ V ⁝ A.
+lemma aaa_inv_zero: â\88\80G,L,A. â\9d¨G,Lâ\9d© ⊢ #0 ⁝ A →
+ ∃∃I,K,V. L = K.ⓑ[I]V & ❨G,K❩ ⊢ V ⁝ A.
/2 width=3 by aaa_inv_zero_aux/ qed-.
-fact aaa_inv_lref_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 ⊢ T ⁝ A → ∀i. T = #(↑i) →
- ∃∃I,K. L = K.ⓘ{I} & ⦃G,K⦄ ⊢ #i ⁝ A.
+fact aaa_inv_lref_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀i. T = #(↑i) →
+ ∃∃I,K. L = K.ⓘ[I] & ❨G,K❩ ⊢ #i ⁝ A.
#G #L #T #A * -G -L -T -A
[ #G #L #s #j #H destruct
| #I #G #L #V #B #_ #j #H destruct
]
qed-.
-lemma aaa_inv_lref: â\88\80G,L,A,i. â¦\83G,Lâ¦\84 ⊢ #↑i ⁝ A →
- ∃∃I,K. L = K.ⓘ{I} & ⦃G,K⦄ ⊢ #i ⁝ A.
+lemma aaa_inv_lref: â\88\80G,L,A,i. â\9d¨G,Lâ\9d© ⊢ #↑i ⁝ A →
+ ∃∃I,K. L = K.ⓘ[I] & ❨G,K❩ ⊢ #i ⁝ A.
/2 width=3 by aaa_inv_lref_aux/ qed-.
-fact aaa_inv_gref_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 ⊢ T ⁝ A → ∀l. T = §l → ⊥.
+fact aaa_inv_gref_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀l. T = §l → ⊥.
#G #L #T #A * -G -L -T -A
[ #G #L #s #k #H destruct
| #I #G #L #V #B #_ #k #H destruct
]
qed-.
-lemma aaa_inv_gref: â\88\80G,L,A,l. â¦\83G,Lâ¦\84 ⊢ §l ⁝ A → ⊥.
+lemma aaa_inv_gref: â\88\80G,L,A,l. â\9d¨G,Lâ\9d© ⊢ §l ⁝ A → ⊥.
/2 width=7 by aaa_inv_gref_aux/ qed-.
-fact aaa_inv_abbr_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80p,W,U. T = â\93\93{p}W.U →
- â\88\83â\88\83B. â¦\83G,Lâ¦\84 â\8a¢ W â\81\9d B & â¦\83G,L.â\93\93Wâ¦\84 ⊢ U ⁝ A.
+fact aaa_inv_abbr_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© â\8a¢ T â\81\9d A â\86\92 â\88\80p,W,U. T = â\93\93[p]W.U →
+ â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B & â\9d¨G,L.â\93\93Wâ\9d© ⊢ U ⁝ A.
#G #L #T #A * -G -L -T -A
[ #G #L #s #q #W #U #H destruct
| #I #G #L #V #B #_ #q #W #U #H destruct
]
qed-.
-lemma aaa_inv_abbr: â\88\80p,G,L,V,T,A. â¦\83G,Lâ¦\84 â\8a¢ â\93\93{p}V.T ⁝ A →
- â\88\83â\88\83B. â¦\83G,Lâ¦\84 â\8a¢ V â\81\9d B & â¦\83G,L.â\93\93Vâ¦\84 ⊢ T ⁝ A.
+lemma aaa_inv_abbr: â\88\80p,G,L,V,T,A. â\9d¨G,Lâ\9d© â\8a¢ â\93\93[p]V.T ⁝ A →
+ â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ V â\81\9d B & â\9d¨G,L.â\93\93Vâ\9d© ⊢ T ⁝ A.
/2 width=4 by aaa_inv_abbr_aux/ qed-.
-fact aaa_inv_abst_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80p,W,U. T = â\93\9b{p}W.U →
- â\88\83â\88\83B1,B2. â¦\83G,Lâ¦\84 â\8a¢ W â\81\9d B1 & â¦\83G,L.â\93\9bWâ¦\84 ⊢ U ⁝ B2 & A = ②B1.B2.
+fact aaa_inv_abst_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© â\8a¢ T â\81\9d A â\86\92 â\88\80p,W,U. T = â\93\9b[p]W.U →
+ â\88\83â\88\83B1,B2. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B1 & â\9d¨G,L.â\93\9bWâ\9d© ⊢ U ⁝ B2 & A = ②B1.B2.
#G #L #T #A * -G -L -T -A
[ #G #L #s #q #W #U #H destruct
| #I #G #L #V #B #_ #q #W #U #H destruct
]
qed-.
-lemma aaa_inv_abst: â\88\80p,G,L,W,T,A. â¦\83G,Lâ¦\84 â\8a¢ â\93\9b{p}W.T ⁝ A →
- â\88\83â\88\83B1,B2. â¦\83G,Lâ¦\84 â\8a¢ W â\81\9d B1 & â¦\83G,L.â\93\9bWâ¦\84 ⊢ T ⁝ B2 & A = ②B1.B2.
+lemma aaa_inv_abst: â\88\80p,G,L,W,T,A. â\9d¨G,Lâ\9d© â\8a¢ â\93\9b[p]W.T ⁝ A →
+ â\88\83â\88\83B1,B2. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B1 & â\9d¨G,L.â\93\9bWâ\9d© ⊢ T ⁝ B2 & A = ②B1.B2.
/2 width=4 by aaa_inv_abst_aux/ qed-.
-fact aaa_inv_appl_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
- â\88\83â\88\83B. â¦\83G,Lâ¦\84 â\8a¢ W â\81\9d B & â¦\83G,Lâ¦\84 ⊢ U ⁝ ②B.A.
+fact aaa_inv_appl_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
+ â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B & â\9d¨G,Lâ\9d© ⊢ U ⁝ ②B.A.
#G #L #T #A * -G -L -T -A
[ #G #L #s #W #U #H destruct
| #I #G #L #V #B #_ #W #U #H destruct
]
qed-.
-lemma aaa_inv_appl: â\88\80G,L,V,T,A. â¦\83G,Lâ¦\84 ⊢ ⓐV.T ⁝ A →
- â\88\83â\88\83B. â¦\83G,Lâ¦\84 â\8a¢ V â\81\9d B & â¦\83G,Lâ¦\84 ⊢ T ⁝ ②B.A.
+lemma aaa_inv_appl: â\88\80G,L,V,T,A. â\9d¨G,Lâ\9d© ⊢ ⓐV.T ⁝ A →
+ â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ V â\81\9d B & â\9d¨G,Lâ\9d© ⊢ T ⁝ ②B.A.
/2 width=3 by aaa_inv_appl_aux/ qed-.
-fact aaa_inv_cast_aux: â\88\80G,L,T,A. â¦\83G,Lâ¦\84 ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
- â¦\83G,Lâ¦\84 â\8a¢ W â\81\9d A â\88§ â¦\83G,Lâ¦\84 ⊢ U ⁝ A.
+fact aaa_inv_cast_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
+ â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d A â\88§ â\9d¨G,Lâ\9d© ⊢ U ⁝ A.
#G #L #T #A * -G -L -T -A
[ #G #L #s #W #U #H destruct
| #I #G #L #V #B #_ #W #U #H destruct
]
qed-.
-lemma aaa_inv_cast: â\88\80G,L,W,T,A. â¦\83G,Lâ¦\84 ⊢ ⓝW.T ⁝ A →
- â¦\83G,Lâ¦\84 â\8a¢ W â\81\9d A â\88§ â¦\83G,Lâ¦\84 ⊢ T ⁝ A.
+lemma aaa_inv_cast: â\88\80G,L,W,T,A. â\9d¨G,Lâ\9d© ⊢ ⓝW.T ⁝ A →
+ â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d A â\88§ â\9d¨G,Lâ\9d© ⊢ T ⁝ A.
/2 width=3 by aaa_inv_cast_aux/ qed-.