+++ /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 c , break term 46 h ] break term 46 T2 )"
- non associative with precedence 45
- for @{ 'PRedTy $c $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 Rt , break term 46 c , break term 46 h ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PRedTy $Rt $c $h $G $L $T1 $T2 }.
include "ground_2/steps/rtc_max.ma".
include "ground_2/steps/rtc_plus.ma".
-include "basic_2/notation/relations/predty_6.ma".
+include "basic_2/notation/relations/predty_7.ma".
include "basic_2/grammar/lenv.ma".
include "basic_2/grammar/genv.ma".
include "basic_2/relocation/lifts.ma".
(* COUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
(* avtivate genv *)
-inductive cpg (h): rtc → relation4 genv lenv term term ≝
-| cpg_atom : ∀I,G,L. cpg h (𝟘𝟘) G L (⓪{I}) (⓪{I})
-| cpg_ess : ∀G,L,s. cpg h (𝟘𝟙) G L (⋆s) (⋆(next h s))
-| cpg_delta: ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
- ⬆*[1] V2 ≡ W2 → cpg h c G (L.ⓓV1) (#0) W2
-| cpg_ell : ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
- ⬆*[1] V2 ≡ W2 → cpg h (c+𝟘𝟙) G (L.ⓛV1) (#0) W2
-| cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T →
- ⬆*[1] T ≡ U → cpg h c G (L.ⓑ{I}V) (#⫯i) U
+inductive cpg (Rt:relation rtc) (h): rtc → relation4 genv lenv term term ≝
+| cpg_atom : ∀I,G,L. cpg Rt h (𝟘𝟘) G L (⓪{I}) (⓪{I})
+| cpg_ess : ∀G,L,s. cpg Rt h (𝟘𝟙) G L (⋆s) (⋆(next h s))
+| cpg_delta: ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
+ ⬆*[1] V2 ≡ W2 → cpg Rt h c G (L.ⓓV1) (#0) W2
+| cpg_ell : ∀c,G,L,V1,V2,W2. cpg Rt h c G L V1 V2 →
+ ⬆*[1] V2 ≡ W2 → cpg Rt h (c+𝟘𝟙) G (L.ⓛV1) (#0) W2
+| cpg_lref : ∀c,I,G,L,V,T,U,i. cpg Rt h c G L (#i) T →
+ ⬆*[1] T ≡ U → cpg Rt h c G (L.ⓑ{I}V) (#⫯i) U
| cpg_bind : ∀cV,cT,p,I,G,L,V1,V2,T1,T2.
- cpg h cV G L V1 V2 → cpg h cT G (L.ⓑ{I}V1) T1 T2 →
- cpg h ((↓cV)∨cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
-| cpg_flat : ∀cV,cT,I,G,L,V1,V2,T1,T2.
- cpg h cV G L V1 V2 → cpg h cT G L T1 T2 →
- cpg h ((↓cV)∨cT) G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
-| cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg h c G (L.ⓓV) T1 T →
- ⬆*[1] T2 ≡ T → cpg h (c+𝟙𝟘) G L (+ⓓV.T1) T2
-| cpg_eps : ∀c,G,L,V,T1,T2. cpg h c G L T1 T2 → cpg h (c+𝟙𝟘) G L (ⓝV.T1) T2
-| cpg_ee : ∀c,G,L,V1,V2,T. cpg h c G L V1 V2 → cpg h (c+𝟘𝟙) G L (ⓝV1.T) V2
+ cpg Rt h cV G L V1 V2 → cpg Rt h cT G (L.ⓑ{I}V1) T1 T2 →
+ cpg Rt h ((↓cV)∨cT) G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
+| cpg_appl : ∀cV,cT,G,L,V1,V2,T1,T2.
+ cpg Rt h cV G L V1 V2 → cpg Rt h cT G L T1 T2 →
+ cpg Rt h ((↓cV)∨cT) G L (ⓐV1.T1) (ⓐV2.T2)
+| cpg_cast : ∀cU,cT,G,L,U1,U2,T1,T2. Rt cU cT →
+ cpg Rt h cU G L U1 U2 → cpg Rt h cT G L T1 T2 →
+ cpg Rt h (cU∨cT) G L (ⓝU1.T1) (ⓝU2.T2)
+| cpg_zeta : ∀c,G,L,V,T1,T,T2. cpg Rt h c G (L.ⓓV) T1 T →
+ ⬆*[1] T2 ≡ T → cpg Rt h (c+𝟙𝟘) G L (+ⓓV.T1) T2
+| cpg_eps : ∀c,G,L,V,T1,T2. cpg Rt h c G L T1 T2 → cpg Rt h (c+𝟙𝟘) G L (ⓝV.T1) T2
+| cpg_ee : ∀c,G,L,V1,V2,T. cpg Rt h c G L V1 V2 → cpg Rt h (c+𝟘𝟙) G L (ⓝV1.T) V2
| cpg_beta : ∀cV,cW,cT,p,G,L,V1,V2,W1,W2,T1,T2.
- cpg h cV G L V1 V2 → cpg h cW G L W1 W2 → cpg h cT G (L.ⓛW1) T1 T2 →
- cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
+ cpg Rt h cV G L V1 V2 → cpg Rt h cW G L W1 W2 → cpg Rt h cT G (L.ⓛW1) T1 T2 →
+ cpg Rt h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓛ{p}W1.T1) (ⓓ{p}ⓝW2.V2.T2)
| cpg_theta: ∀cV,cW,cT,p,G,L,V1,V,V2,W1,W2,T1,T2.
- cpg h cV G L V1 V → ⬆*[1] V ≡ V2 → cpg h cW G L W1 W2 →
- cpg h cT G (L.ⓓW1) T1 T2 →
- cpg h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
+ cpg Rt h cV G L V1 V → ⬆*[1] V ≡ V2 → cpg Rt h cW G L W1 W2 →
+ cpg Rt h cT G (L.ⓓW1) T1 T2 →
+ cpg Rt h (((↓cV)∨(↓cW)∨cT)+𝟙𝟘) G L (ⓐV1.ⓓ{p}W1.T1) (ⓓ{p}W2.ⓐV2.T2)
.
interpretation
"counted context-sensitive parallel rt-transition (term)"
- 'PRedTy c h G L T1 T2 = (cpg h c G L T1 T2).
+ 'PRedTy Rt c h G L T1 T2 = (cpg Rt h c G L T1 T2).
(* Basic properties *********************************************************)
-(* Note: this is "∀h,g,L. reflexive … (cpg h (𝟘𝟘) L)" *)
-lemma cpg_refl: ∀h,G,T,L. ⦃G, L⦄ ⊢ T ⬈[𝟘𝟘, h] T.
-#h #G #T elim T -T // * /2 width=1 by cpg_bind, cpg_flat/
-qed.
-
-lemma cpg_pair_sn: ∀c,h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[c, h] V2 →
- ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈[↓c, h] ②{I}V2.T.
-#c #h * /2 width=1 by cpg_bind, cpg_flat/
+(* Note: this is "∀Rt. reflexive … Rt → ∀h,g,L. reflexive … (cpg Rt h (𝟘𝟘) L)" *)
+lemma cpg_refl: ∀Rt. reflexive … Rt → ∀h,G,T,L. ⦃G, L⦄ ⊢ T ⬈[Rt, 𝟘𝟘, h] T.
+#Rt #HRt #h #G #T elim T -T // * /2 width=1 by cpg_bind/
+* /2 width=1 by cpg_appl, cpg_cast/
qed.
(* Basic inversion lemmas ***************************************************)
-fact cpg_inv_atom1_aux: ∀c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2 → ∀J. T1 = ⓪{J} →
+fact cpg_inv_atom1_aux: ∀Rt,c,h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈[Rt, c, h] T2 → ∀J. T1 = ⓪{J} →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
| ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
- | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
- | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & J = LRef 0 & c = cV+𝟘𝟙
- | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 &
+ | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 &
L = K.ⓑ{I}V & J = LRef (⫯i).
-#c #h #G #L #T1 #T2 * -c -G -L -T1 -T2
+#Rt #c #h #G #L #T1 #T2 * -c -G -L -T1 -T2
[ #I #G #L #J #H destruct /3 width=1 by or5_intro0, conj/
| #G #L #s #J #H destruct /3 width=3 by or5_intro1, ex3_intro/
| #c #G #L #V1 #V2 #W2 #HV12 #VW2 #J #H destruct /3 width=8 by or5_intro2, ex5_4_intro/
| #c #G #L #V1 #V2 #W2 #HV12 #VW2 #J #H destruct /3 width=8 by or5_intro3, ex5_4_intro/
| #c #I #G #L #V #T #U #i #HT #HTU #J #H destruct /3 width=9 by or5_intro4, ex4_5_intro/
| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
-| #cV #cT #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #J #H destruct
+| #cU #cT #G #L #U1 #U2 #T1 #T2 #_ #_ #_ #J #H destruct
| #c #G #L #V #T1 #T #T2 #_ #_ #J #H destruct
| #c #G #L #V #T1 #T2 #_ #J #H destruct
| #c #G #L #V1 #V2 #T #_ #J #H destruct
]
qed-.
-lemma cpg_inv_atom1: ∀c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[c, h] T2 →
+lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[Rt, c, h] T2 →
∨∨ T2 = ⓪{J} ∧ c = 𝟘𝟘
| ∃∃s. J = Sort s & T2 = ⋆(next h s) & c = 𝟘𝟙
- | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & J = LRef 0 & c = cV
- | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & J = LRef 0 & c = cV+𝟘𝟙
- | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 &
+ | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 &
L = K.ⓑ{I}V & J = LRef (⫯i).
/2 width=3 by cpg_inv_atom1_aux/ qed-.
-lemma cpg_inv_sort1: ∀c,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[c, h] T2 →
+lemma cpg_inv_sort1: ∀Rt,c,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[Rt, c, h] T2 →
(T2 = ⋆s ∧ c = 𝟘𝟘) ∨ (T2 = ⋆(next h s) ∧ c = 𝟘𝟙).
-#c #h #G #L #T2 #s #H
+#Rt #c #h #G #L #T2 #s #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
[ #s0 #H destruct /3 width=1 by or_intror, conj/
|2,3: #cV #K #V1 #V2 #_ #_ #_ #H destruct
]
qed-.
-lemma cpg_inv_zero1: ∀c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈[c, h] T2 →
+lemma cpg_inv_zero1: ∀Rt,c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈[Rt, c, h] T2 →
∨∨ (T2 = #0 ∧ c = 𝟘𝟘)
- | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓓV1 & c = cV
- | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[cV, h] V2 & ⬆*[1] V2 ≡ T2 &
+ | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 &
L = K.ⓛV1 & c = cV+𝟘𝟙.
-#c #h #G #L #T2 #H
+#Rt #c #h #G #L #T2 #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/
[ #s #H destruct
|2,3: #cV #K #V1 #V2 #HV12 #HVT2 #H1 #_ #H2 destruct /3 width=8 by or3_intro1, or3_intro2, ex4_4_intro/
]
qed-.
-lemma cpg_inv_lref1: ∀c,h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈[c, h] T2 →
+lemma cpg_inv_lref1: ∀Rt,c,h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈[Rt, c, h] T2 →
(T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨
- ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈[c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
-#c #h #G #L #T2 #i #H
+ ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V.
+#Rt #c #h #G #L #T2 #i #H
elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/
[ #s #H destruct
|2,3: #cV #K #V1 #V2 #_ #_ #_ #H destruct
]
qed-.
-lemma cpg_inv_gref1: ∀c,h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ⬈[c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
-#c #h #G #L #T2 #l #H
+lemma cpg_inv_gref1: ∀Rt,c,h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ⬈[Rt, c, h] T2 → T2 = §l ∧ c = 𝟘𝟘.
+#Rt #c #h #G #L #T2 #l #H
elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/
[ #s #H destruct
|2,3: #cV #K #V1 #V2 #_ #_ #_ #H destruct
]
qed-.
-fact cpg_inv_bind1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 →
+fact cpg_inv_bind1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 →
∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → (
- ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[cT, h] T2 &
+ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
U2 = ⓑ{p,J}V2.T2 & c = ((↓cV)∨cT)
) ∨
- ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
+ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T &
p = true & J = Abbr & c = cT+𝟙𝟘.
-#c #h #G #L #U #U2 * -c -G -L -U -U2
+#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
[ #I #G #L #q #J #W #U1 #H destruct
| #G #L #s #q #J #W #U1 #H destruct
| #c #G #L #V1 #V2 #W2 #_ #_ #q #J #W #U1 #H destruct
| #c #G #L #V1 #V2 #W2 #_ #_ #q #J #W #U1 #H destruct
| #c #I #G #L #V #T #U #i #_ #_ #q #J #W #U1 #H destruct
-| #rv #cT #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #q #J #W #U1 #H destruct /3 width=8 by ex4_4_intro, or_introl/
-| #rv #cT #I #G #L #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #q #J #W #U1 #H destruct /3 width=8 by ex4_4_intro, or_introl/
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
+| #cU #cT #G #L #U1 #U2 #T1 #T2 #_ #_ #_ #q #J #W #U1 #H destruct
| #c #G #L #V #T1 #T #T2 #HT1 #HT2 #q #J #W #U1 #H destruct /3 width=5 by ex5_2_intro, or_intror/
| #c #G #L #V #T1 #T2 #_ #q #J #W #U1 #H destruct
| #c #G #L #V1 #V2 #T #_ #q #J #W #U1 #H destruct
-| #rv #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #q #J #W #U1 #H destruct
-| #rv #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #q #J #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #q #J #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #q #J #W #U1 #H destruct
]
qed-.
-lemma cpg_inv_bind1: ∀c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c, h] U2 → (
- ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] U2 → (
+ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U2 = ⓑ{p,I}V2.T2 & c = ((↓cV)∨cT)
) ∨
- ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
+ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T &
p = true & I = Abbr & c = cT+𝟙𝟘.
/2 width=3 by cpg_inv_bind1_aux/ qed-.
-lemma cpg_inv_abbr1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[c, h] U2 → (
- ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt, c, h] U2 → (
+ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U2 = ⓓ{p}V2.T2 & c = ((↓cV)∨cT)
) ∨
- ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[cT, h] T & ⬆*[1] U2 ≡ T &
+ ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T &
p = true & c = cT+𝟙𝟘.
-#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
+#Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
/3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/
qed-.
-lemma cpg_inv_abst1: ∀c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈[c, h] U2 →
- ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_abst1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈[Rt, c, h] U2 →
+ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U2 = ⓛ{p}V2.T2 & c = ((↓cV)∨cT).
-#c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
+#Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H *
[ /3 width=8 by ex4_4_intro/
| #c #T #_ #_ #_ #H destruct
]
qed-.
-fact cpg_inv_flat1_aux: ∀c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[c, h] U2 →
- ∀J,V1,U1. U = ⓕ{J}V1.U1 →
- ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
- U2 = ⓕ{J}V2.T2 & c = ((↓cV)∨cT)
- | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & J = Cast & c = cT+𝟙𝟘
- | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & J = Cast & c = cV+𝟘𝟙
- | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
- J = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
- | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
- J = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
-#c #h #G #L #U #U2 * -c -G -L -U -U2
-[ #I #G #L #J #W #U1 #H destruct
-| #G #L #s #J #W #U1 #H destruct
-| #c #G #L #V1 #V2 #W2 #_ #_ #J #W #U1 #H destruct
-| #c #G #L #V1 #V2 #W2 #_ #_ #J #W #U1 #H destruct
-| #c #I #G #L #V #T #U #i #_ #_ #J #W #U1 #H destruct
-| #rv #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #J #W #U1 #H destruct
-| #rv #cT #I #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #J #W #U1 #H destruct /3 width=8 by or5_intro0, ex4_4_intro/
-| #c #G #L #V #T1 #T #T2 #_ #_ #J #W #U1 #H destruct
-| #c #G #L #V #T1 #T2 #HT12 #J #W #U1 #H destruct /3 width=3 by or5_intro1, ex3_intro/
-| #c #G #L #V1 #V2 #T #HV12 #J #W #U1 #H destruct /3 width=3 by or5_intro2, ex3_intro/
-| #rv #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #J #W #U1 #H destruct /3 width=15 by or5_intro3, ex7_9_intro/
-| #rv #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #J #W #U1 #H destruct /3 width=17 by or5_intro4, ex8_10_intro/
+fact cpg_inv_appl1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 →
+ ∀V1,U1. U = ⓐV1.U1 →
+ ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
+ U2 = ⓐV2.T2 & c = ((↓cV)∨cT)
+ | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
+ U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
+ | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
+ U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
+#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
+[ #I #G #L #W #U1 #H destruct
+| #G #L #s #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #I #G #L #V #T #U #i #_ #_ #W #U1 #H destruct
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #HV12 #HT12 #W #U1 #H destruct /3 width=8 by or3_intro0, ex4_4_intro/
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T #T2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T2 #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #T #_ #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #W #U1 #H destruct /3 width=15 by or3_intro1, ex6_9_intro/
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #W #U1 #H destruct /3 width=17 by or3_intro2, ex7_10_intro/
]
qed-.
-lemma cpg_inv_flat1: ∀c,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[c, h] U2 →
- ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
- U2 = ⓕ{I}V2.T2 & c = ((↓cV)∨cT)
- | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & I = Cast & c = cT+𝟙𝟘
- | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & I = Cast & c = cV+𝟘𝟙
- | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
- I = Appl & U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
- | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
- I = Appl & U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
-/2 width=3 by cpg_inv_flat1_aux/ qed-.
-
-lemma cpg_inv_appl1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ⬈[c, h] U2 →
- ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
+lemma cpg_inv_appl1: ∀Rt,c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐV1.U1 ⬈[Rt, c, h] U2 →
+ ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
U2 = ⓐV2.T2 & c = ((↓cV)∨cT)
- | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[cT, h] T2 &
+ | ∃∃cV,cW,cT,p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U1 = ⓛ{p}W1.T1 & U2 = ⓓ{p}ⓝW2.V2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘
- | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[cT, h] T2 &
+ | ∃∃cV,cW,cT,p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V & ⬆*[1] V ≡ V2 & ⦃G, L⦄ ⊢ W1 ⬈[Rt, cW, h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U1 = ⓓ{p}W1.T1 & U2 = ⓓ{p}W2.ⓐV2.T2 & c = ((↓cV)∨(↓cW)∨cT)+𝟙𝟘.
-#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
-[ /3 width=8 by or3_intro0, ex4_4_intro/
-|2,3: #c #_ #H destruct
-| /3 width=15 by or3_intro1, ex6_9_intro/
-| /3 width=17 by or3_intro2, ex7_10_intro/
-]
-qed-.
+/2 width=3 by cpg_inv_appl1_aux/ qed-.
-lemma cpg_inv_cast1: ∀c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[c, h] U2 →
- ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[cT, h] T2 &
- U2 = ⓝV2.T2 & c = ((↓cV)∨cT)
- | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[cT, h] U2 & c = cT+𝟙𝟘
- | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] U2 & c = cV+𝟘𝟙.
-#c #h #G #L #V1 #U1 #U2 #H elim (cpg_inv_flat1 … H) -H *
-[ /3 width=8 by or3_intro0, ex4_4_intro/
-|2,3: /3 width=3 by or3_intro1, or3_intro2, ex2_intro/
-| #rv #cW #cT #p #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #H destruct
-| #rv #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #H destruct
+fact cpg_inv_cast1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 →
+ ∀V1,U1. U = ⓝV1.U1 →
+ ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
+ Rt cV cT & U2 = ⓝV2.T2 & c = (cV∨cT)
+ | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] U2 & c = cT+𝟙𝟘
+ | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] U2 & c = cV+𝟘𝟙.
+#Rt #c #h #G #L #U #U2 * -c -G -L -U -U2
+[ #I #G #L #W #U1 #H destruct
+| #G #L #s #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V1 #V2 #W2 #_ #_ #W #U1 #H destruct
+| #c #I #G #L #V #T #U #i #_ #_ #W #U1 #H destruct
+| #cV #cT #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
+| #cV #cT #G #L #V1 #V2 #T1 #T2 #HRt #HV12 #HT12 #W #U1 #H destruct /3 width=9 by or3_intro0, ex5_4_intro/
+| #c #G #L #V #T1 #T #T2 #_ #_ #W #U1 #H destruct
+| #c #G #L #V #T1 #T2 #HT12 #W #U1 #H destruct /3 width=3 by or3_intro1, ex2_intro/
+| #c #G #L #V1 #V2 #T #HV12 #W #U1 #H destruct /3 width=3 by or3_intro2, ex2_intro/
+| #cV #cW #cT #p #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #W #U1 #H destruct
+| #cV #cW #cT #p #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #W #U1 #H destruct
]
qed-.
+lemma cpg_inv_cast1: ∀Rt,c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[Rt, c, h] U2 →
+ ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] T2 &
+ Rt cV cT & U2 = ⓝV2.T2 & c = (cV∨cT)
+ | ∃∃cT. ⦃G, L⦄ ⊢ U1 ⬈[Rt, cT, h] U2 & c = cT+𝟙𝟘
+ | ∃∃cV. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] U2 & c = cV+𝟘𝟙.
+/2 width=3 by cpg_inv_cast1_aux/ qed-.
+
(* Basic forward lemmas *****************************************************)
-lemma cpg_fwd_bind1_minus: ∀c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[c, h] T → ∀p.
- ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[c, h] ⓑ{p,I}V2.T2 &
+lemma cpg_fwd_bind1_minus: ∀Rt,c,h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[Rt, c, h] T → ∀p.
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] ⓑ{p,I}V2.T2 &
T = -ⓑ{I}V2.T2.
-#c #h #I #G #L #V1 #T1 #T #H #p elim (cpg_inv_bind1 … H) -H *
+#Rt #c #h #I #G #L #V1 #T1 #T #H #p elim (cpg_inv_bind1 … H) -H *
[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct /3 width=4 by cpg_bind, ex2_2_intro/
| #c #T2 #_ #_ #H destruct
]
(* Advanced properties ******************************************************)
-lemma cpg_delta_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ⬈[c, h] V2 →
- ⬆*[⫯i] V2 ≡ T2 → ⦃G, L⦄ ⊢ #i ⬈[c, h] T2.
-#c #h #G #K #V #V2 #i elim i -i
+lemma cpg_delta_drops: ∀Rt,c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ⬈[Rt, c, h] V2 →
+ ⬆*[⫯i] V2 ≡ T2 → ⦃G, L⦄ ⊢ #i ⬈[Rt, c, h] T2.
+#Rt #c #h #G #K #V #V2 #i elim i -i
[ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_delta/
| #i #IH #L0 #T0 #H0 #HV2 #HVT2
elim (drops_inv_succ … H0) -H0 #I #L #V0 #HLK #H destruct
]
qed.
-lemma cpg_ell_drops: ∀c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ⬈[c, h] V2 →
- ⬆*[⫯i] V2 ≡ T2 → ⦃G, L⦄ ⊢ #i ⬈[c+𝟘𝟙, h] T2.
-#c #h #G #K #V #V2 #i elim i -i
+lemma cpg_ell_drops: ∀Rt,c,h,G,K,V,V2,i,L,T2. ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ⬈[Rt,c, h] V2 →
+ ⬆*[⫯i] V2 ≡ T2 → ⦃G, L⦄ ⊢ #i ⬈[Rt, c+𝟘𝟙, h] T2.
+#Rt #c #h #G #K #V #V2 #i elim i -i
[ #L #T2 #HLK lapply (drops_fwd_isid … HLK ?) // #H destruct /3 width=3 by cpg_ell/
| #i #IH #L0 #T0 #H0 #HV2 #HVT2
elim (drops_inv_succ … H0) -H0 #I #L #V0 #HLK #H destruct
(* Advanced inversion lemmas ************************************************)
-lemma cpg_inv_lref1_drops: ∀c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ⬈[c, h] T2 →
+lemma cpg_inv_lref1_drops: ∀Rt,c,h,G,i,L,T2. ⦃G, L⦄ ⊢ #i ⬈[Rt,c, h] T2 →
∨∨ T2 = #i ∧ c = 𝟘𝟘
- | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+ | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & c = cV
- | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+ | ∃∃cV,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & c = cV + 𝟘𝟙.
-#c #h #G #i elim i -i
+#Rt #c #h #G #i elim i -i
[ #L #T2 #H elim (cpg_inv_zero1 … H) -H * /3 width=1 by or3_intro0, conj/
/4 width=8 by drops_refl, ex4_4_intro, or3_intro2, or3_intro1/
| #i #IH #L #T2 #H elim (cpg_inv_lref1 … H) -H * /3 width=1 by or3_intro0, conj/
]
qed-.
-lemma cpg_inv_atom1_drops: ∀c,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ⬈[c, h] T2 →
+lemma cpg_inv_atom1_drops: ∀Rt,c,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ⬈[Rt, c, h] T2 →
∨∨ T2 = ⓪{I} ∧ c = 𝟘𝟘
| ∃∃s. T2 = ⋆(next h s) & I = Sort s & c = 𝟘𝟙
- | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+ | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV
- | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[cV, h] V2 &
+ | ∃∃cV,i,K,V,V2. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ⬈[Rt, cV, h] V2 &
⬆*[⫯i] V2 ≡ T2 & I = LRef i & c = cV + 𝟘𝟙.
-#c #h * #n #G #L #T2 #H
+#Rt #c #h * #n #G #L #T2 #H
[ elim (cpg_inv_sort1 … H) -H *
/3 width=3 by or4_intro0, or4_intro1, ex3_intro, conj/
| elim (cpg_inv_lref1_drops … H) -H *
(* Properties with generic slicing for local environments *******************)
(* Note: it should use drops_split_trans_pair2 *)
-lemma cpg_lifts: ∀c,h,G. d_liftable2 (cpg h c G).
-#c #h #G #K #T generalize in match c; -c
+lemma cpg_lifts: ∀Rt. reflexive … Rt → ∀c,h,G. d_liftable2 (cpg Rt h c G).
+#Rt #HRt #c #h #G #K #T generalize in match c; -c
@(fqup_wf_ind_eq … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * *
[ #s #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct -IH
lapply (lifts_inv_sort1 … H1) -H1 #H destruct
/2 width=3 by cpg_atom, cpg_ess, lifts_sort, ex2_intro/
| #i1 #HG #HK #HT #c #T2 #H2 #b #f #L #HLK #X1 #H1 destruct
elim (cpg_inv_lref1_drops … H2) -H2 *
- [ #H1 #H2 destruct /2 width=3 by ex2_intro/ ]
+ [ #H1 #H2 destruct /3 width=3 by cpg_refl, ex2_intro/ ]
#cV #K0 #V #V2 #HK0 #HV2 #HVT2 #H destruct
elim (lifts_inv_lref1 … H1) -H1 #i2 #Hf #H destruct
lapply (drops_trans … HLK … HK0 ??) -HLK [3,6: |*: // ] #H
elim (lifts_split_trans … HXU2 f (𝐔❴⫯O❵)) [2: /2 width=1 by after_uni_one_dx/ ]
/3 width=5 by cpg_zeta, ex2_intro/
]
-| #I #V1 #T1 #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct
+| * #V1 #T1 #HG #HK #HT #c #X2 #H2 #b #f #L #HLK #X1 #H1 destruct
elim (lifts_inv_flat1 … H1) -H1 #W1 #U1 #HVW1 #HTU1 #H destruct
- elim (cpg_inv_flat1 … H2) -H2 *
- [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
- elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
- elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
- /3 width=5 by cpg_flat, lifts_flat, ex2_intro/
- | #cT #HT12 #H1 #H2 destruct
- elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
- /3 width=3 by cpg_eps, ex2_intro/
- | #cV #HV12 #H1 #H2 destruct
- elim (IH … HV12 … HLK … HVW1) -IH -HV12 -HLK -HVW1 //
- /3 width=3 by cpg_ee, ex2_intro/
- | #cV #cY #cT #a #V2 #Y1 #Y2 #T0 #T2 #HV12 #HY12 #HT12 #H1 #H2 #H3 #H4 destruct
- elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
- elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
- elim (IH … HY12 … HLK … HYZ1) -HY12 //
- elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
- /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
- | #cV #cY #cT #a #V2 #V20 #Y1 #Y2 #T0 #T2 #HV12 #HV20 #HY12 #HT12 #H1 #H2 #H3 #H4 destruct
- elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
- elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 // #W2 #HVW2 #HW12
- elim (IH … HY12 … HLK … HYZ1) -HY12 //
- elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
- elim (lifts_total W2 (𝐔❴1❵)) #W20 #HW20
- lapply (lifts_trans … HVW2 … HW20 ??) -HVW2 [3: |*: // ] #H
- lapply (lifts_conf … HV20 … H (↑f) ?) -V2 /2 width=3 by after_uni_one_sn/
- /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+ [ elim (cpg_inv_appl1 … H2) -H2 *
+ [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+ elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+ /3 width=5 by cpg_appl, lifts_flat, ex2_intro/
+ | #cV #cY #cT #a #V2 #Y1 #Y2 #T0 #T2 #HV12 #HY12 #HT12 #H1 #H2 #H3 destruct
+ elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+ elim (IH … HY12 … HLK … HYZ1) -HY12 //
+ elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+ /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
+ | #cV #cY #cT #a #V2 #V20 #Y1 #Y2 #T0 #T2 #HV12 #HV20 #HY12 #HT12 #H1 #H2 #H3 destruct
+ elim (lifts_inv_bind1 … HTU1) -HTU1 #Z1 #U0 #HYZ1 #HTU1 #H destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 // #W2 #HVW2 #HW12
+ elim (IH … HY12 … HLK … HYZ1) -HY12 //
+ elim (IH … HT12 … HTU1) -IH -HT12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+ elim (lifts_total W2 (𝐔❴1❵)) #W20 #HW20
+ lapply (lifts_trans … HVW2 … HW20 ??) -HVW2 [3: |*: // ] #H
+ lapply (lifts_conf … HV20 … H (↑f) ?) -V2 /2 width=3 by after_uni_one_sn/
+ /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+ ]
+ | elim (cpg_inv_cast1 … H2) -H2 *
+ [ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
+ elim (IH … HV12 … HLK … HVW1) -HV12 -HVW1 //
+ elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+ /3 width=5 by cpg_cast, lifts_flat, ex2_intro/
+ | #cT #HT12 #H destruct
+ elim (IH … HT12 … HLK … HTU1) -IH -HT12 -HLK -HTU1 //
+ /3 width=3 by cpg_eps, ex2_intro/
+ | #cV #HV12 #H destruct
+ elim (IH … HV12 … HLK … HVW1) -IH -HV12 -HLK -HVW1 //
+ /3 width=3 by cpg_ee, ex2_intro/
+ ]
]
]
qed-.
(* Inversion lemmas with generic slicing for local environments *************)
-lemma cpg_inv_lifts1: ∀c,h,G. d_deliftable2_sn (cpg h c G).
-#c #h #G #L #U generalize in match c; -c
+lemma cpg_inv_lifts1: ∀Rt. reflexive … Rt → ∀c,h,G. d_deliftable2_sn (cpg Rt h c G).
+#Rt #HRt #c #h #G #L #U generalize in match c; -c
@(fqup_wf_ind_eq … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * *
[ #s #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct -IH
lapply (lifts_inv_sort2 … H1) -H1 #H destruct
/2 width=3 by cpg_atom, cpg_ess, lifts_sort, ex2_intro/
| #i2 #HG #HL #HU #c #U2 #H2 #b #f #K #HLK #X1 #H1 destruct
elim (cpg_inv_lref1_drops … H2) -H2 *
- [ #H1 #H2 destruct /2 width=3 by ex2_intro/ ]
+ [ #H1 #H2 destruct /3 width=3 by cpg_refl, ex2_intro/ ]
#cW #L0 #W #W2 #HL0 #HW2 #HWU2 #H destruct
elim (lifts_inv_lref2 … H1) -H1 #i1 #Hf #H destruct
lapply (drops_split_div … HLK (𝐔❴i1❵) ???) -HLK [4,8: * |*: // ] #Y0 #HK0 #HLY0
elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ] #T2 #HTU2 #HT12
elim (lifts_div4_one … HTU2 … HXU2) -U2 /3 width=5 by cpg_zeta, ex2_intro/
]
-| #I #W1 #U1 #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct
+| * #W1 #U1 #HG #HL #HU #c #X2 #H2 #b #f #K #HLK #X1 #H1 destruct
elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #HVW1 #HTU1 #H destruct
- elim (cpg_inv_flat1 … H2) -H2 *
- [ #cW #cU #W2 #U2 #HW12 #HU12 #H1 #H2 destruct
- elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
- elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
- /3 width=5 by cpg_flat, lifts_flat, ex2_intro/
- | #cU #HU12 #H1 #H2 destruct
- elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
- /3 width=3 by cpg_eps, ex2_intro/
- | #cW #HW12 #H1 #H2 destruct
- elim (IH … HW12 … HLK … HVW1) -IH -HW12 -HLK -HVW1 //
- /3 width=3 by cpg_ee, ex2_intro/
- | #cW #cZ #cU #a #W2 #Z1 #Z2 #U0 #U2 #HW12 #HZ12 #HU12 #H1 #H2 #H3 #H4 destruct
- elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
- elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
- elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
- elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
- /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
- | #cW #cZ #cU #a #W2 #W20 #Z1 #Z2 #U0 #U2 #HW12 #HW20 #HZ12 #HU12 #H1 #H2 #H3 #H4 destruct
- elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
- elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 // #V2 #HVW2 #HV12
- elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
- elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
- lapply (lifts_trans … HVW2 … HW20 ??) -W2 [3: |*: // ] #H
- elim (lifts_split_trans … H ? (↑f)) -H [ |*: /2 width=3 by after_uni_one_sn/ ]
- /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+ [ elim (cpg_inv_appl1 … H2) -H2 *
+ [ #cW #cU #W2 #U2 #HW12 #HU12 #H1 #H2 destruct
+ elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
+ elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
+ /3 width=5 by cpg_appl, lifts_flat, ex2_intro/
+ | #cW #cZ #cU #a #W2 #Z1 #Z2 #U0 #U2 #HW12 #HZ12 #HU12 #H1 #H2 #H3 destruct
+ elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
+ elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
+ elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
+ elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+ /4 width=7 by cpg_beta, lifts_bind, lifts_flat, ex2_intro/
+ | #cW #cZ #cU #a #W2 #W20 #Z1 #Z2 #U0 #U2 #HW12 #HW20 #HZ12 #HU12 #H1 #H2 #H3 destruct
+ elim (lifts_inv_bind2 … HTU1) -HTU1 #Y1 #T0 #HYZ1 #HTU1 #H destruct
+ elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 // #V2 #HVW2 #HV12
+ elim (IH … HZ12 … HLK … HYZ1) -HZ12 //
+ elim (IH … HU12 … HTU1) -IH -HU12 -HTU1 [ |*: /3 width=3 by drops_skip/ ]
+ lapply (lifts_trans … HVW2 … HW20 ??) -W2 [3: |*: // ] #H
+ elim (lifts_split_trans … H ? (↑f)) -H [ |*: /2 width=3 by after_uni_one_sn/ ]
+ /4 width=9 by cpg_theta, lifts_bind, lifts_flat, ex2_intro/
+ ]
+ | elim (cpg_inv_cast1 … H2) -H2 *
+ [ #cW #cU #W2 #U2 #HW12 #HU12 #HcWU #H1 #H2 destruct
+ elim (IH … HW12 … HLK … HVW1) -HW12 -HVW1 //
+ elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
+ /3 width=5 by cpg_cast, lifts_flat, ex2_intro/
+ | #cU #HU12 #H destruct
+ elim (IH … HU12 … HLK … HTU1) -IH -HU12 -HLK -HTU1 //
+ /3 width=3 by cpg_eps, ex2_intro/
+ | #cW #HW12 #H destruct
+ elim (IH … HW12 … HLK … HVW1) -IH -HW12 -HLK -HVW1 //
+ /3 width=3 by cpg_ee, ex2_intro/
+ ]
]
]
qed-.
(* Properties with restricted refinement for local environments *************)
-lemma lsubr_cpg_trans: ∀c,h,G. lsub_trans … (cpg h c G) lsubr.
-#c #h #G #L1 #T1 #T2 #H elim H -c -G -L1 -T1 -T2
+lemma lsubr_cpg_trans: ∀Rt,c,h,G. lsub_trans … (cpg Rt h c G) lsubr.
+#Rt #c #h #G #L1 #T1 #T2 #H elim H -c -G -L1 -T1 -T2
[ //
| /2 width=2 by cpg_ess/
| #c #G #L1 #V1 #V2 #W2 #_ #HVW2 #IH #X #H
| #c #I1 #G #L1 #V1 #T1 #U1 #i #_ #HTU1 #IH #X #H
elim (lsubr_fwd_pair2 … H) -H #I2 #L2 #V2 #HL21 #H destruct
/3 width=3 by cpg_lref/
-|6,11: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/
-|7,9,10: /3 width=1 by cpg_flat, cpg_eps, cpg_ee/
-|8,12: /4 width=3 by cpg_zeta, cpg_theta, lsubr_pair/
+|6,12: /4 width=1 by cpg_bind, cpg_beta, lsubr_pair/
+|7,8,10,11: /3 width=1 by cpg_appl, cpg_cast, cpg_eps, cpg_ee/
+|9,13: /4 width=3 by cpg_zeta, cpg_theta, lsubr_pair/
]
qed-.
(* Properties with simple terms *********************************************)
(* Note: the main property of simple terms *)
-lemma cpg_inv_appl1_simple: ∀c,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[c, h] U → 𝐒⦃T1⦄ →
- ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[cV, h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[cT, h] T2 &
+lemma cpg_inv_appl1_simple: ∀Rt,c,h,G,L,V1,T1,U. ⦃G, L⦄ ⊢ ⓐV1.T1 ⬈[Rt, c, h] U → 𝐒⦃T1⦄ →
+ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
U = ⓐV2.T2 & c = ((↓cV)∨cT).
-#c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
+#Rt #c #h #G #L #V1 #T1 #U #H #HT1 elim (cpg_inv_appl1 … H) -H *
[ /2 width=8 by ex4_4_intro/
| #cV #cW #cT #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #H destruct
elim (simple_inv_bind … HT1)
(* Basic_2A1: includes: cpr *)
definition cpm (n) (h): relation4 genv lenv term term ≝
- λG,L,T1,T2. ∃∃c. 𝐑𝐓⦃n, c⦄ & ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2.
+ λG,L,T1,T2. ∃∃c. 𝐑𝐓⦃n, c⦄ & ⦃G, L⦄ ⊢ T1 ⬈[eq_t, c, h] T2.
interpretation
"semi-counted context-sensitive parallel rt-transition (term)"
lemma cpm_bind: ∀n,h,p,I,G,L,V1,V2,T1,T2.
⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 →
⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] ⓑ{p,I}V2.T2.
-#n #h #p #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 *
+#n #h #p #I #G #L #V1 #V2 #T1 #T2 * #cV #HcV #HV12 *
/5 width=5 by cpg_bind, isrt_max_O1, isr_shift, ex2_intro/
qed.
-(* Note: cpr_flat: does not hold in basic_1 *)
-(* Basic_1: includes: pr2_thin_dx *)
-(* Basic_2A1: includes: cpr_flat *)
-lemma cpm_flat: ∀n,h,I,G,L,V1,V2,T1,T2.
+lemma cpm_appl: ∀n,h,G,L,V1,V2,T1,T2.
⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
- ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[n, h] ⓕ{I}V2.T2.
-#n #h #I #G #L #V1 #V2 #T1 #T2 * #riV #rhV #HV12 *
-/5 width=5 by isrt_max_O1, isr_shift, cpg_flat, ex2_intro/
+ ⦃G, L⦄ ⊢ ⓐV1.T1 ➡[n, h] ⓐV2.T2.
+#n #h #G #L #V1 #V2 #T1 #T2 * #cV #HcV #HV12 *
+/5 width=5 by isrt_max_O1, isr_shift, cpg_appl, ex2_intro/
+qed.
+
+lemma cpm_cast: ∀n,h,G,L,U1,U2,T1,T2.
+ ⦃G, L⦄ ⊢ U1 ➡[n, h] U2 → ⦃G, L⦄ ⊢ T1 ➡[n, h] T2 →
+ ⦃G, L⦄ ⊢ ⓝU1.T1 ➡[n, h] ⓝU2.T2.
+#n #h #G #L #U1 #U2 #T1 #T2 * #cU #HcU #HU12 *
+/4 width=6 by cpg_cast, isrt_max_idem1, isrt_mono, ex2_intro/
qed.
(* Basic_2A1: includes: cpr_zeta *)
(* Basic_1: includes by definition: pr0_refl *)
(* Basic_2A1: includes: cpr_atom *)
lemma cpr_refl: ∀h,G,L. reflexive … (cpm 0 h G L).
-/2 width=3 by ex2_intro/ qed.
-
-(* Basic_1: was: pr2_head_1 *)
-lemma cpr_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 →
- ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡[h] ②{I}V2.T.
-#h #I #G #L #V1 #V2 *
-/3 width=3 by cpg_pair_sn, isr_shift, ex2_intro/
-qed.
+/3 width=3 by cpg_refl, ex2_intro/ qed.
(* Basic inversion lemmas ***************************************************)
/3 width=5 by ex3_2_intro, ex2_intro/
qed-.
-lemma cpm_inv_flat1: ∀n,h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[n, h] U2 →
- ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 &
- U2 = ⓕ{I}V2.T2
- | (⦃G, L⦄ ⊢ U1 ➡[n, h] U2 ∧ I = Cast)
- | ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & I = Cast & n = ⫯m
- | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ W1 ➡[h] W2 &
- ⦃G, L.ⓛW1⦄ ⊢ T1 ➡[n, h] T2 &
- U1 = ⓛ{p}W1.T1 &
- U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
- | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V & ⬆*[1] V ≡ V2 &
- ⦃G, L⦄ ⊢ W1 ➡[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[n, h] T2 &
- U1 = ⓓ{p}W1.T1 &
- U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
-#n #h #I #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_flat1 … H) -H *
-[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
- elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
- elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
- /4 width=5 by or5_intro0, ex3_2_intro, ex2_intro/
-| #cU #U12 #H1 #H2 destruct
- /5 width=3 by isrt_inv_plus_O_dx, or5_intro1, conj, ex2_intro/
-| #cU #H12 #H1 #H2 destruct
- elim (isrt_inv_plus_SO_dx … Hc) -Hc // #m #Hc #H destruct
- /4 width=3 by or5_intro2, ex3_intro, ex2_intro/
-| #cV #cW #cT #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct
- lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
- elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
- elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
- elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
- elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
- /4 width=11 by or5_intro3, ex6_6_intro, ex2_intro/
-| #cV #cW #cT #p #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HW12 #HT12 #H1 #H2 #H3 #H4 destruct
- lapply (isrt_inv_plus_O_dx … Hc ?) -Hc // #Hc
- elim (isrt_inv_max … Hc) -Hc #n0 #nT #Hc #HcT #H destruct
- elim (isrt_inv_max … Hc) -Hc #nV #nW #HcV #HcW #H destruct
- elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
- elim (isrt_inv_shift … HcW) -HcW #HcW #H destruct
- /4 width=13 by or5_intro4, ex7_7_intro, ex2_intro/
-]
-qed-.
-
(* Basic_1: includes: pr0_gen_appl pr2_gen_appl *)
(* Basic_2A1: includes: cpr_inv_appl1 *)
lemma cpm_inv_appl1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ➡[n, h] U2 →
qed-.
lemma cpm_inv_cast1: ∀n,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ➡[n, h] U2 →
- ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n,h] T2 &
+ ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 &
U2 = ⓝV2.T2
| ⦃G, L⦄ ⊢ U1 ➡[n, h] U2
| ∃∃m. ⦃G, L⦄ ⊢ V1 ➡[m, h] U2 & n = ⫯m.
#n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
-[ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
+[ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct
- elim (isrt_inv_shift … HcV) -HcV #HcV #H destruct
+ lapply (isrt_eq_t_trans … HcV HcVT) -HcVT #H
+ lapply (isrt_inj … H HcT) -H #H destruct <idempotent_max
/4 width=5 by or3_intro0, ex3_2_intro, ex2_intro/
| #cU #U12 #H destruct
/4 width=3 by isrt_inv_plus_O_dx, or3_intro1, ex2_intro/
(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR TERMS ************************)
+(* Basic properties *********************************************************)
+
+(* Note: cpr_flat: does not hold in basic_1 *)
+(* Basic_1: includes: pr2_thin_dx *)
+lemma cpr_flat: ∀h,I,G,L,V1,V2,T1,T2.
+ ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ⦃G, L⦄ ⊢ T1 ➡[h] T2 →
+ ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ➡[h] ⓕ{I}V2.T2.
+#h * /2 width=1 by cpm_cast, cpm_appl/
+qed.
+
+(* Basic_1: was: pr2_head_1 *)
+lemma cpr_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 →
+ ∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ➡[h] ②{I}V2.T.
+#h * /2 width=1 by cpm_bind, cpr_flat/
+qed.
+
(* Basic inversion properties ***********************************************)
lemma cpr_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h] T2 →
#h #G #L #T2 #l #H elim (cpm_inv_gref1 … H) -H //
qed-.
+(* Basic_1: includes: pr0_gen_cast pr2_gen_cast *)
+lemma cpr_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡[h] U2 → (
+ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 &
+ U2 = ⓝV2.T2
+ ) ∨ ⦃G, L⦄ ⊢ U1 ➡[h] U2.
+#h #G #L #V1 #U1 #U2 #H elim (cpm_inv_cast1 … H) -H
+/2 width=1 by or_introl, or_intror/ * #n #_ #H destruct
+qed-.
+
lemma cpr_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ➡[h] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 &
U2 = ⓕ{I}V2.T2
⦃G, L⦄ ⊢ W1 ➡[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ➡[h] T2 &
U1 = ⓓ{p}W1.T1 &
U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
-#h #I #G #L #V1 #U1 #U2 #H elim (cpm_inv_flat1 … H) -H *
-/3 width=13 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex7_7_intro, ex6_6_intro, ex3_2_intro, conj/
-#n #_ #_ #H destruct
-qed-.
-
-(* Basic_1: includes: pr0_gen_cast pr2_gen_cast *)
-lemma cpr_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡[h] U2 → (
- ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 &
- U2 = ⓝV2.T2
- ) ∨ ⦃G, L⦄ ⊢ U1 ➡[h] U2.
-#h #G #L #V1 #U1 #U2 #H elim (cpm_inv_cast1 … H) -H
-/2 width=1 by or_introl, or_intror/ * #n #_ #H destruct
+#h * #G #L #V1 #U1 #U2 #H
+[ elim (cpm_inv_appl1 … H) -H *
+ /3 width=13 by or4_intro0, or4_intro2, or4_intro3, ex7_7_intro, ex6_6_intro, ex3_2_intro/
+| elim (cpr_inv_cast1 … H) -H [ * ]
+ /3 width=5 by or4_intro0, or4_intro1, ex3_2_intro, conj/
+]
qed-.
(* Basic_1: removed theorems 12:
(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************)
definition cpx (h): relation4 genv lenv term term ≝
- λG,L,T1,T2. ∃c. ⦃G, L⦄ ⊢ T1 ⬈[c, h] T2.
+ λG,L,T1,T2. ∃c. ⦃G, L⦄ ⊢ T1 ⬈[eq_f, c, h] T2.
interpretation
"uncounted context-sensitive parallel rt-transition (term)"
lemma cpx_flat: ∀h,I,G,L,V1,V2,T1,T2.
⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 →
⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ⬈[h] ⓕ{I}V2.T2.
-#h #I #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
-/3 width=2 by cpg_flat, ex_intro/
+#h * #G #L #V1 #V2 #T1 #T2 * #cV #HV12 *
+/3 width=5 by cpg_appl, cpg_cast, ex_intro/
qed.
lemma cpx_zeta: ∀h,G,L,V,T1,T,T2. ⦃G, L.ⓓV⦄ ⊢ T1 ⬈[h] T →
(* Basic_2A1: includes: cpx_atom *)
lemma cpx_refl: ∀h,G,L. reflexive … (cpx h G L).
-/2 width=2 by ex_intro/ qed.
+/3 width=2 by cpg_refl, ex_intro/ qed.
+
+(* Advanced properties ******************************************************)
lemma cpx_pair_sn: ∀h,I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
∀T. ⦃G, L⦄ ⊢ ②{I}V1.T ⬈[h] ②{I}V2.T.
-#h #I #G #L #V1 #V2 *
-/3 width=2 by cpg_pair_sn, ex_intro/
+#h * /2 width=2 by cpx_flat, cpx_bind/
qed.
(* Basic inversion lemmas ***************************************************)
/3 width=5 by ex3_2_intro, ex_intro/
qed-.
-lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[h] U2 →
- ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
- U2 = ⓕ{I}V2.T2
- | (⦃G, L⦄ ⊢ U1 ⬈[h] U2 ∧ I = Cast)
- | (⦃G, L⦄ ⊢ V1 ⬈[h] U2 ∧ I = Cast)
- | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[h] W2 &
- ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 &
- U1 = ⓛ{p}W1.T1 &
- U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
- | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V & ⬆*[1] V ≡ V2 &
- ⦃G, L⦄ ⊢ W1 ⬈[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 &
- U1 = ⓓ{p}W1.T1 &
- U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
-#h #I #G #L #V1 #U1 #U2 * #c #H elim (cpg_inv_flat1 … H) -H *
-/4 width=14 by or5_intro0, or5_intro1, or5_intro2, or5_intro3, or5_intro4, ex7_7_intro, ex6_6_intro, ex3_2_intro, ex_intro, conj/
-qed-.
-
lemma cpx_inv_appl1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓐ V1.U1 ⬈[h] U2 →
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
U2 = ⓐV2.T2
/4 width=5 by or3_intro0, or3_intro1, or3_intro2, ex3_2_intro, ex_intro/
qed-.
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpx_inv_flat1: ∀h,I,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓕ{I}V1.U1 ⬈[h] U2 →
+ ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ U1 ⬈[h] T2 &
+ U2 = ⓕ{I}V2.T2
+ | (⦃G, L⦄ ⊢ U1 ⬈[h] U2 ∧ I = Cast)
+ | (⦃G, L⦄ ⊢ V1 ⬈[h] U2 ∧ I = Cast)
+ | ∃∃p,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L⦄ ⊢ W1 ⬈[h] W2 &
+ ⦃G, L.ⓛW1⦄ ⊢ T1 ⬈[h] T2 &
+ U1 = ⓛ{p}W1.T1 &
+ U2 = ⓓ{p}ⓝW2.V2.T2 & I = Appl
+ | ∃∃p,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V & ⬆*[1] V ≡ V2 &
+ ⦃G, L⦄ ⊢ W1 ⬈[h] W2 & ⦃G, L.ⓓW1⦄ ⊢ T1 ⬈[h] T2 &
+ U1 = ⓓ{p}W1.T1 &
+ U2 = ⓓ{p}W2.ⓐV2.T2 & I = Appl.
+#h * #G #L #V1 #U1 #U2 #H
+[ elim (cpx_inv_appl1 … H) -H *
+ /3 width=14 by or5_intro0, or5_intro3, or5_intro4, ex7_7_intro, ex6_6_intro, ex3_2_intro/
+| elim (cpx_inv_cast1 … H) -H [ * ]
+ /3 width=14 by or5_intro0, or5_intro1, or5_intro2, ex3_2_intro, conj/
+]
+qed-.
+
(* Basic forward lemmas *****************************************************)
lemma cpx_fwd_bind1_minus: ∀h,I,G,L,V1,T1,T. ⦃G, L⦄ ⊢ -ⓑ{I}V1.T1 ⬈[h] T → ∀p.
interpretation "one t-step (rtc)"
'ZeroOne = (mk_rtc O O O (S O)).
+
+definition eq_f: relation rtc ≝ λc1,c2. ⊤.
+
+inductive eq_t: relation rtc ≝
+| eq_t_intro: ∀ri1,ri2,rs1,rs2,ti,ts.
+ eq_t (〈ri1, rs1, ti, ts〉) (〈ri2, rs2, ti, ts〉)
+.
+
+(* Basic properties *********************************************************)
+
+lemma eq_t_refl: reflexive … eq_t.
+* // qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact eq_t_inv_dx_aux: ∀x,y. eq_t x y →
+ ∀ri1,rs1,ti,ts. x = 〈ri1,rs1,ti,ts〉 →
+ ∃∃ri2,rs2. y = 〈ri2,rs2,ti,ts〉.
+#x #y * -x -y
+#ri1 #ri #rs1 #rs #ti1 #ts1 #ri2 #rs2 #ti2 #ts2 #H destruct -ri2 -rs2
+/2 width=3 by ex1_2_intro/
+qed-.
+
+lemma eq_t_inv_dx: ∀ri1,rs1,ti,ts,y. eq_t (〈ri1,rs1,ti,ts〉) y →
+ ∃∃ri2,rs2. y = 〈ri2,rs2,ti,ts〉.
+/2 width=5 by eq_t_inv_dx_aux/ qed-.
lemma isrt_01: 𝐑𝐓⦃1, 𝟘𝟙⦄.
/2 width=3 by ex1_2_intro/ qed.
+lemma isrt_eq_t_trans: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → eq_t c1 c2 → 𝐑𝐓⦃n, c2⦄.
+#n #c1 #c2 * #ri1 #rs1 #H destruct
+#H elim (eq_t_inv_dx … H) -H /2 width=3 by ex1_2_intro/
+qed-.
+
(* Basic inversion properties ***********************************************)
lemma isrt_inv_00: ∀n. 𝐑𝐓⦃n, 𝟘𝟘⦄ → 0 = n.
(* Main inversion properties ************************************************)
-theorem isrt_mono: ∀n1,n2,c. 𝐑𝐓⦃n1, c⦄ → 𝐑𝐓⦃n2, c⦄ → n1 = n2.
+theorem isrt_inj: ∀n1,n2,c. 𝐑𝐓⦃n1, c⦄ → 𝐑𝐓⦃n2, c⦄ → n1 = n2.
#n1 #n2 #c * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
qed-.
+
+theorem isrt_mono: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → 𝐑𝐓⦃n, c2⦄ → eq_t c1 c2.
+#n #c1 #c2 * #ri1 #rs1 #H1 * #ri2 #rs2 #H2 destruct //
+qed-.
#n #c1 #c2 #H1 #H2 >(max_O2 n) /2 width=1 by isrt_max/
qed.
+lemma isrt_max_idem1: ∀n,c1,c2. 𝐑𝐓⦃n, c1⦄ → 𝐑𝐓⦃n, c2⦄ → 𝐑𝐓⦃n, c1∨c2⦄.
+#n #c1 #c2 #H1 #H2 >(idempotent_max n) /2 width=1 by isrt_max/
+qed.
+
(* Inversion properties with test for constrained rt-transition counter *****)
lemma isrt_inv_max: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ →
lemma isrt_inv_max_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 ∨ c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄.
#n #c1 #c2 #H #H2
elim (isrt_inv_max … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_mono … Hn2 H2) -c2 #H destruct //
+lapply (isrt_inj … Hn2 H2) -c2 #H destruct //
qed-.
(* Properties with shift ****************************************************)
lemma isrt_inv_plus_O_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃0, c2⦄ → 𝐑𝐓⦃n, c1⦄.
#n #c1 #c2 #H #H2
elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_mono … Hn2 H2) -c2 #H destruct //
+lapply (isrt_inj … Hn2 H2) -c2 #H destruct //
qed-.
lemma isrt_inv_plus_SO_dx: ∀n,c1,c2. 𝐑𝐓⦃n, c1 + c2⦄ → 𝐑𝐓⦃1, c2⦄ →
∃∃m. 𝐑𝐓⦃m, c1⦄ & n = ⫯m.
#n #c1 #c2 #H #H2
elim (isrt_inv_plus … H) -H #n1 #n2 #Hn1 #Hn2 #H destruct
-lapply (isrt_mono … Hn2 H2) -c2 #H destruct
+lapply (isrt_inj … Hn2 H2) -c2 #H destruct
/2 width=3 by ex2_intro/
qed-.
projects / helm.git / commitdiff