+++ /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( ⦃G, L⦄ ⊢ break term 46 T ⁝ break term 46 A )"
- non associative with precedence 45
- for @{ 'AtomicArity $L $T $A }.
--- /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 A )"
+ non associative with precedence 45
+ for @{ 'AtomicArity $G $L $T $A }.
+++ /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( T1 ⁝ ⊑ break term 46 T2 )"
- non associative with precedence 45
- for @{ 'LRSubEqA $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( G ⊢ break term 46 L1 ⁝ ⊑ break term 46 L2 )"
+ non associative with precedence 45
+ for @{ 'LRSubEqA $G $L1 $L2 }.
+++ /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 h , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 g ] break ⦃ term 46 l , break term 46 T2 ⦄ )"
- non associative with precedence 45
- for @{ 'StaticType $h $g $L $T1 $T2 $l }.
--- /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 g ] break ⦃ term 46 l , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'StaticType $h $g $G $L $T1 $T2 $l }.
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/atomicarity_3.ma".
+include "basic_2/notation/relations/atomicarity_4.ma".
include "basic_2/grammar/aarity.ma".
+include "basic_2/grammar/genv.ma".
include "basic_2/relocation/ldrop.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
-inductive aaa: lenv → term → predicate aarity ≝
-| aaa_sort: ∀L,k. aaa L (⋆k) (⓪)
-| aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
-| aaa_abbr: ∀a,L,V,T,B,A.
- aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓ{a}V. T) A
-| aaa_abst: ∀a,L,V,T,B,A.
- aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛ{a}V. T) (②B. A)
-| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (②B. A) → aaa L (ⓐV. T) A
-| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (ⓝV. T) A
+(* activate genv *)
+inductive aaa: relation4 genv lenv term aarity ≝
+| aaa_sort: ∀G,L,k. aaa G L (⋆k) (⓪)
+| aaa_lref: ∀I,G,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I}V → aaa G K V B → aaa G L (#i) B
+| aaa_abbr: ∀a,G,L,V,T,B,A.
+ aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{a}V.T) A
+| aaa_abst: ∀a,G,L,V,T,B,A.
+ aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ{a}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
.
interpretation "atomic arity assignment (term)"
- 'AtomicArity L T A = (aaa L T A).
+ 'AtomicArity G L T A = (aaa G L T A).
(* Basic inversion lemmas ***************************************************)
-fact aaa_inv_sort_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀k. T = ⋆k → A = ⓪.
-#L #T #A * -L -T -A
+fact aaa_inv_sort_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀k. T = ⋆k → A = ⓪.
+#G #L #T #A * -G -L -T -A
[ //
-| #I #L #K #V #B #i #_ #_ #k #H destruct
-| #a #L #V #T #B #A #_ #_ #k #H destruct
-| #a #L #V #T #B #A #_ #_ #k #H destruct
-| #L #V #T #B #A #_ #_ #k #H destruct
-| #L #V #T #A #_ #_ #k #H destruct
+| #I #G #L #K #V #B #i #_ #_ #k #H destruct
+| #a #G #L #V #T #B #A #_ #_ #k #H destruct
+| #a #G #L #V #T #B #A #_ #_ #k #H destruct
+| #G #L #V #T #B #A #_ #_ #k #H destruct
+| #G #L #V #T #A #_ #_ #k #H destruct
]
-qed.
-
-lemma aaa_inv_sort: ∀L,A,k. ⦃G, L⦄ ⊢ ⋆k ⁝ A → A = ⓪.
-/2 width=5/ qed-.
-
-fact aaa_inv_lref_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #i →
- ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A.
-#L #T #A * -L -T -A
-[ #L #k #i #H destruct
-| #I #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/
-| #a #L #V #T #B #A #_ #_ #i #H destruct
-| #a #L #V #T #B #A #_ #_ #i #H destruct
-| #L #V #T #B #A #_ #_ #i #H destruct
-| #L #V #T #A #_ #_ #i #H destruct
+qed-.
+
+lemma aaa_inv_sort: ∀G,L,A,k. ⦃G, L⦄ ⊢ ⋆k ⁝ A → A = ⓪.
+/2 width=6 by aaa_inv_sort_aux/ qed-.
+
+fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #i →
+ ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #i #H destruct
+| #I #G #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/
+| #a #G #L #V #T #B #A #_ #_ #i #H destruct
+| #a #G #L #V #T #B #A #_ #_ #i #H destruct
+| #G #L #V #T #B #A #_ #_ #i #H destruct
+| #G #L #V #T #A #_ #_ #i #H destruct
]
-qed.
-
-lemma aaa_inv_lref: ∀L,A,i. ⦃G, L⦄ ⊢ #i ⁝ A →
- ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A.
-/2 width=3/ qed-.
-
-fact aaa_inv_gref_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p. T = §p → ⊥.
-#L #T #A * -L -T -A
-[ #L #k #q #H destruct
-| #I #L #K #V #B #i #HLK #HB #q #H destruct
-| #a #L #V #T #B #A #_ #_ #q #H destruct
-| #a #L #V #T #B #A #_ #_ #q #H destruct
-| #L #V #T #B #A #_ #_ #q #H destruct
-| #L #V #T #A #_ #_ #q #H destruct
+qed-.
+
+lemma aaa_inv_lref: ∀G,L,A,i. ⦃G, L⦄ ⊢ #i ⁝ A →
+ ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+/2 width=3 by aaa_inv_lref_aux/ qed-.
+
+fact aaa_inv_gref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p. T = §p → ⊥.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #q #H destruct
+| #I #G #L #K #V #B #i #HLK #HB #q #H destruct
+| #a #G #L #V #T #B #A #_ #_ #q #H destruct
+| #a #G #L #V #T #B #A #_ #_ #q #H destruct
+| #G #L #V #T #B #A #_ #_ #q #H destruct
+| #G #L #V #T #A #_ #_ #q #H destruct
]
-qed.
-
-lemma aaa_inv_gref: ∀L,A,p. ⦃G, L⦄ ⊢ §p ⁝ A → ⊥.
-/2 width=6/ qed-.
-
-fact aaa_inv_abbr_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U →
- ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & L. ⓓW ⊢ U ⁝ A.
-#L #T #A * -L -T -A
-[ #L #k #a #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #a #W #U #H destruct
-| #b #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=2/
-| #b #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #L #V #T #A #_ #_ #a #W #U #H destruct
+qed-.
+
+lemma aaa_inv_gref: ∀G,L,A,p. ⦃G, L⦄ ⊢ §p ⁝ A → ⊥.
+/2 width=7 by aaa_inv_gref_aux/ qed-.
+
+fact aaa_inv_abbr_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U →
+ ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L.ⓓW⦄ ⊢ U ⁝ A.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #a #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
+| #b #G #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=2/
+| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #G #L #V #T #A #_ #_ #a #W #U #H destruct
]
-qed.
-
-lemma aaa_inv_abbr: ∀a,L,V,T,A. ⦃G, L⦄ ⊢ ⓓ{a}V. T ⁝ A →
- ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & L. ⓓV ⊢ T ⁝ A.
-/2 width=4/ qed-.
-
-fact aaa_inv_abst_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓛ{a}W. U →
- ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & L. ⓛW ⊢ U ⁝ B2 & A = ②B1. B2.
-#L #T #A * -L -T -A
-[ #L #k #a #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #a #W #U #H destruct
-| #b #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #b #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=5/
-| #L #V #T #B #A #_ #_ #a #W #U #H destruct
-| #L #V #T #A #_ #_ #a #W #U #H destruct
+qed-.
+
+lemma aaa_inv_abbr: ∀a,G,L,V,T,A. ⦃G, L⦄ ⊢ ⓓ{a}V. T ⁝ A →
+ ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L.ⓓV⦄ ⊢ T ⁝ A.
+/2 width=4 by aaa_inv_abbr_aux/ qed-.
+
+fact aaa_inv_abst_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀a,W,U. T = ⓛ{a}W. U →
+ ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & ⦃G, L.ⓛW⦄ ⊢ U ⁝ B2 & A = ②B1.B2.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #a #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
+| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #b #G #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=5/
+| #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #G #L #V #T #A #_ #_ #a #W #U #H destruct
]
-qed.
-
-lemma aaa_inv_abst: ∀a,L,W,T,A. ⦃G, L⦄ ⊢ ⓛ{a}W. T ⁝ A →
- ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & L. ⓛW ⊢ T ⁝ B2 & A = ②B1. B2.
-/2 width=4/ qed-.
-
-fact aaa_inv_appl_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓐW. U →
- ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L⦄ ⊢ U ⁝ ②B. A.
-#L #T #A * -L -T -A
-[ #L #k #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3/
-| #L #V #T #A #_ #_ #W #U #H destruct
+qed-.
+
+lemma aaa_inv_abst: ∀a,G,L,W,T,A. ⦃G, L⦄ ⊢ ⓛ{a}W. T ⁝ A →
+ ∃∃B1,B2. ⦃G, L⦄ ⊢ W ⁝ B1 & ⦃G, L.ⓛW⦄ ⊢ T ⁝ B2 & A = ②B1.B2.
+/2 width=4 by aaa_inv_abst_aux/ qed-.
+
+fact aaa_inv_appl_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
+ ∃∃B. ⦃G, L⦄ ⊢ W ⁝ B & ⦃G, L⦄ ⊢ U ⁝ ②B.A.
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #G #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3/
+| #G #L #V #T #A #_ #_ #W #U #H destruct
]
-qed.
+qed-.
-lemma aaa_inv_appl: ∀L,V,T,A. ⦃G, L⦄ ⊢ ⓐV. T ⁝ A →
- ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L⦄ ⊢ T ⁝ ②B. A.
-/2 width=3/ qed-.
+lemma aaa_inv_appl: ∀G,L,V,T,A. ⦃G, L⦄ ⊢ ⓐV.T ⁝ A →
+ ∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L⦄ ⊢ T ⁝ ②B.A.
+/2 width=3 by aaa_inv_appl_aux/ qed-.
-fact aaa_inv_cast_aux: ∀L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓝW. U →
+fact aaa_inv_cast_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓝW. U →
⦃G, L⦄ ⊢ W ⁝ A ∧ ⦃G, L⦄ ⊢ U ⁝ A.
-#L #T #A * -L -T -A
-[ #L #k #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #a #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #A #HV #HT #W #U #H destruct /2 width=1/
+#G #L #T #A * -G -L -T -A
+[ #G #L #k #W #U #H destruct
+| #I #G #L #K #V #B #i #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #G #L #V #T #B #A #_ #_ #W #U #H destruct
+| #G #L #V #T #A #HV #HT #W #U #H destruct /2 width=1/
]
-qed.
+qed-.
-lemma aaa_inv_cast: ∀L,W,T,A. ⦃G, L⦄ ⊢ ⓝW. T ⁝ A →
+lemma aaa_inv_cast: ∀G,L,W,T,A. ⦃G, L⦄ ⊢ ⓝW. T ⁝ A →
⦃G, L⦄ ⊢ W ⁝ A ∧ ⦃G, L⦄ ⊢ T ⁝ A.
-/2 width=3/ qed-.
+/2 width=3 by aaa_inv_cast_aux/ qed-.
(* Main properties **********************************************************)
-theorem aaa_mono: ∀L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
-#L #T #A1 #H elim H -L -T -A1
-[ #L #k #A2 #H
+theorem aaa_mono: ∀G,L,T,A1. ⦃G, L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G, L⦄ ⊢ T ⁝ A2 → A1 = A2.
+#G #L #T #A1 #H elim H -G -L -T -A1
+[ #G #L #k #A2 #H
>(aaa_inv_sort … H) -H //
-| #I1 #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
+| #I1 #G #L #K1 #V1 #B #i #HLK1 #_ #IHA1 #A2 #H
elim (aaa_inv_lref … H) -H #I2 #K2 #V2 #HLK2 #HA2
lapply (ldrop_mono … HLK1 … HLK2) -L #H destruct /2 width=1/
-| #a #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
+| #a #G #L #V #T #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_abbr … H) -H /2 width=1/
-| #a #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
+| #a #G #L #V1 #T1 #B1 #A1 #_ #_ #IHB1 #IHA1 #X #H
elim (aaa_inv_abst … H) -H #B2 #A2 #HB2 #HA2 #H destruct /3 width=1/
-| #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
+| #G #L #V1 #T1 #B1 #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_appl … H) -H #B2 #_ #HA2
lapply (IHA1 … HA2) -L #H destruct //
-| #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
+| #G #L #V #T #A1 #_ #_ #_ #IHA1 #A2 #H
elim (aaa_inv_cast … H) -H /2 width=1/
]
qed-.
(* Properties concerning basic relocation ***********************************)
-lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T2. ⇧[d, e] T1 ≡ T2 → L2 ⊢ T2 ⁝ A.
-#L1 #T1 #A #H elim H -L1 -T1 -A
-[ #L1 #k #L2 #d #e #_ #T2 #H
+lemma aaa_lift: ∀G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+#G #L1 #T1 #A #H elim H -G -L1 -T1 -A
+[ #G #L1 #k #L2 #d #e #_ #T2 #H
>(lift_inv_sort1 … H) -H //
-| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L2 #d #e #HL21 #T2 #H
elim (lift_inv_lref1 … H) -H * #Hid #H destruct
[ elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
/3 width=8/
| lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
]
-| #a #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
/4 width=4/
-| #a #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+| #a #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
elim (lift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
/4 width=4/
-| #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
+| #G #L1 #V1 #T1 #B #A #_ #_ #IHB #IHA #L2 #d #e #HL21 #X #H
elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
/3 width=4/
-| #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H
+| #G #L1 #V1 #T1 #A #_ #_ #IH1 #IH2 #L2 #d #e #HL21 #X #H
elim (lift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
/3 width=4/
]
qed.
-lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ⁝ A.
-#L2 #T2 #A #H elim H -L2 -T2 -A
-[ #L2 #k #L1 #d #e #_ #T1 #H
+lemma aaa_inv_lift: ∀G,L2,T2,A. ⦃G, L2⦄ ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T1. ⇧[d, e] T1 ≡ T2 → ⦃G, L1⦄ ⊢ T1 ⁝ A.
+#G #L2 #T2 #A #H elim H -G -L2 -T2 -A
+[ #G #L2 #k #L1 #d #e #_ #T1 #H
>(lift_inv_sort2 … H) -H //
-| #I #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H
+| #I #G #L2 #K2 #V2 #B #i #HLK2 #_ #IHB #L1 #d #e #HL21 #T1 #H
elim (lift_inv_lref2 … H) -H * #Hid #H destruct
[ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/
| lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // -Hid /3 width=8/
]
-| #a #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
/4 width=4/
-| #a #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+| #a #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
/4 width=4/
-| #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
+| #G #L2 #V2 #T2 #B #A #_ #_ #IHB #IHA #L1 #d #e #HL21 #X #H
elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
/3 width=4/
-| #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H
+| #G #L2 #V2 #T2 #A #_ #_ #IH1 #IH2 #L1 #d #e #HL21 #X #H
elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
/3 width=4/
]
(* Properties concerning generic relocation *********************************)
-lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →
- L1 ⊢ T1 ⁝ A → L2 ⊢ T2 ⁝ A.
-#L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des
+lemma aaa_lifts: ∀G,L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →
+ ⦃G, L1⦄ ⊢ T1 ⁝ A → ⦃G, L2⦄ ⊢ T2 ⁝ A.
+#G #L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des
[ #L #T1 #H #HT1
<(lifts_inv_nil … H) -H //
| #L1 #L #L2 #des #d #e #_ #HL2 #IHL1 #T1 #H #HT1
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lrsubeqa_2.ma".
+include "basic_2/notation/relations/lrsubeqa_3.ma".
+include "basic_2/static/aaa.ma". (**) (* disambiguation error *)
include "basic_2/substitution/lsubr.ma".
-include "basic_2/static/aaa.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
-inductive lsuba: relation lenv ≝
-| lsuba_atom: lsuba (⋆) (⋆)
-| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1.ⓑ{I}V) (L2.ⓑ{I}V)
-| lsuba_abbr: ∀L1,L2,W,V,A. L1 ⊢ ⓝW.V ⁝ A → L2 ⊢ W ⁝ A →
- lsuba L1 L2 → lsuba (L1.ⓓⓝW.V) (L2.ⓛW)
+inductive lsuba (G:genv): relation lenv ≝
+| lsuba_atom: lsuba G (⋆) (⋆)
+| lsuba_pair: ∀I,L1,L2,V. lsuba G L1 L2 → lsuba G (L1.ⓑ{I}V) (L2.ⓑ{I}V)
+| lsuba_abbr: ∀L1,L2,W,V,A. ⦃G, L1⦄ ⊢ ⓝW.V ⁝ A → ⦃G, L2⦄ ⊢ W ⁝ A →
+ lsuba G L1 L2 → lsuba G (L1.ⓓⓝW.V) (L2.ⓛW)
.
interpretation
"local environment refinement (atomic arity assigment)"
- 'LRSubEqA L1 L2 = (lsuba L1 L2).
+ 'LRSubEqA G L1 L2 = (lsuba G L1 L2).
(* Basic inversion lemmas ***************************************************)
-fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ⁝⊑ L2 → L1 = ⋆ → L2 = ⋆.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_atom1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
| #L1 #L2 #W #V #A #_ #_ #_ #H destruct
]
qed-.
-lemma lsuba_inv_atom1: ∀L2. ⋆ ⁝⊑ L2 → L2 = ⋆.
-/2 width=3 by lsuba_inv_atom1_aux/ qed-.
+lemma lsuba_inv_atom1: ∀G,L2. G ⊢ ⋆ ⁝⊑ L2 → L2 = ⋆.
+/2 width=4 by lsuba_inv_atom1_aux/ qed-.
-fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
- (∃∃K2. K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
- ∃∃K2,W,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
- I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_pair1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ (∃∃K2. G ⊢ K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⁝⊑ K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+#G #L1 #L2 * -L1 -L2
[ #J #K1 #X #H destruct
| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
| #L1 #L2 #W #V #A #HV #HW #HL12 #J #K1 #X #H destruct /3 width=9/
]
qed-.
-lemma lsuba_inv_pair1: ∀I,K1,L2,X. K1.ⓑ{I}X ⁝⊑ L2 →
- (∃∃K2. K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
- ∃∃K2,W,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+lemma lsuba_inv_pair1: ∀I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⁝⊑ L2 →
+ (∃∃K2. G ⊢ K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⁝⊑ K2 &
I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
/2 width=3 by lsuba_inv_pair1_aux/ qed-.
-fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ⁝⊑ L2 → L2 = ⋆ → L1 = ⋆.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → L2 = ⋆ → L1 = ⋆.
+#G #L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
| #L1 #L2 #W #V #A #_ #_ #_ #H destruct
]
qed-.
-lemma lsubc_inv_atom2: ∀L1. L1 ⁝⊑ ⋆ → L1 = ⋆.
-/2 width=3 by lsuba_inv_atom2_aux/ qed-.
+lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⁝⊑ ⋆ → L1 = ⋆.
+/2 width=4 by lsuba_inv_atom2_aux/ qed-.
-fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
- (∃∃K1. K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
- ∃∃K1,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
- I = Abst & L1 = K1.ⓓⓝW.V.
-#L1 #L2 * -L1 -L2
+fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
+ (∃∃K1. G ⊢ K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
+ ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⁝⊑ K2 & I = Abst & L1 = K1.ⓓⓝW.V.
+#G #L1 #L2 * -L1 -L2
[ #J #K2 #U #H destruct
| #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3/
| #L1 #L2 #W #V #A #HV #HW #HL12 #J #K2 #U #H destruct /3 width=7/
]
qed-.
-lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ⁝⊑ K2.ⓑ{I}W →
- (∃∃K1. K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
- ∃∃K1,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
+lemma lsuba_inv_pair2: ∀I,G,L1,K2,W. G ⊢ L1 ⁝⊑ K2.ⓑ{I}W →
+ (∃∃K1. G ⊢ K1 ⁝⊑ K2 & L1 = K1.ⓑ{I}W) ∨
+ ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⁝⊑ K2 &
I = Abst & L1 = K1.ⓓⓝW.V.
/2 width=3 by lsuba_inv_pair2_aux/ qed-.
(* Basic forward lemmas *****************************************************)
-lemma lsuba_fwd_lsubr: ∀L1,L2. L1 ⁝⊑ L2 → L1 ⊑ L2.
-#L1 #L2 #H elim H -L1 -L2 // /2 width=1/
+lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → L1 ⊑ L2.
+#G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/
qed-.
(* Basic properties *********************************************************)
-lemma lsuba_refl: ∀L. L ⁝⊑ L.
-#L elim L -L // /2 width=1/
+lemma lsuba_refl: ∀G,L. G ⊢ L ⁝⊑ L.
+#G #L elim L -L // /2 width=1/
qed.
(* Properties concerning atomic arity assignment ****************************)
-lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ⁝ A → ∀L2. L1 ⁝⊑ L2 → L2 ⊢ V ⁝ A.
-#L1 #V #A #H elim H -L1 -V -A
+lemma lsuba_aaa_conf: ∀G,L1,V,A. ⦃G, L1⦄ ⊢ V ⁝ A →
+ ∀L2. G ⊢ L1 ⁝⊑ L2 → ⦃G, L2⦄ ⊢ V ⁝ A.
+#G #L1 #V #A #H elim H -G -L1 -V -A
[ //
-| #I #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12
+| #I #G #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12
elim (lsuba_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2
elim (lsuba_inv_pair1 … H) -H * #K2
[ #HK12 #H destruct /3 width=5/
]
qed-.
-lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ⁝ A → ∀L1. L1 ⁝⊑ L2 → L1 ⊢ V ⁝ A.
-#L2 #V #A #H elim H -L2 -V -A
+lemma lsuba_aaa_trans: ∀G,L2,V,A. ⦃G, L2⦄ ⊢ V ⁝ A →
+ ∀L1. G ⊢ L1 ⁝⊑ L2 → ⦃G, L1⦄ ⊢ V ⁝ A.
+#G #L2 #V #A #H elim H -G -L2 -V -A
[ //
-| #I #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12
+| #I #G #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12
elim (lsuba_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1
elim (lsuba_inv_pair2 … H) -H * #K1
[ #HK12 #H destruct /3 width=5/
(* Properties concerning basic local environment slicing ********************)
(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
- ∃∃K2. K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
-#L1 #L2 #H elim H -L1 -L2
+lemma lsuba_ldrop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. G ⊢ K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
+#G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3/
| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK1
qed-.
(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
-#L1 #L2 #H elim H -L1 -L2
+lemma lsuba_ldrop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. G ⊢ K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
+#G #L1 #L2 #H elim H -L1 -L2
[ /2 width=3/
| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK2
(* Main properties **********************************************************)
-theorem lsuba_trans: ∀L1,L. L1 ⁝⊑ L → ∀L2. L ⁝⊑ L2 → L1 ⁝⊑ L2.
-#L1 #L #H elim H -L1 -L
+theorem lsuba_trans: ∀G,L1,L. G ⊢ L1 ⁝⊑ L → ∀L2. G ⊢ L ⁝⊑ L2 → G ⊢ L1 ⁝⊑ L2.
+#G #L1 #L #H elim H -L1 -L
[ #X #H >(lsuba_inv_atom1 … H) -H //
| #I #L1 #L #Y #HL1 #IHL1 #X #H
elim (lsuba_inv_pair1 … H) -H * #L2
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/statictype_6.ma".
+include "basic_2/notation/relations/statictype_7.ma".
+include "basic_2/grammar/genv.ma". (**) (* disambiguation error *)
include "basic_2/relocation/ldrop.ma".
include "basic_2/static/sd.ma".
(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
-inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝
-| ssta_sort: ∀L,k,l. deg h g k l → ssta h g l L (⋆k) (⋆(next h k))
-| ssta_ldef: ∀L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l K V W →
- ⇧[0, i + 1] W ≡ U → ssta h g l L (#i) U
-| ssta_ldec: ∀L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l K W V →
- ⇧[0, i + 1] W ≡ U → ssta h g (l+1) L (#i) U
-| ssta_bind: ∀a,I,L,V,T,U,l. ssta h g l (L. ⓑ{I} V) T U →
- ssta h g l L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
-| ssta_appl: ∀L,V,T,U,l. ssta h g l L T U →
- ssta h g l L (ⓐV.T) (ⓐV.U)
-| ssta_cast: ∀L,W,T,U,l. ssta h g l L T U → ssta h g l L (ⓝW. T) U
+(* activate genv *)
+inductive ssta (h:sh) (g:sd h): nat → genv → lenv → relation term ≝
+| ssta_sort: ∀G,L,k,l. deg h g k l → ssta h g l G L (⋆k) (⋆(next h k))
+| ssta_ldef: ∀G,L,K,V,W,U,i,l. ⇩[0, i] L ≡ K. ⓓV → ssta h g l G K V W →
+ ⇧[0, i + 1] W ≡ U → ssta h g l G L (#i) U
+| ssta_ldec: ∀G,L,K,W,V,U,i,l. ⇩[0, i] L ≡ K. ⓛW → ssta h g l G K W V →
+ ⇧[0, i + 1] W ≡ U → ssta h g (l+1) G L (#i) U
+| ssta_bind: ∀a,I,G,L,V,T,U,l. ssta h g l G (L. ⓑ{I} V) T U →
+ ssta h g l G L (ⓑ{a,I}V.T) (ⓑ{a,I}V.U)
+| ssta_appl: ∀G,L,V,T,U,l. ssta h g l G L T U →
+ ssta h g l G L (ⓐV.T) (ⓐV.U)
+| ssta_cast: ∀G,L,W,T,U,l. ssta h g l G L T U → ssta h g l G L (ⓝW.T) U
.
interpretation "stratified static type assignment (term)"
- 'StaticType h g L T U l = (ssta h g l L T U).
+ 'StaticType h g G L T U l = (ssta h g l G L T U).
-definition ssta_step: ∀h. sd h → lenv → relation term ≝ λh,g,L,T,U.
+definition ssta_step: ∀h. sd h → genv → lenv → relation term ≝ λh,g,G,L,T,U.
∃l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, U⦄.
(* Basic inversion lemmas ************************************************)
-fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀k0. T = ⋆k0 →
+fact ssta_inv_sort1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀k0. T = ⋆k0 →
deg h g k0 l ∧ U = ⋆(next h k0).
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #Hkl #k0 #H destruct /2 width=1/
-| #L #K #V #W #U #i #l #_ #_ #_ #k0 #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #k0 #H destruct
-| #a #I #L #V #T #U #l #_ #k0 #H destruct
-| #L #V #T #U #l #_ #k0 #H destruct
-| #L #W #T #U #l #_ #k0 #H destruct
-qed.
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #Hkl #k0 #H destruct /2 width=1/
+| #G #L #K #V #W #U #i #l #_ #_ #_ #k0 #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #k0 #H destruct
+| #a #I #G #L #V #T #U #l #_ #k0 #H destruct
+| #G #L #V #T #U #l #_ #k0 #H destruct
+| #G #L #W #T #U #l #_ #k0 #H destruct
+qed-.
(* Basic_1: was just: sty0_gen_sort *)
-lemma ssta_inv_sort1: ∀h,g,L,U,k,l. ⦃G, L⦄ ⊢ ⋆k •[h, g] ⦃l, U⦄ →
+lemma ssta_inv_sort1: ∀h,g,G,L,U,k,l. ⦃G, L⦄ ⊢ ⋆k •[h, g] ⦃l, U⦄ →
deg h g k l ∧ U = ⋆(next h k).
-/2 width=4/ qed-.
+/2 width=5 by ssta_inv_sort1_aux/ qed-.
-fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀j. T = #j →
- (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
+fact ssta_inv_lref1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀j. T = #j →
+ (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
⇧[0, j + 1] W ≡ U
) ∨
- (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
+ (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃G, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
⇧[0, j + 1] W ≡ U & l = l0 + 1
).
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #j #H destruct
-| #L #K #V #W #U #i #l #HLK #HVW #HWU #j #H destruct /3 width=6/
-| #L #K #W #V #U #i #l #HLK #HWV #HWU #j #H destruct /3 width=8/
-| #a #I #L #V #T #U #l #_ #j #H destruct
-| #L #V #T #U #l #_ #j #H destruct
-| #L #W #T #U #l #_ #j #H destruct
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #j #H destruct
+| #G #L #K #V #W #U #i #l #HLK #HVW #HWU #j #H destruct /3 width=6/
+| #G #L #K #W #V #U #i #l #HLK #HWV #HWU #j #H destruct /3 width=8/
+| #a #I #G #L #V #T #U #l #_ #j #H destruct
+| #G #L #V #T #U #l #_ #j #H destruct
+| #G #L #W #T #U #l #_ #j #H destruct
]
-qed.
+qed-.
(* Basic_1: was just: sty0_gen_lref *)
-lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃G, L⦄ ⊢ #i •[h, g] ⦃l, U⦄ →
- (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
+lemma ssta_inv_lref1: ∀h,g,G,L,U,i,l. ⦃G, L⦄ ⊢ #i •[h, g] ⦃l, U⦄ →
+ (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V •[h, g] ⦃l, W⦄ &
⇧[0, i + 1] W ≡ U
) ∨
- (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
+ (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃G, K⦄ ⊢ W •[h, g] ⦃l0, V⦄ &
⇧[0, i + 1] W ≡ U & l = l0 + 1
).
-/2 width=3/ qed-.
-
-fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #p0 #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct
-| #a #I #L #V #T #U #l #_ #p0 #H destruct
-| #L #V #T #U #l #_ #p0 #H destruct
-| #L #W #T #U #l #_ #p0 #H destruct
-qed.
-
-lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃G, L⦄ ⊢ §p •[h, g] ⦃l, U⦄ → ⊥.
-/2 width=9/ qed-.
-
-fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
+/2 width=3 by ssta_inv_lref1_aux/ qed-.
+
+fact ssta_inv_gref1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥.
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #p0 #H destruct
+| #G #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #p0 #H destruct
+| #a #I #G #L #V #T #U #l #_ #p0 #H destruct
+| #G #L #V #T #U #l #_ #p0 #H destruct
+| #G #L #W #T #U #l #_ #p0 #H destruct
+qed-.
+
+lemma ssta_inv_gref1: ∀h,g,G,L,U,p,l. ⦃G, L⦄ ⊢ §p •[h, g] ⦃l, U⦄ → ⊥.
+/2 width=10 by ssta_inv_gref1_aux/ qed-.
+
+fact ssta_inv_bind1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
∀a,I,X,Y. T = ⓑ{a,I}Y.X →
- ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #a #I #X #Y #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
-| #b #J #L #V #T #U #l #HTU #a #I #X #Y #H destruct /2 width=3/
-| #L #V #T #U #l #_ #a #I #X #Y #H destruct
-| #L #W #T #U #l #_ #a #I #X #Y #H destruct
+ ∃∃Z. ⦃G, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #a #I #X #Y #H destruct
+| #G #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #a #I #X #Y #H destruct
+| #b #J #G #L #V #T #U #l #HTU #a #I #X #Y #H destruct /2 width=3/
+| #G #L #V #T #U #l #_ #a #I #X #Y #H destruct
+| #G #L #W #T #U #l #_ #a #I #X #Y #H destruct
]
-qed.
+qed-.
(* Basic_1: was just: sty0_gen_bind *)
-lemma ssta_inv_bind1: ∀h,g,a,I,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓑ{a,I}Y.X •[h, g] ⦃l, U⦄ →
- ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
-/2 width=3/ qed-.
+lemma ssta_inv_bind1: ∀h,g,a,I,G,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓑ{a,I}Y.X •[h, g] ⦃l, U⦄ →
+ ∃∃Z. ⦃G, L.ⓑ{I}Y⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z.
+/2 width=3 by ssta_inv_bind1_aux/ qed-.
-fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀X,Y. T = ⓐY.X →
+fact ssta_inv_appl1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ∀X,Y. T = ⓐY.X →
∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓐY.Z.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #X #Y #H destruct
-| #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #i #l #_ #_ #_ #X #Y #H destruct
-| #a #I #L #V #T #U #l #_ #X #Y #H destruct
-| #L #V #T #U #l #HTU #X #Y #H destruct /2 width=3/
-| #L #W #T #U #l #_ #X #Y #H destruct
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #X #Y #H destruct
+| #G #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct
+| #G #L #K #W #V #U #i #l #_ #_ #_ #X #Y #H destruct
+| #a #I #G #L #V #T #U #l #_ #X #Y #H destruct
+| #G #L #V #T #U #l #HTU #X #Y #H destruct /2 width=3/
+| #G #L #W #T #U #l #_ #X #Y #H destruct
]
-qed.
+qed-.
(* Basic_1: was just: sty0_gen_appl *)
-lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓐY.X •[h, g] ⦃l, U⦄ →
+lemma ssta_inv_appl1: ∀h,g,G,L,Y,X,U,l. ⦃G, L⦄ ⊢ ⓐY.X •[h, g] ⦃l, U⦄ →
∃∃Z. ⦃G, L⦄ ⊢ X •[h, g] ⦃l, Z⦄ & U = ⓐY.Z.
-/2 width=3/ qed-.
+/2 width=3 by ssta_inv_appl1_aux/ qed-.
-fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
+fact ssta_inv_cast1_aux: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
∀X,Y. T = ⓝY.X → ⦃G, L⦄ ⊢ X •[h, g] ⦃l, U⦄.
-#h #g #L #T #U #l * -L -T -U -l
-[ #L #k #l #_ #X #Y #H destruct
-| #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct
-| #L #K #W #V #U #l #i #_ #_ #_ #X #Y #H destruct
-| #a #I #L #V #T #U #l #_ #X #Y #H destruct
-| #L #V #T #U #l #_ #X #Y #H destruct
-| #L #W #T #U #l #HTU #X #Y #H destruct //
+#h #g #G #L #T #U #l * -G -L -T -U -l
+[ #G #L #k #l #_ #X #Y #H destruct
+| #G #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct
+| #G #L #K #W #V #U #l #i #_ #_ #_ #X #Y #H destruct
+| #a #I #G #L #V #T #U #l #_ #X #Y #H destruct
+| #G #L #V #T #U #l #_ #X #Y #H destruct
+| #G #L #W #T #U #l #HTU #X #Y #H destruct //
]
-qed.
+qed-.
(* Basic_1: was just: sty0_gen_cast *)
-lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃G, L⦄ ⊢ ⓝY.X •[h, g] ⦃l, U⦄ →
+lemma ssta_inv_cast1: ∀h,g,G,L,X,Y,U,l. ⦃G, L⦄ ⊢ ⓝY.X •[h, g] ⦃l, U⦄ →
⦃G, L⦄ ⊢ X •[h, g] ⦃l, U⦄.
-/2 width=4/ qed-.
+/2 width=4 by ssta_inv_cast1_aux/ qed-.
(* Properties on atomic arity assignment for terms **************************)
-lemma ssta_aaa: ∀h,g,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ⦃G, L⦄ ⊢ U ⁝ A.
-#h #g #L #T #A #H elim H -L -T -A
-[ #L #k #U #l #H
+lemma ssta_aaa: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ → ⦃G, L⦄ ⊢ U ⁝ A.
+#h #g #G #L #T #A #H elim H -G -L -T -A
+[ #G #L #k #U #l #H
elim (ssta_inv_sort1 … H) -H #_ #H destruct //
-| #I #L #K #V #B #i #HLK #HV #IHV #U #l #H
+| #I #G #L #K #V #B #i #HLK #HV #IHV #U #l #H
elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0 ] #HLK0 #HVW0 #HU [ #H ]
lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
@(aaa_lift … HLK … HU) -HU -L // -HV /2 width=2/
-| #a #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
+| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/
-| #a #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
+| #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/
-| #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
+| #G #L #V #T #B #A #HV #_ #_ #IHT #X #l #H
elim (ssta_inv_appl1 … H) -H #U #HTU #H destruct /3 width=3/
-| #L #V #T #A #_ #_ #IHV #IHT #X #l #H
+| #G #L #V #T #A #_ #_ #IHV #IHT #X #l #H
lapply (ssta_inv_cast1 … H) -H /2 width=2/
]
qed.
(* *)
(**************************************************************************)
+include "basic_2/static/ssta.ma". (**) (* disambiguation error *)
include "basic_2/relocation/ldrop_ldrop.ma".
-include "basic_2/static/ssta.ma".
(* STRATIFIED STATIC TYPE ASSIGNMENT ON TERMS *******************************)
(* Properties on relocation *************************************************)
(* Basic_1: was just: sty0_lift *)
-lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
+lemma ssta_lift: ∀h,g,G,L1,T1,U1,l. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ →
∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 →
- ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄.
-#h #g #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l
-[ #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+ ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄.
+#h #g #G #L1 #T1 #U1 #l #H elim H -G -L1 -T1 -U1 -l
+[ #G #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2
>(lift_inv_sort1 … H1) -X1
>(lift_inv_sort1 … H2) -X2 /2 width=1/
-| #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+| #G #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hid #H destruct
[ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
| lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
]
-| #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+| #G #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
elim (lift_inv_lref1 … H) * #Hid #H destruct
[ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
| lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
]
-| #a #I #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+| #a #I #G #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
-| #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+| #G #L1 #V1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
-| #L1 #W1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+| #G #L1 #W1 #T1 #U1 #l #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
elim (lift_inv_flat1 … H) -H #W2 #T2 #HW12 #HT12 #H destruct /3 width=5/
]
qed.
(* Note: apparently this was missing in basic_1 *)
-lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ →
+lemma ssta_inv_lift1: ∀h,g,G,L2,T2,U2,l. ⦃G, L2⦄ ⊢ T2 •[h, g] ⦃l, U2⦄ →
∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ & ⇧[d, e] U1 ≡ U2.
-#h #g #L2 #T2 #U2 #l #H elim H -L2 -T2 -U2 -l
-[ #L2 #k #l #Hkl #L1 #d #e #_ #X #H
+ ∃∃U1. ⦃G, L1⦄ ⊢ T1 •[h, g] ⦃l, U1⦄ & ⇧[d, e] U1 ≡ U2.
+#h #g #G #L2 #T2 #U2 #l #H elim H -G -L2 -T2 -U2 -l
+[ #G #L2 #k #l #Hkl #L1 #d #e #_ #X #H
>(lift_inv_sort2 … H) -X /3 width=3/
-| #L2 #K2 #V2 #W2 #W #i #l #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H
+| #G #L2 #K2 #V2 #W2 #W #i #l #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H
elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ]
[ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12
elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12
| <le_plus_minus_comm //
]
]
-| #L2 #K2 #W2 #V2 #W #i #l #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H
+| #G #L2 #K2 #W2 #V2 #W #i #l #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H
elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HWV2 | -IHWV2 ]
[ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #W1 #HLK1 #HK21 #HW12
elim (IHWV2 … HK21 … HW12) -K2 #V1 #HWV1 #_
| <le_plus_minus_comm //
]
]
-| #a #I #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+| #a #I #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/
-| #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+| #G #L2 #V2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/
-| #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
+| #G #L2 #W2 #T2 #U2 #l #_ #IHTU2 #L1 #d #e #HL21 #X #H
elim (lift_inv_flat2 … H) -H #W1 #T1 #HW12 #HT12 #H destruct
elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=3/
]
-qed.
+qed-.
(* Advanced forvard lemmas **************************************************)
(* Basic_1: was just: sty0_correct *)
-lemma ssta_fwd_correct: ∀h,g,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
+lemma ssta_fwd_correct: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l, U⦄ →
∃T0. ⦃G, L⦄ ⊢ U •[h, g] ⦃l-1, T0⦄.
-#h #g #L #T #U #l #H elim H -L -T -U -l
+#h #g #G #L #T #U #l #H elim H -G -L -T -U -l
[ /4 width=2/
-| #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
+| #G #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
elim (lift_total V0 0 (i+1)) /3 width=10/
-| #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
+| #G #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
elim (lift_total V 0 (i+1)) /3 width=10/
-| #a #I #L #V #T #U #l #_ * /3 width=2/
-| #L #V #T #U #l #_ * #T0 #HUT0 /3 width=2/
-| #L #W #T #U #l #_ * /2 width=2/
+| #a #I #G #L #V #T #U #l #_ * /3 width=2/
+| #G #L #V #T #U #l #_ * #T0 #HUT0 /3 width=2/
+| #G #L #W #T #U #l #_ * /2 width=2/
]
qed-.
(* Main properties **********************************************************)
(* Note: apparently this was missing in basic_1 *)
-theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃G, L⦄ ⊢ T •[h, g] ⦃l1, U1⦄ →
+theorem ssta_mono: ∀h,g,G,L,T,U1,l1. ⦃G, L⦄ ⊢ T •[h, g] ⦃l1, U1⦄ →
∀U2,l2. ⦃G, L⦄ ⊢ T •[h, g] ⦃l2, U2⦄ → l1 = l2 ∧ U1 = U2.
-#h #g #L #T #U1 #l1 #H elim H -L -T -U1 -l1
-[ #L #k #l #Hkl #X #l2 #H
+#h #g #G #L #T #U1 #l1 #H elim H -G -L -T -U1 -l1
+[ #G #L #k #l #Hkl #X #l2 #H
elim (ssta_inv_sort1 … H) -H #Hkl2 #H destruct
>(deg_mono … Hkl2 … Hkl) -g -L -l2 /2 width=1/
-| #L #K #V #W #U1 #i #l1 #HLK #_ #HWU1 #IHVW #U2 #l2 #H
+| #G #L #K #V #W #U1 #i #l1 #HLK #_ #HWU1 #IHVW #U2 #l2 #H
elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 [2: #l0] #HLK0 #HVW0 #HW0U2
lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
lapply (IHVW … HVW0) -IHVW -HVW0 * #H1 #H2 destruct
>(lift_mono … HWU1 … HW0U2) -W0 -U1 /2 width=1/
-| #L #K #W #V #U1 #i #l1 #HLK #_ #HWU1 #IHWV #U2 #l2 #H
+| #G #L #K #W #V #U1 #i #l1 #HLK #_ #HWU1 #IHWV #U2 #l2 #H
elim (ssta_inv_lref1 … H) -H * #K0 #W0 #V0 [2: #l0 ] #HLK0 #HWV0 #HV0U2
lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct
>(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/
-| #a #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
+| #a #I #G #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct
elim (IHTU1 … HTU2) -T /3 width=1/
-| #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
+| #G #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct
elim (IHTU1 … HTU2) -T /3 width=1/
-| #L #W1 #T #U1 #l1 #_ #IHTU1 #U2 #l2 #H
+| #G #L #W1 #T #U1 #l1 #_ #IHTU1 #U2 #l2 #H
lapply (ssta_inv_cast1 … H) -H #HTU2
elim (IHTU1 … HTU2) -T /2 width=1/
]
(* Advanced inversion lemmas ************************************************)
-lemma ssta_inv_refl_pos: ∀h,g,L,T,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, T⦄ → ⊥.
-#h #g #L #T #l #HTT
+lemma ssta_inv_refl_pos: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T •[h, g] ⦃l+1, T⦄ → ⊥.
+#h #g #G #L #T #l #HTT
elim (ssta_fwd_correct … HTT) <minus_plus_m_m #U #HTU
elim (ssta_mono … HTU … HTT) -h -L #H #_ -T -U
elim (plus_xySz_x_false 0 l 0 ?) //
projects / helm.git / commitdiff