csuba/getl csuba_getl_abst_rev
csuba/getl csuba_getl_abbr_rev
csuba/props csuba_refl
-
-# check #############################################################
-
csubc/arity csubc_arity_conf
csubc/arity csubc_arity_trans
-csubc/clear csubc_clear_conf
csubc/csuba csubc_csuba
csubc/drop1 drop1_csubc_trans
-csubc/drop1 csubc_drop1_conf_rev
-csubc/drop csubc_drop_conf_O
csubc/drop drop_csubc_trans
-csubc/drop csubc_drop_conf_rev
-csubc/fwd csubc_gen_sort_l
-csubc/fwd csubc_gen_head_l
-csubc/fwd csubc_gen_sort_r
-csubc/fwd csubc_gen_head_r
-csubc/getl csubc_getl_conf
-csubc/props csubc_refl
-
-# waiting ####################################################################
-
csubt/clear csubt_clear_conf
csubt/csuba csubt_csuba
csubt/drop csubt_drop_flat
csubv/getl csubv_getl_conf_void
csubv/props csubv_bind_same
csubv/props csubv_refl
+
+# check #############################################################
+
drop1/fwd drop1_gen_pnil
drop1/fwd drop1_gen_pcons
drop1/props drop1_skip_bind
drop1/props drop1_cons_tail
+
+# waiting ####################################################################
+
drop/props drop_ctail
ex0/props aplus_gz_le
ex0/props aplus_gz_ge
∀L,k. NF … (RR L) RS (⋆k).
definition CP2 ≝ λRR:lenv→relation term. λRS:relation term.
- ∀L,K,W,i. ⇩[0,i] L ≡ K. 𝕓{Abst} W → NF … (RR L) RS (#i).
+ ∀L,K,W,i. ⇩[0,i] L ≡ K. ⓛW → NF … (RR L) RS (#i).
definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term.
- ∀L,V,k. RP L (𝕔{Appl}⋆k.V) → RP L V.
+ ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V.
definition CP4 ≝ λRR:lenv→relation term. λRS:relation term.
∀L0,L,T,T0,d,e. NF … (RR L) RS T →
(* *)
(**************************************************************************)
-include "Basic_2/unfold/gr2_gr2.ma".
include "Basic_2/unfold/lifts_lifts.ma".
include "Basic_2/unfold/ldrops_ldrops.ma".
-include "Basic_2/computation/lsubc.ma".
-
-(* NOTE: The constant (0) can not be generalized *)
-axiom lsubc_ldrop_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2.
-
-axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
- ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
-
-axiom aaa_mono: ∀L,T,A1. L ⊢ T ÷ A1 → ∀A2. L ⊢ T ÷ A2 → A1 = A2.
-
-axiom aaa_lifts: ∀L1,L2,T1,T2,A,des.
- L1 ⊢ T1 ÷ A → ⇩*[des] L2 ≡ L1 → ⇧*[des] T1 ≡ T2 → L2 ⊢ T2 ÷ A.
+include "Basic_2/static/aaa_lifts.ma".
+include "Basic_2/static/aaa_aaa.ma".
+include "Basic_2/computation/lsubc_ldrops.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
- lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
+ lapply (aacr_acr … H1RP H2RP ⓪) #HAtom
@(s2 … HAtom … ◊) // /2 width=2/
| #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
lapply (aacr_acr … H1RP H2RP B) #HB
elim (ldrops_ldrop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1
>(at_mono … Hi1 … Hi0) -i1
elim (ldrops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct
- elim (lsubc_ldrop_trans … HL20 … HL0) -HL0 #X #HLK2 #H
+ elim (lsubc_ldrop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
elim (lsubc_inv_pair2 … H) -H *
[ #K2 #HK20 #H destruct
generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2
| -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
#K2 #V2 #A2 #HKV2A #HKV0A #_ #H1 #H2 destruct
lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b
- lapply (aaa_lifts … HKV1B HK01 HV10) -HKV1B -HK01 -HV10 #HKV0B
+ lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
>(aaa_mono … HKV0A … HKV0B) in HKV2A; -HKV0A -HKV0B #HKV2B
elim (lift_total V2 0 (i0 +1)) #V #HV2
@(s4 … HB … ◊ … HV2 HLK2)
| -IHB
#L3 #V3 #T3 #des3 #HL32 #HT03 #HB
elim (lifts_total des3 W0) #W2 #HW02
- elim (ldrops_lsubc_trans … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts ? L2 ? W2 ? (des @ des3) HLWB ? ?) -HLWB /2 width=3/ #HLW2B
- @(IHA (L2. 𝕓{Abst} W2) … (des + 1 @ des3 + 1)) -IHA
+ elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
+ lapply (aaa_lifts … L2 W2 … (des @ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
+ @(IHA (L2. ⓛW2) … (des + 1 @ des3 + 1)) -IHA
/2 width=3/ /3 width=5/
]
| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
(**************************************************************************)
include "Basic_2/grammar/aarity.ma".
+include "Basic_2/unfold/gr2_gr2.ma".
include "Basic_2/unfold/lifts_lift_vector.ma".
+include "Basic_2/unfold/ldrops_ldrop.ma".
include "Basic_2/computation/acp.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* Note: this is Tait's ii *)
definition S3 ≝ λRP,C:lenv→predicate term.
- ∀L,Vs,V,T,W. C L (ⒶVs. 𝕔{Abbr}V. T) → RP L W → C L (ⒶVs. 𝕔{Appl}V. 𝕔{Abst}W. T).
+ ∀L,Vs,V,T,W. C L (ⒶVs. ⓓV. T) → RP L W → C L (ⒶVs. ⓐV. ⓛW. T).
definition S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i.
C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 →
- ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 → C L (Ⓐ Vs. #i).
+ ⇩[0, i] L ≡ K. ⓓV1 → C L (Ⓐ Vs. #i).
definition S5 ≝ λRP,C:lenv→predicate term.
∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀V,T. C (L. 𝕓{Abbr}V) (ⒶV2s. T) → RP L V → C L (ⒶV1s. 𝕔{Abbr}V. T).
+ ∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T).
definition S6 ≝ λRP,C:lenv→predicate term.
- ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. 𝕔{Cast}W. T).
+ ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓣW. T).
definition S7 ≝ λC:lenv→predicate term. ∀L1,L2,T1,T2,d,e.
C L1 T1 → ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
λT. match A with
[ AAtom ⇒ RP L T
| APair B A ⇒ ∀L0,V0,T0,des. aacr RP B L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 →
- aacr RP A L0 (𝕔{Appl} V0. T0)
+ aacr RP A L0 (ⓐV0. T0)
].
interpretation
@conj /2 width=1/ /2 width=6 by rp_lifts/
qed.
-axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀A. acr RR RS RP (aacr RP A).
-(*
#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
#B #A #IHB #IHA @mk_acr normalize
[ #L #T #H
elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
@(s3 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /4 width=5/
+| #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
+ elim (ldrops_ldrop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
+ >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
+ elim (ldrops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct
+ elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
+ elim (lifts_lift_trans … HVW1 … HW12 … Hdes0) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
+ >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
+ @(s4 … IHA … (V0 :: V0s) … HW12 HL02) /3 width=4/
| #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
@(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/
@(HA … (des + 1)) /2 width=1/
[ @(s7 … IHB … HB … HV120) /2 width=1/
- | @liftsv_applv //
+ | @lifts_applv //
elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
>(liftv_mono … HV12s … HV10s) -V1s //
]
| /3 width=7/
]
qed.
-*)
+
lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L,W,T,A,B. RP L W → (
∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 →
- ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛
+ ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. ⓓV0, T0⦄ [RP] ϵ 〚A〛
) →
- ⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛.
+ ⦃L, ⓛW. T⦄ [RP] ϵ 〚②B. A〛.
#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
lapply (aacr_acr … H1RP H2RP A) #HCA
lapply (aacr_acr … H1RP H2RP B) #HCB
inductive lsubc (RP:lenv→predicate term): relation lenv ≝
| lsubc_atom: lsubc RP (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V)
| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ÷ A →
- lsubc RP L1 L2 → lsubc RP (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+ lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW)
.
interpretation
(* Basic inversion lemmas ***************************************************)
-fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I} W →
- (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#RP #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+]
+qed.
+
+(* Basic_1: was: csubc_gen_sort_r *)
+lemma lsubc_inv_atom1: ∀RP,L2. ⋆ [RP] ⊑ L2 → L2 = ⋆.
+/2 width=4/ qed-.
+
+fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
+ (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
+ K1 [RP] ⊑ K2 &
+ L2 = K2. ⓛW & I = Abbr.
+#RP #L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K1 #V #H destruct /3 width=7/
+]
+qed.
+
+(* Basic_1: was: csubc_gen_head_r *)
+lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V [RP] ⊑ L2 →
+ (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
+ K1 [RP] ⊑ K2 &
+ L2 = K2. ⓛW & I = Abbr.
+/2 width=3/ qed-.
+
+fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L2 = ⋆ → L1 = ⋆.
+#RP #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+]
+qed.
+
+(* Basic_1: was: csubc_gen_sort_l *)
+lemma lsubc_inv_atom2: ∀RP,L1. L1 [RP] ⊑ ⋆ → L1 = ⋆.
+/2 width=4/ qed-.
+
+fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+ (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨
∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
K1 [RP] ⊑ K2 &
- L1 = K1. 𝕓{Abbr} V & I = Abst.
+ L1 = K1. ⓓV & I = Abst.
#RP #L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #H #HV1 #HW2 #I #K2 #W #H destruct /3 width=7/
+| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K2 #W #H destruct /3 width=7/
]
qed.
-lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. 𝕓{I} W →
- (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+(* Basic_1: was: csubc_gen_head_l *)
+lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. ⓑ{I} W →
+ (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨
∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
K1 [RP] ⊑ K2 &
- L1 = K1. 𝕓{Abbr} V & I = Abst.
+ L1 = K1. ⓓV & I = Abst.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
+(* Basic_1: was: csubc_refl *)
lemma lsubc_refl: ∀RP,L. L [RP] ⊑ L.
#RP #L elim L -L // /2 width=1/
qed.
+
+(* Basic_1: removed theorems 2: csubc_clear_conf csubc_getl_conf *)
--- /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 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/static/aaa_lift.ma".
+include "Basic_2/computation/acp_cr.ma".
+include "Basic_2/computation/lsubc.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Basic_1: was: csubc_drop_conf_O *)
+(* Note: the constant (0) can not be generalized *)
+lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2.
+#RP #L1 #L2 #H elim H -L1 -L2
+[ #X #e #H
+ >(ldrop_inv_atom1 … H) -H /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #X #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #H destruct
+ [ elim (IHL12 L2 0 ?) -IHL12 // #X #H <(ldrop_inv_refl … H) -H /3 width=3/
+ | elim (IHL12 … H) -L2 /3 width=3/
+ ]
+| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #X #e #H
+ elim (ldrop_inv_O1 … H) -H * #He #H destruct
+ [ elim (IHL12 L2 0 ?) -IHL12 // #X #H <(ldrop_inv_refl … H) -H /3 width=7/
+ | elim (IHL12 … H) -L2 /3 width=3/
+ ]
+qed-.
+
+(* Basic_1: was: csubc_drop_conf_rev *)
+lemma ldrop_lsubc_trans: ∀RR,RS,RP.
+ acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
+ ∃∃L2. L1 [RP] ⊑ L2 & ⇩[d, e] L2 ≡ K2.
+#RR #RS #RP #Hacp #Hacr #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H
+ >(lsubc_inv_atom1 … H) -H /2 width=3/
+| #L1 #I #V1 #X #H
+ elim (lsubc_inv_pair1 … H) -H *
+ [ #K1 #HLK1 #H destruct /3 width=3/
+ | #K1 #W1 #A #HV1 #HW1 #HLK1 #H1 #H2 destruct /3 width=3/
+ ]
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+ elim (IHLK1 … HK12) -K1 /3 width=5/
+| #L1 #K1 #I #V1 #V2 #d #e #HLK1 #HV21 #IHLK1 #X #H
+ elim (lsubc_inv_pair1 … H) -H *
+ [ #K2 #HK12 #H destruct
+ elim (IHLK1 … HK12) -K1 /3 width=5/
+ | #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct
+ elim (IHLK1 … HK12) #K #HL1K #HK2
+ lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
+ lapply (s7 … HA … HV2 HLK1 HV21) -HV2
+ elim (lift_total W2 d e) /4 width=9/
+ ]
+]
+qed-.
--- /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 *)
+(* *)
+(**************************************************************************)
+
+include "Basic_2/computation/lsubc_ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+
+(* Properties concerning generic local environment slicing ******************)
+
+(* Basic_1: was: csubc_drop1_conf_rev *)
+lemma ldrops_lsubc_trans: ∀RR,RS,RP.
+ acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
+ ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
+#RR #RS #RP #Hacp #Hacr #L1 #K1 #des #H elim H -L1 -K1 -des
+[ /2 width=3/
+| #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12
+ elim (ldrop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2
+ elim (IHL … HLK) -IHL -HLK /3 width=5/
+]
+qed-.
| GRef _ ⇒ U
]
| TPair I V T ⇒ match I with
- [ Bind I ⇒ 𝕓{I} (flift d e V). (flift (d+1) e T)
- | Flat I ⇒ 𝕗{I} (flift d e V). (flift d e T)
+ [ Bind2 I ⇒ ⓑ{I} (flift d e V). (flift (d+1) e T)
+ | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T)
]
].
interpretation "atom (ext. local environment)"
'Star = XAtom.
-interpretation "environment binding construction (quad)"
- 'DBind L I u K V = (XQuad L I u K V).
+interpretation "environment construction (quad)"
+ 'DxItem4 L I u K V = (XQuad L I u K V).
(* machine stack *)
definition stack: Type[0] ≝ list2 xenv term.
rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0))
(mk_rtm G u F S V)
| rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| →
- rtm_step (mk_rtm (G. 𝕓{I} V) u E S (§p))
+ rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p))
(mk_rtm G u E S (§p))
| rtm_gdelta: ∀G,V,u,E,S,p. p = |G| →
- rtm_step (mk_rtm (G. 𝕓{Abbr} V) u E S (§p))
+ rtm_step (mk_rtm (G. ⓓV) u E S (§p))
(mk_rtm G u E S V)
| rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
- rtm_step (mk_rtm (G. 𝕓{Abst} V) u E S (§p))
+ rtm_step (mk_rtm (G. ⓛV) u E S (§p))
(mk_rtm G u E S V)
| rtm_tau : ∀G,u,E,S,W,T.
- rtm_step (mk_rtm G u E S (𝕔{Cast} W. T))
+ rtm_step (mk_rtm G u E S (ⓣW. T))
(mk_rtm G u E S T)
| rtm_appl : ∀G,u,E,S,V,T.
- rtm_step (mk_rtm G u E S (𝕔{Appl} V. T))
+ rtm_step (mk_rtm G u E S (ⓐV. T))
(mk_rtm G u E ({E, V} :: S) T)
| rtm_beta : ∀G,u,E,F,V,S,W,T.
- rtm_step (mk_rtm G u E ({F, V} :: S) (𝕔{Abst} W. T))
+ rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T))
(mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
| rtm_push : ∀G,u,E,W,T.
- rtm_step (mk_rtm G u E ⟠ (𝕔{Abst} W. T))
+ rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
(mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T)
| rtm_theta : ∀G,u,E,S,V,T.
- rtm_step (mk_rtm G u E S (𝕔{Abbr} V. T))
+ rtm_step (mk_rtm G u E S (ⓓV. T))
(mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
.
| GRef _ ⇒ U
]
| TPair I V T ⇒ match I with
- [ Bind I ⇒ 𝕓{I} (fsubst W d V). (fsubst W (d+1) T)
- | Flat I ⇒ 𝕗{I} (fsubst W d V). (fsubst W d T)
+ [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T)
+ | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T)
]
].
(* Main properties **********************************************************)
theorem fsubst_delift: ∀K,V,T,L,d.
- ⇩[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ [d ← V] T.
+ ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T.
#K #V #T elim T -T
[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
elim (lt_or_eq_or_gt i d) #Hid
(* Main inversion properties ************************************************)
-theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. 𝕓{Abbr} V →
+theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
#K #V #T1 elim T1 -T1
[ * #i #L #T2 #d #HLK #H
(* *)
(**************************************************************************)
+(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
+ * Confluence of context-sensitive parallel reduction closed: 2011 September 21
+ * Confluence of context-free parallel reduction closed: 2011 September 6
+ * Specification started: 2011 April 17
+ * - Patience on me to gain peace and perfection! -
+ * [ suggested invocation to start formal specifications with ]
+ *)
+
include "Ground_2/star.ma".
include "Basic_2/notation.ma".
| APair: aarity → aarity → aarity (* binary aarity construction *)
.
-interpretation "aarity construction (atomic)" 'SItem = AAtom.
+interpretation "aarity construction (atomic)"
+ 'Item0 = AAtom.
-interpretation "aarity construction (binary)" 'SItem A1 A2 = (APair A1 A2).
+interpretation "aarity construction (binary)"
+ 'SnItem2 A1 A2 = (APair A1 A2).
(* Basic inversion lemmas ***************************************************)
-lemma discr_apair_xy_x: ∀A,B. 𝕔 B. A = B → False.
+lemma discr_apair_xy_x: ∀A,B. ②B. A = B → False.
#A #B elim B -B
[ #H destruct
| #Y #X #IHY #_ #H destruct
]
qed-.
-lemma discr_tpair_xy_y: ∀B,A. 𝕔 B. A = A → False.
+lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → False.
#B #A elim A -A
[ #H destruct
| #Y #X #_ #IHX #H destruct
let rec shift L T on L ≝ match L with
[ LAtom ⇒ T
-| LPair L I V ⇒ shift L (𝕓{I} V. T)
+| LPair L I V ⇒ shift L (ⓑ{I} V. T)
].
interpretation "shift (closure)" 'Append L T = (shift L T).
∀L,T. R L T.
(* Basic_1: was: flt_shift *)
-lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T].
+lemma cw_shift: ∀K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ②{I} V. T].
normalize //
qed.
interpretation "sort (global environment)"
'Star = (nil2 bind2 term).
+interpretation "environment construction (binary)"
+ 'DxItem2 L I T = (cons2 bind2 term I T L).
+
interpretation "environment binding construction (binary)"
- 'DBind L I T = (cons2 bind2 term I T L).
+ 'DxBind2 L I T = (cons2 bind2 term I T L).
+
+interpretation "abbreviation (global environment)"
+ 'DxAbbr L T = (cons2 bind2 term Abbr T L).
+
+interpretation "abstraction (global environment)"
+ 'DxAbst L T = (cons2 bind2 term Abst T L).
(* Basic properties *********************************************************)
(* *)
(**************************************************************************)
-(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
- * Confluence of context-sensitive parallel reduction closed: 2011 September 21
- * Confluence of context-free parallel reduction closed: 2011 September 6
- * Specification started: 2011 April 17
- * - Patience on me to gain peace and perfection! -
- * [ suggested invocation to start formal specifications with ]
- *)
-
include "Ground_2/arith.ma".
include "Basic_2/notation.ma".
(* binary items *)
inductive item2: Type[0] ≝
- | Bind: bind2 → item2 (* binding item *)
- | Flat: flat2 → item2 (* non-binding item *)
+ | Bind2: bind2 → item2 (* binding item *)
+ | Flat2: flat2 → item2 (* non-binding item *)
.
-coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2.
+coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind2 on _I:bind2 to item2.
-coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2.
+coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat2 on _I:flat2 to item2.
(* Basic properties *********************************************************)
| LPair: lenv → bind2 → term → lenv (* binary binding construction *)
.
-interpretation "sort (local environment)" 'Star = LAtom.
+interpretation "sort (local environment)"
+ 'Star = LAtom.
-interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T).
+interpretation "environment construction (binary)"
+ 'DxItem2 L I T = (LPair L I T).
+
+interpretation "environment binding construction (binary)"
+ 'DxBind2 L I T = (LPair L I T).
+
+interpretation "abbreviation (local environment)"
+ 'DxAbbr L T = (LPair L Abbr T).
+
+interpretation "abstraction (local environment)"
+ 'DxAbst L T = (LPair L Abst T).
| lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
| lsubs_OO: ∀L1,L2. lsubs 0 0 L1 L2
| lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
- lsubs 0 (e + 1) (L1. 𝕓{Abbr} V) (L2.𝕓{Abbr} V)
+ lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
| lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
- lsubs 0 (e + 1) (L1. 𝕓{Abst} V1) (L2.𝕓{I} V2)
+ lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2)
| lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- lsubs d e L1 L2 → lsubs (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
+ lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
.
interpretation
qed.
lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
- L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
+ L1. ⓑ{I} V [0, e + 1] ≼ L2.ⓑ{I} V.
#L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
qed.
qed.
lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≼ L2. 𝕓{I2} V2.
+ ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 [d, e] ≼ L2. ⓑ{I2} V2.
#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
qed.
| TPair: item2 → term → term → term (* binary item construction *)
.
-interpretation "sort (term)" 'Star k = (TAtom (Sort k)).
+interpretation "term construction (atomic)"
+ 'Item0 I = (TAtom I).
-interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)).
+interpretation "term construction (binary)"
+ 'SnItem2 I T1 T2 = (TPair I T1 T2).
-interpretation "global reference (term)" 'GRef p = (TAtom (GRef p)).
+interpretation "term binding construction (binary)"
+ 'SnBind2 I T1 T2 = (TPair (Bind2 I) T1 T2).
-interpretation "term construction (atomic)" 'SItem I = (TAtom I).
+interpretation "term flat construction (binary)"
+ 'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
-interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
+interpretation "sort (term)"
+ 'Star k = (TAtom (Sort k)).
-interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2).
+interpretation "local reference (term)"
+ 'LRef i = (TAtom (LRef i)).
-interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2).
+interpretation "global reference (term)"
+ 'GRef p = (TAtom (GRef p)).
+
+interpretation "abbreviation (term)"
+ 'SnAbbr T1 T2 = (TPair (Bind2 Abbr) T1 T2).
+
+interpretation "abstraction (term)"
+ 'SnAbst T1 T2 = (TPair (Bind2 Abst) T1 T2).
+
+interpretation "application (term)"
+ 'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2).
+
+interpretation "native type annotation (term)"
+ 'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
(* Basic inversion lemmas ***************************************************)
-lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
+lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → False.
#I #T #V elim V -V
[ #J #H destruct
| #J #W #U #IHW #_ #H destruct
qed-.
(* Basic_1: was: thead_x_y_y *)
-lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False.
+lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → False.
#I #V #T elim T -T
[ #J #H destruct
| #J #W #U #_ #IHU #H destruct
(* SIMPLE (NEUTRAL) TERMS ***************************************************)
inductive simple: predicate term ≝
- | simple_atom: ∀I. simple (𝕒{I})
- | simple_flat: ∀I,V,T. simple (𝕗{I} V. T)
+ | simple_atom: ∀I. simple (⓪{I})
+ | simple_flat: ∀I,V,T. simple (ⓕ{I} V. T)
.
interpretation "simple (term)" 'Simple T = (simple T).
(* Basic inversion lemmas ***************************************************)
-fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = 𝕓{J} W. U → False.
+fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
#T * -T
[ #I #J #W #U #H destruct
| #I #V #T #J #W #U #H destruct
]
qed.
-lemma simple_inv_bind: ∀I,V,T. 𝕊[𝕓{I} V. T] → False.
+lemma simple_inv_bind: ∀I,V,T. 𝕊[ⓑ{I} V. T] → False.
/2 width=6/ qed-.
let rec applv Vs T on Vs ≝
match Vs with
[ nil ⇒ T
- | cons hd tl ⇒ 𝕔{Appl} hd. (applv tl T)
+ | cons hd tl ⇒ ⓐhd. (applv tl T)
].
-interpretation "application construction (vector)" 'ApplV Vs T = (applv Vs T).
+interpretation "application o vevtor (term)"
+ 'SnApplV Vs T = (applv Vs T).
(* HOMOMORPHIC TERMS ********************************************************)
inductive thom: relation term ≝
- | thom_atom: ∀I. thom (𝕒{I}) (𝕒{I})
- | thom_abst: ∀V1,V2,T1,T2. thom (𝕔{Abst} V1. T1) (𝕔{Abst} V2. T2)
+ | thom_atom: ∀I. thom (⓪{I}) (⓪{I})
+ | thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2)
| thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] →
- thom (𝕔{Appl} V1. T1) (𝕔{Appl} V2. T2)
+ thom (ⓐV1. T1) (ⓐV2. T2)
.
interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
(* Basic inversion lemmas ***************************************************)
-fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕓{I}W1.U1 →
- ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2.
+fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 →
+ ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
]
qed.
-lemma thom_inv_bind1: ∀I,W1,U1,T2. 𝕓{I}W1.U1 ≈ T2 →
- ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2.
+lemma thom_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 →
+ ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
/2 width=5/ qed-.
-fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕗{I}W1.U1 →
+fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] &
- I = Appl & T2 = 𝕔{Appl} W2. U2.
+ I = Appl & T2 = ⓐW2. U2.
#T1 #T2 * -T1 -T2
[ #J #I #W1 #U1 #H destruct
| #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
]
qed.
-lemma thom_inv_flat1: ∀I,W1,U1,T2. 𝕗{I}W1.U1 ≈ T2 →
+lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] &
- I = Appl & T2 = 𝕔{Appl} W2. U2.
+ I = Appl & T2 = ⓐW2. U2.
/2 width=4/ qed-.
(* Basic_1: removed theorems 7:
k : sort index
p,q : global reference position
t,u : local reference position level (de Bruijn's)
+
+NAMING CONVENTIONS FOR CONSTRUCTORS
+
+0: atomic
+2: binary
+
+A: application to vector
+
+a: application
+b: binder
+d: abbreviation
+f: flat
+l: abstraction
+t: native type annotation
(* Grammar ******************************************************************)
+notation "hvbox( ⓪ )"
+ non associative with precedence 90
+ for @{ 'Item0 }.
+
+notation "hvbox( ⓪ { I } )"
+ non associative with precedence 90
+ for @{ 'Item0 $I }.
+
notation "hvbox( ⋆ )"
non associative with precedence 90
for @{ 'Star }.
non associative with precedence 90
for @{ 'GRef $p }.
-notation "hvbox( 𝕒 )"
+notation "hvbox( ② term 90 T1 . break term 90 T )"
non associative with precedence 90
- for @{ 'SItem }.
+ for @{ 'SnItem2 $T1 $T }.
-notation "hvbox( 𝕒 { I } )"
+notation "hvbox( ② { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
- for @{ 'SItem $I }.
+ for @{ 'SnItem2 $I $T1 $T }.
-notation "hvbox( 𝕔 term 90 T1 . break term 90 T )"
+notation "hvbox( ⓑ { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
- for @{ 'SItem $T1 $T }.
+ for @{ 'SnBind2 $I $T1 $T }.
-notation "hvbox( 𝕔 { I } break term 90 T1 . break term 90 T )"
+notation "hvbox( ⓕ { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
- for @{ 'SItem $I $T1 $T }.
+ for @{ 'SnFlat2 $I $T1 $T }.
-notation "hvbox( 𝕓 { I } break term 90 T1 . break term 90 T )"
+notation "hvbox( ⓓ term 90 T1 . break term 90 T2 )"
non associative with precedence 90
- for @{ 'SBind $I $T1 $T }.
+ for @{ 'SnAbbr $T1 $T2 }.
-notation "hvbox( 𝕗 { I } break term 90 T1 . break term 90 T )"
+notation "hvbox( ⓛ term 90 T1 . break term 90 T2 )"
non associative with precedence 90
- for @{ 'SFlat $I $T1 $T }.
+ for @{ 'SnAbst $T1 $T2 }.
+
+notation "hvbox( ⓐ term 90 T1 . break term 90 T2 )"
+ non associative with precedence 90
+ for @{ 'SnAppl $T1 $T2 }.
+
+notation "hvbox( ⓣ term 90 T1 . break term 90 T2 )"
+ non associative with precedence 90
+ for @{ 'SnCast $T1 $T2 }.
notation "hvbox( Ⓐ term 90 T1 . break term 90 T )"
non associative with precedence 90
- for @{ 'ApplV $T1 $T }.
+ for @{ 'SnApplV $T1 $T }.
-notation "hvbox( T . break 𝕓 { I } break term 90 T1 )"
- non associative with precedence 89
- for @{ 'DBind $T $I $T1 }.
-(*
-notation > "hvbox( T . break 𝕔 { I } break term 90 T1 )"
+notation > "hvbox( T . break ②{ I } break term 47 T1 )"
+ non associative with precedence 46
+ for @{ 'DxBind2 $T $I $T1 }.
+
+notation "hvbox( T . break ⓑ { I } break term 90 T1 )"
non associative with precedence 89
- for @{ 'DBind $T $I $T1 }.
-*) (**) (* this breaks all parsing *)
+ for @{ 'DxBind2 $T $I $T1 }.
+
+notation "hvbox( T1 . break ⓓ T2 )"
+ left associative with precedence 48
+ for @{ 'DxAbbr $T1 $T2 }.
+
+notation "hvbox( T1 . break ⓛ T2 )"
+ left associative with precedence 49
+ for @{ 'DxAbst $T1 $T2 }.
+
notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )"
non associative with precedence 47
- for @{ 'DBind $T $I $T1 $T2 $T3 }.
+ for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
notation "hvbox( # [ x ] )"
non associative with precedence 90
(* Note: new property *)
(* Basic_1: was only: pr2_thin_dx *)
lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
- L ⊢ V1 ➡ V2 → L ⊢ T1 ➡ T2 → L ⊢ 𝕗{I} V1. T1 ➡ 𝕗{I} V2. T2.
+ L ⊢ V1 ➡ V2 → L ⊢ T1 ➡ T2 → L ⊢ ⓕ{I} V1. T1 ➡ ⓕ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
qed.
lemma cpr_cast: ∀L,V,T1,T2.
- L ⊢ T1 ➡ T2 → L ⊢ 𝕔{Cast} V. T1 ➡ T2.
+ L ⊢ T1 ➡ T2 → L ⊢ ⓣV. T1 ➡ T2.
#L #V #T1 #T2 * /3 width=3/
qed.
qed-.
(* Basic_1: was: pr2_gen_cast *)
-lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ➡ U2 → (
+lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓣV1. T1 ➡ U2 → (
∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 &
- U2 = 𝕔{Cast} V2. T2
+ U2 = ⓣV2. T2
) ∨ L ⊢ T1 ➡ U2.
#L #V1 #T1 #U2 * #X #H #HU2
elim (tpr_inv_cast1 … H) -H /3 width=3/
(* Advanced properties ******************************************************)
lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 →
- L ⊢ 𝕓{I} V1. T1 ➡ 𝕓{I} V2. T2.
+ L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12
@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
qed.
(* Basic_1: was only: pr2_gen_cbind *)
-lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ➡ V2 → L. 𝕓{I} V2 ⊢ T1 ➡ T2 →
- L ⊢ 𝕓{I} V1. T1 ➡ 𝕓{I} V2. T2.
+lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T2 →
+ L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2 width=1/ #HT0
+lapply (tpss_lsubs_conf … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
lapply (tpss_tps … HT0) -HT0 #HT0
@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
qed.
(* Advanced properties ******************************************************)
lemma cpr_cdelta: ∀L,K,V1,W1,W2,i.
- ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ▶* W1 →
+ ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, |L| - i - 1] ▶* W1 →
⇧[0, i + 1] W1 ≡ W2 → L ⊢ #i ➡ W2.
#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
(* Basic_1: was: pr2_gen_lref *)
lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ➡ T2 →
T2 = #i ∨
- ∃∃K,V1,T1. ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 &
+ ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 &
K ⊢ V1 [0, |L| - i - 1] ▶* T1 &
⇧[0, i + 1] T1 ≡ T2 &
i < |L|.
qed-.
(* Basic_1: was: pr2_gen_abst *)
-lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ➡ U2 →
- ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+lemma cpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 →
+ ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
/2 width=3/ qed-.
(* Relocation properties ****************************************************)
inductive ltpr: relation lenv ≝
| ltpr_stom: ltpr (⋆) (⋆)
| ltpr_pair: ∀K1,K2,I,V1,V2.
- ltpr K1 K2 → V1 ➡ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+ ltpr K1 K2 → V1 ➡ V2 → ltpr (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) (*ⓑ*)
.
interpretation
lemma ltpr_inv_atom1: ∀L2. ⋆ ➡ L2 → L2 = ⋆.
/2 width=3/ qed-.
-fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ➡ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
- ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. 𝕓{I} V2.
+fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ➡ L2 → ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. ⓑ{I} V2.
#L1 #L2 * -L1 -L2
[ #K1 #I #V1 #H destruct
| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/
qed.
(* Basic_1: was: wcpr0_gen_head *)
-lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ➡ L2 →
- ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. 𝕓{I} V2.
+lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 ➡ L2 →
+ ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. ⓑ{I} V2.
/2 width=3/ qed-.
fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ➡ L2 → L2 = ⋆ → L1 = ⋆.
lemma ltpr_inv_atom2: ∀L1. L1 ➡ ⋆ → L1 = ⋆.
/2 width=3/ qed-.
-fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ➡ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
- ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. 𝕓{I} V1.
+fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ➡ L2 → ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. ⓑ{I} V1.
#L1 #L2 * -L1 -L2
[ #K2 #I #V2 #H destruct
| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/
]
qed.
-lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. 𝕓{I} V2 →
- ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. 𝕓{I} V1.
+lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. ⓑ{I} V1.
/2 width=3/ qed-.
(* Basic forward lemmas *****************************************************)
(* Basic inversion lemmas ***************************************************)
-lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T].
+lemma tnf_inv_abst: ∀V,T. ℕ[ⓛV.T] → ℕ[V] ∧ ℕ[T].
#V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓛV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
]
qed-.
-lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
+lemma tnf_inv_appl: ∀V,T. ℕ[ⓐV.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
#V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
| generalize in match HVT1; -HVT1 elim T1 -T1 * // * #W1 #U1 #_ #_ #H
[ elim (lift_total V1 0 1) #V2 #HV12
- lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2 width=3/ -HV12 #H destruct
- | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2 width=1/ #H destruct
+ lapply (H (ⓓW1.ⓐV2.U1) ?) -H /2 width=3/ -HV12 #H destruct
+ | lapply (H (ⓓV1.U1) ?) -H /2 width=1/ #H destruct
]
qed-.
-lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
+lemma tnf_inv_abbr: ∀V,T. ℕ[ⓓV.T] → False.
#V #T #H elim (is_lift_dec T 0 1)
[ * #U #HTU
lapply (H U ?) -H /2 width=3/ #H destruct
elim (lift_inv_pair_xy_y … HTU)
| #HT
- elim (tps_full (⋆) V T (⋆. 𝕓{Abbr} V) 0 ?) // #T2 #T1 #HT2 #HT12
- lapply (H (𝕓{Abbr}V.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
+ elim (tps_full (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
+ lapply (H (ⓓV.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
]
qed.
-lemma tnf_inv_cast: ∀V,T. ℕ[𝕔{Cast}V.T] → False.
+lemma tnf_inv_cast: ∀V,T. ℕ[ⓣV.T] → False.
#V #T #H lapply (H T ?) -H /2 width=1/ #H
@(discr_tpair_xy_y … H)
qed-.
theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
/2 width=3/ qed.
-lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[𝕔{Abst}V.T].
+lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T].
/4 width=1/ qed.
-lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[𝕔{Appl}V.T].
+lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T].
/4 width=1/ qed.
(* Basic_1: includes: pr0_delta1 *)
inductive tpr: relation term ≝
-| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
+| tpr_atom : ∀I. tpr (⓪{I}) (⓪{I})
| tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
- tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+ tpr (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
| tpr_beta : ∀V1,V2,W,T1,T2.
- tpr V1 V2 → tpr T1 T2 →
- tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2)
+ tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
| tpr_delta: ∀I,V1,V2,T1,T2,T.
- tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ▶ T →
- tpr (𝕓{I} V1. T1) (𝕓{I} V2. T)
+ tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T →
+ tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T)
| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
- tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2)
-| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 →
- tpr (𝕔{Abbr} V. T) T2
-| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2
+ tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
+| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
+| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (ⓣV. T1) T2
.
interpretation
(* Basic properties *********************************************************)
lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 →
- 𝕓{I} V1. T1 ➡ 𝕓{I} V2. T2.
+ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
(* Basic inversion lemmas ***************************************************)
-fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}.
+fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = ⓪{I} → U2 = ⓪{I}.
#U1 #U2 * -U1 -U2
[ //
| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
qed.
(* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
-lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ➡ U2 → U2 = 𝕒{I}.
+lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
/2 width=3/ qed-.
-fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ▶ T &
- U2 = 𝕓{I} V2. T
+ ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ U2 = ⓑ{I} V2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
#U1 #U2 * -U1 -U2
]
qed.
-lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ➡ U2 →
+lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ▶ T &
- U2 = 𝕓{I} V2. T
+ ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ U2 = ⓑ{I} V2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
/2 width=3/ qed-.
(* Basic_1: was pr0_gen_abbr *)
-lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ➡ U2 →
+lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
(∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
- ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ▶ T &
- U2 = 𝕓{Abbr} V2. T
+ ⋆. ⓓV2 ⊢ T2 [0, 1] ▶ T &
+ U2 = ⓓV2. T
) ∨
∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 … H) -H * /3 width=7/
qed-.
-fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 →
+fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = ⓕ{I} V1. U0 →
∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
- U2 = 𝕗{I} V2. T2
+ U2 = ⓕ{I} V2. T2
| ∃∃V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2 & I = Appl
+ U0 = ⓛW. T1 &
+ U2 = ⓓV2. T2 & I = Appl
| ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
⇧[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+ U0 = ⓓW1. T1 &
+ U2 = ⓓW2. ⓐV. T2 &
I = Appl
| (U0 ➡ U2 ∧ I = Cast).
#U1 #U2 * -U1 -U2
]
qed.
-lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ➡ U2 →
+lemma tpr_inv_flat1: ∀V1,U0,U2,I. ⓕ{I} V1. U0 ➡ U2 →
∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
- U2 = 𝕗{I} V2. T2
+ U2 = ⓕ{I} V2. T2
| ∃∃V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2 & I = Appl
+ U0 = ⓛW. T1 &
+ U2 = ⓓV2. T2 & I = Appl
| ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
⇧[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+ U0 = ⓓW1. T1 &
+ U2 = ⓓW2. ⓐV. T2 &
I = Appl
| (U0 ➡ U2 ∧ I = Cast).
/2 width=3/ qed-.
(* Basic_1: was pr0_gen_appl *)
-lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ➡ U2 →
+lemma tpr_inv_appl1: ∀V1,U0,U2. ⓐV1. U0 ➡ U2 →
∨∨ ∃∃V2,T2. V1 ➡ V2 & U0 ➡ T2 &
- U2 = 𝕔{Appl} V2. T2
+ U2 = ⓐV2. T2
| ∃∃V2,W,T1,T2. V1 ➡ V2 & T1 ➡ T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2
+ U0 = ⓛW. T1 &
+ U2 = ⓓV2. T2
| ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
⇧[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
+ U0 = ⓓW1. T1 &
+ U2 = ⓓW2. ⓐV. T2.
#V1 #U0 #U2 #H
elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
qed-.
(* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ➡ U → 𝕊[T1] →
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝕊[T1] →
∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
- U = 𝕔{Appl} V2. T2.
+ U = ⓐV2. T2.
#V1 #T1 #U #H #HT1
elim (tpr_inv_appl1 … H) -H *
[ /2 width=5/
qed-.
(* Basic_1: was: pr0_gen_cast *)
-lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ➡ U2 →
- (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Cast} V2. T2)
+lemma tpr_inv_cast1: ∀V1,T1,U2. ⓣV1. T1 ➡ U2 →
+ (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓣV2. T2)
∨ T1 ➡ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_flat1 … H) -H * /3 width=5/
fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
- T1 = 𝕔{Abbr} V. T
- | ∃∃V,T. T ➡ #i & T1 = 𝕔{Cast} V. T.
+ T1 = ⓓV. T
+ | ∃∃V,T. T ➡ #i & T1 = ⓣV. T.
#T1 #T2 * -T1 -T2
[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
∨∨ T1 = #i
| ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
- T1 = 𝕔{Abbr} V. T
- | ∃∃V,T. T ➡ #i & T1 = 𝕔{Cast} V. T.
+ T1 = ⓓV. T
+ | ∃∃V,T. T ➡ #i & T1 = ⓣV. T.
/2 width=3/ qed-.
(* Basic_1: removed theorems 3:
(* Advanced inversion lemmas ************************************************)
-fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 →
- ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = ⓛV1. T1 →
+ ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
#U1 #U2 * -U1 -U2
[ #I #V #T #H destruct
| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
qed.
(* Basic_1: was pr0_gen_abst *)
-lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ➡ U2 →
- ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+lemma tpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 →
+ ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
/2 width=3/ qed-.
(* Confluence lemmas ********************************************************)
-fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ➡ X & 𝕒{I} ➡ X.
+fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X.
/2 width=3/ qed.
fact tpr_conf_flat_flat:
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 →
- ∃∃T0. 𝕗{I} V1. T1 ➡ T0 & 𝕗{I} V2. T2 ➡ T0.
+ ∃∃T0. ⓕ{I} V1. T1 ➡ T0 & ⓕ{I} V2. T2 ➡ T0.
#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → V0 ➡ V2 →
- U0 ➡ T2 → 𝕔{Abst} W0. U0 ➡ T1 →
- ∃∃X. 𝕔{Appl} V1. T1 ➡ X & 𝕔{Abbr} V2. T2 ➡ X.
+ U0 ➡ T2 → ⓛW0. U0 ➡ T1 →
+ ∃∃X. ⓐV1. T1 ➡ X & ⓓV2. T2 ➡ X.
#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct
elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → V0 ➡ V2 → ⇧[O,1] V2 ≡ V →
- W0 ➡ W2 → U0 ➡ U2 → 𝕔{Abbr} W0. U0 ➡ T1 →
- ∃∃X. 𝕔{Appl} V1. T1 ➡ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ➡ X.
+ W0 ➡ W2 → U0 ➡ U2 → ⓓW0. U0 ➡ T1 →
+ ∃∃X. ⓐV1. T1 ➡ X & ⓓW2. ⓐV. U2 ➡ X.
#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #VV #HVV1 #HVV2
elim (lift_total VV 0 1) #VVV #HVV
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → T0 ➡ T1 → T0 ➡ X2 →
- ∃∃X. 𝕔{Cast} V1. T1 ➡ X & X2 ➡ X.
+ ∃∃X. ⓣV1. T1 ➡ X & X2 ➡ X.
#X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/
qed.
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 →
- ∃∃X. 𝕔{Abbr} V1. T1 ➡X & 𝕔{Abbr} V2. T2 ➡ X.
+ ∃∃X. ⓓV1. T1 ➡X & ⓓV2. T2 ➡ X.
#W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/
elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ /3 width=5/
∃∃X. X1 ➡ X & X2 ➡ X
) →
V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 →
- ⋆. 𝕓{I1} V1 ⊢ T1 [O, 1] ▶ TT1 →
- ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ▶ TT2 →
- ∃∃X. 𝕓{I1} V1. TT1 ➡ X & 𝕓{I1} V2. TT2 ➡ X.
+ ⋆. ⓑ{I1} V1 ⊢ T1 [O, 1] ▶ TT1 →
+ ⋆. ⓑ{I1} V2 ⊢ T2 [O, 1] ▶ TT2 →
+ ∃∃X. ⓑ{I1} V1. TT1 ➡ X & ⓑ{I1} V2. TT2 ➡ X.
#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
- V0 ➡ V1 → T0 ➡ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ▶ TT1 →
+ V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 [O,1] ▶ TT1 →
T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 →
- ∃∃X. 𝕓{Abbr} V1. TT1 ➡ X & X2 ➡ X.
+ ∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X.
#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct
) →
V0 ➡ V1 → V0 ➡ V2 → W0 ➡ W1 → W0 ➡ W2 → T0 ➡ T1 → T0 ➡ T2 →
⇧[O, 1] V1 ≡ VV1 → ⇧[O, 1] V2 ≡ VV2 →
- ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ➡ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ➡ X.
+ ∃∃X. ⓓW1. ⓐVV1. T1 ➡ X & ⓓW2. ⓐVV2. T2 ➡ X.
#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
elim (IH … HW01 … HW02) -HW01 -HW02 /2 width=1/ #W #HW1 #HW2
elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
- lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
+ elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+ lapply (tpss_lsubs_conf … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
- elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+ elim (IHT12 … HTT1 (L2. ⓑ{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
- lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2 width=1/ #HTT2
- elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
- lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
+ lapply (tps_lsubs_conf … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
+ elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
+ lapply (tpss_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
- lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
+ lapply (tpss_lsubs_conf … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2
- elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+ elim (IHT12 … HTT1 (L2. ⓓWW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
elim (lift_total VV2 0 1) #VV #H2VV
- lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
+ lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
@ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
| #V1 #TT1 #T1 #T2 #HTT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct
qed.
lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 →
- ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ▶ U1 →
- ∃∃U2. U1 ➡ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ▶ U2.
+ ⋆. ⓑ{I} V1 ⊢ T1 [0, 1] ▶ U1 →
+ ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ U2.
#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -T1 /2 width=1/ /3 width=3/
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ /3 width=3/
qed.
lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
(* reducible terms *)
inductive trf: predicate term ≝
-| trf_abst_sn: ∀V,T. trf V → trf (𝕔{Abst} V. T)
-| trf_abst_dx: ∀V,T. trf T → trf (𝕔{Abst} V. T)
-| trf_appl_sn: ∀V,T. trf V → trf (𝕔{Appl} V. T)
-| trf_appl_dx: ∀V,T. trf T → trf (𝕔{Appl} V. T)
-| trf_abbr : ∀V,T. trf (𝕔{Abbr} V. T)
-| trf_cast : ∀V,T. trf (𝕔{Cast} V. T)
-| trf_beta : ∀V,W,T. trf (𝕔{Appl} V. 𝕔{Abst} W. T)
+| trf_abst_sn: ∀V,T. trf V → trf (ⓛV. T)
+| trf_abst_dx: ∀V,T. trf T → trf (ⓛV. T)
+| trf_appl_sn: ∀V,T. trf V → trf (ⓐV. T)
+| trf_appl_dx: ∀V,T. trf T → trf (ⓐV. T)
+| trf_abbr : ∀V,T. trf (ⓓV. T)
+| trf_cast : ∀V,T. trf (ⓣV. T)
+| trf_beta : ∀V,W,T. trf (ⓐV. ⓛW. T)
.
interpretation
(* Basic inversion lemmas ***************************************************)
-fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = 𝕒{I} → False.
+fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T = ⓪{I} → False.
#I #T * -T
[ #V #T #_ #H destruct
| #V #T #_ #H destruct
]
qed.
-lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
+lemma trf_inv_atom: ∀I. ℝ[⓪{I}] → False.
/2 width=4/ qed-.
-fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
+fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = ⓛW. U → ℝ[W] ∨ ℝ[U].
#W #U #T * -T
[ #V #T #HV #H destruct /2 width=1/
| #V #T #HT #H destruct /2 width=1/
]
qed.
-lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
+lemma trf_inv_abst: ∀V,T. ℝ[ⓛV.T] → ℝ[V] ∨ ℝ[T].
/2 width=3/ qed-.
-fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Appl} W. U →
+fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = ⓐW. U →
∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
#W #U #T * -T
[ #V #T #_ #H destruct
]
qed.
-lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
+lemma trf_inv_appl: ∀W,U. ℝ[ⓐW.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
/2 width=3/ qed-.
-lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
+lemma tif_inv_abbr: ∀V,T. 𝕀[ⓓV.T] → False.
/2 width=1/ qed-.
-lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
+lemma tif_inv_abst: ∀V,T. 𝕀[ⓛV.T] → 𝕀[V] ∧ 𝕀[T].
/4 width=1/ qed-.
-lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
+lemma tif_inv_appl: ∀V,T. 𝕀[ⓐV.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
#V #T #HVT @and3_intro /3 width=1/
generalize in match HVT; -HVT elim T -T //
* // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
qed-.
-lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
+lemma tif_inv_cast: ∀V,T. 𝕀[ⓣV.T] → False.
/2 width=1/ qed-.
(* Basic properties *********************************************************)
-lemma tif_atom: ∀I. 𝕀[𝕒{I}].
+lemma tif_atom: ∀I. 𝕀[⓪{I}].
/2 width=4/ qed.
-lemma tif_abst: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕀[𝕔 {Abst}V.T].
+lemma tif_abst: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕀[ⓛV.T].
#V #T #HV #HT #H
elim (trf_inv_abst … H) -H /2 width=1/
qed.
-lemma tif_appl: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕊[T] → 𝕀[𝕔{Appl}V.T].
+lemma tif_appl: ∀V,T. 𝕀[V] → 𝕀[T] → 𝕊[T] → 𝕀[ⓐV.T].
#V #T #HV #HT #S #H
elim (trf_inv_appl … H) -H /2 width=1/
qed.
(* 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_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: ∀L,V,T,B,A.
- aaa L V B → aaa (L. 𝕓{Abbr} V) T A → aaa L (𝕔{Abbr} V. T) A
+ aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓV. T) A
| aaa_abst: ∀L,V,T,B,A.
- aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abst} V. T) (𝕔 B. A)
-| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (𝕔 B. A) → aaa L (𝕔{Appl} V. T) A
-| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (𝕔{Cast} V. T) A
+ aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛ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
.
-interpretation
- "atomic arity assignment (term)"
+interpretation "atomic arity assignment (term)"
'AtomicArity L T A = (aaa L T A).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact aaa_inv_sort_aux: ∀L,T,A. L ⊢ T ÷ A → ∀k. T = ⋆k → A = ⓪.
+#L #T #A * -L -T -A
+[ //
+| #I #L #K #V #B #i #_ #_ #k #H destruct
+| #L #V #T #B #A #_ #_ #k #H destruct
+| #L #V #T #B #A #_ #_ #k #H destruct
+| #L #V #T #B #A #_ #_ #k #H destruct
+| #L #V #T #A #_ #_ #k #H destruct
+]
+qed.
+
+lemma aaa_inv_sort: ∀L,A,k. L ⊢ ⋆k ÷ A → A = ⓪.
+/2 width=5/ qed-.
+
+fact aaa_inv_lref_aux: ∀L,T,A. 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/
+| #L #V #T #B #A #_ #_ #i #H destruct
+| #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_lref: ∀L,A,i. L ⊢ #i ÷ A →
+ ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A.
+/2 width=3/ qed-.
+
+fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓓW. U →
+ ∃∃B. L ⊢ W ÷ B & L. ⓓW ⊢ U ÷ A.
+#L #T #A * -L -T -A
+[ #L #k #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #W #U #H destruct
+| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=2/
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #A #_ #_ #W #U #H destruct
+]
+qed.
+
+lemma aaa_inv_abbr: ∀L,V,T,A. L ⊢ ⓓV. T ÷ A →
+ ∃∃B. L ⊢ V ÷ B & L. ⓓV ⊢ T ÷ A.
+/2 width=3/ qed-.
+
+fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓛW. U →
+ ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ U ÷ B2 & A = ②B1. B2.
+#L #T #A * -L -T -A
+[ #L #k #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=5/
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #A #_ #_ #W #U #H destruct
+]
+qed.
+
+lemma aaa_inv_abst: ∀L,W,T,A. L ⊢ ⓛW. T ÷ A →
+ ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ T ÷ B2 & A = ②B1. B2.
+/2 width=3/ qed-.
+
+fact aaa_inv_appl_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓐW. U →
+ ∃∃B. L ⊢ W ÷ B & 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
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #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_appl: ∀L,V,T,A. L ⊢ ⓐV. T ÷ A →
+ ∃∃B. L ⊢ V ÷ B & L ⊢ T ÷ ②B. A.
+/2 width=3/ qed-.
+
+fact aaa_inv_cast_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓣW. U →
+ L ⊢ W ÷ A ∧ 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
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #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/
+]
+qed.
+
+lemma aaa_inv_cast: ∀L,W,T,A. L ⊢ ⓣW. T ÷ A →
+ L ⊢ W ÷ A ∧ L ⊢ T ÷ A.
+/2 width=3/ qed-.
inductive lsuba: relation lenv ≝
| lsuba_atom: lsuba (⋆) (⋆)
-| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V)
| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ÷ A → L2 ⊢ W ÷ A →
- lsuba L1 L2 → lsuba (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+ lsuba L1 L2 → lsuba (L1. ⓓV) (L2. ⓛW)
.
interpretation
(* Basic inversion lemmas ***************************************************)
-fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I} W →
- (∃∃K1. K1 ÷⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+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 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
- L1 = K1. 𝕓{Abbr} V & I = Abst.
+ L1 = K1. ⓓV & I = Abst.
#L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
]
qed.
-lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ÷⊑ K2. 𝕓{I} W →
- (∃∃K1. K1 ÷⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ÷⊑ K2. ⓑ{I} W →
+ (∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨
∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
- L1 = K1. 𝕓{Abbr} V & I = Abst.
+ L1 = K1. ⓓV & I = Abst.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
inductive gdrop (e:nat): relation genv ≝
| gdrop_gt: ∀G. |G| ≤ e → gdrop e G (⋆)
| gdrop_eq: ∀G. |G| = e + 1 → gdrop e G G
-| gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. 𝕓{I} V) G2
+| gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. ⓑ{I} V) G2
.
interpretation "global slicing"
]
qed-.
-fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇩[e] G ≡ G2 → G = G1. 𝕓{I} V →
+fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇩[e] G ≡ G2 → G = G1. ⓑ{I} V →
e < |G1| → ⇩[e] G1 ≡ G2.
#I #G #G1 #G2 #V #e * -G -G2
[ #G #H1 #H destruct #H2
qed.
lemma gdrop_inv_lt: ∀I,G1,G2,V,e.
- ⇩[e] G1. 𝕓{I} V ≡ G2 → e < |G1| → ⇩[e] G1 ≡ G2.
+ ⇩[e] G1. ⓑ{I} V ≡ G2 → e < |G1| → ⇩[e] G1 ≡ G2.
/2 width=5/ qed-.
(* Basic properties *********************************************************)
(* Basic_1: includes: ldrop_skip_bind *)
inductive ldrop: nat → nat → relation lenv ≝
| ldrop_atom : ∀d,e. ldrop d e (⋆) (⋆)
-| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
-| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. 𝕓{I} V) L2
+| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
+| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. ⓑ{I} V) L2
| ldrop_skip : ∀L1,L2,I,V1,V2,d,e.
ldrop d e L1 L2 → ⇧[d,e] V2 ≡ V1 →
- ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
+ ldrop (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
.
interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
/2 width=5/ qed-.
fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 →
- ∀K,I,V. L1 = K. 𝕓{I} V →
- (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+ ∀K,I,V. L1 = K. ⓑ{I} V →
+ (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
(0 < e ∧ ⇩[d, e - 1] K ≡ L2).
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #K #I #V #H destruct
]
qed.
-lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇩[0, e] K. 𝕓{I} V ≡ L2 →
- (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 →
+ (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
(0 < e ∧ ⇩[0, e - 1] K ≡ L2).
/2 width=3/ qed-.
(* Basic_1: was: ldrop_gen_ldrop *)
lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
- ⇩[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
+ ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
#e #K #I #V #L2 #H #He
elim (ldrop_inv_O1 … H) -H * // #H destruct
elim (lt_refl_false … He)
qed-.
fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
- ∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
+ ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
⇧[d - 1, e] V2 ≡ V1 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K #V #H destruct
| #L #I #V #H elim (lt_refl_false … H)
qed.
(* Basic_1: was: ldrop_gen_skip_l *)
-lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d →
+lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d →
∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
⇧[d - 1, e] V2 ≡ V1 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
/2 width=3/ qed-.
fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+ ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 &
⇧[d - 1, e] V2 ≡ V1 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K #V #H destruct
| #L #I #V #H elim (lt_refl_false … H)
qed.
(* Basic_1: was: ldrop_gen_skip_r *)
-lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
+lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < d →
∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & ⇧[d - 1, e] V2 ≡ V1 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
qed.
lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
- ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. 𝕓{I} V ≡ L2.
+ ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. ⓑ{I} V ≡ L2.
#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
- ∀K1,V,i. ⇩[0, i] L1 ≡ K1. 𝕓{Abbr} V →
+ ∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV →
d ≤ i → i < d + e →
∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
- ⇩[0, i] L2 ≡ K2. 𝕓{Abbr} V.
+ ⇩[0, i] L2 ≡ K2. ⓓV.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
[ #d #e #K1 #V #i #H
lapply (ldrop_inv_atom1 … H) -H #H destruct
(* Basic forvard lemmas *****************************************************)
(* Basic_1: was: ldrop_S *)
-lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. 𝕓{I2} V2 →
+lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
⇩[O, e + 1] L1 ≡ K2.
#L1 elim L1 -L1
[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
qed-.
lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
- ⇩[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|.
+ ⇩[0, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
#L1 elim L1 -L1
[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
(* Basic_1: was: ldrop_conf_lt *)
theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
- ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. 𝕓{I} V2 →
+ ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
e2 < d1 → let d ≝ d1 - e2 - 1 in
- ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. 𝕓{I} V1 &
+ ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1
[ #d #e #e2 #K2 #I #V2 #H
| lift_gref : ∀p,d,e. lift d e (§p) (§p)
| lift_bind : ∀I,V1,V2,T1,T2,d,e.
lift d e V1 V2 → lift (d + 1) e T1 T2 →
- lift d e (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+ lift d e (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
| lift_flat : ∀I,V1,V2,T1,T2,d,e.
lift d e V1 V2 → lift d e T1 T2 →
- lift d e (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+ lift d e (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
.
interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2).
/2 width=5/ qed-.
fact lift_inv_bind1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
- ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
+ ∀I,V1,U1. T1 = ⓑ{I} V1.U1 →
∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
- T2 = 𝕓{I} V2. U2.
+ T2 = ⓑ{I} V2. U2.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V1 #U1 #H destruct
| #i #d #e #_ #I #V1 #U1 #H destruct
]
qed.
-lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ⇧[d,e] 𝕓{I} V1. U1 ≡ T2 →
+lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ⇧[d,e] ⓑ{I} V1. U1 ≡ T2 →
∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
- T2 = 𝕓{I} V2. U2.
+ T2 = ⓑ{I} V2. U2.
/2 width=3/ qed-.
fact lift_inv_flat1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
- ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
+ ∀I,V1,U1. T1 = ⓕ{I} V1.U1 →
∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
- T2 = 𝕗{I} V2. U2.
+ T2 = ⓕ{I} V2. U2.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V1 #U1 #H destruct
| #i #d #e #_ #I #V1 #U1 #H destruct
]
qed.
-lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ⇧[d,e] 𝕗{I} V1. U1 ≡ T2 →
+lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ⇧[d,e] ⓕ{I} V1. U1 ≡ T2 →
∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
- T2 = 𝕗{I} V2. U2.
+ T2 = ⓕ{I} V2. U2.
/2 width=3/ qed-.
fact lift_inv_sort2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
/2 width=5/ qed-.
fact lift_inv_bind2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
- ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
+ ∀I,V2,U2. T2 = ⓑ{I} V2.U2 →
∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
- T1 = 𝕓{I} V1. U1.
+ T1 = ⓑ{I} V1. U1.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
qed.
(* Basic_1: was: lift_gen_bind *)
-lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡ 𝕓{I} V2. U2 →
+lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡ ⓑ{I} V2. U2 →
∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
- T1 = 𝕓{I} V1. U1.
+ T1 = ⓑ{I} V1. U1.
/2 width=3/ qed-.
fact lift_inv_flat2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
- ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
+ ∀I,V2,U2. T2 = ⓕ{I} V2.U2 →
∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
- T1 = 𝕗{I} V1. U1.
+ T1 = ⓕ{I} V1. U1.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
qed.
(* Basic_1: was: lift_gen_flat *)
-lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡ 𝕗{I} V2. U2 →
+lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡ ⓕ{I} V2. U2 →
∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
- T1 = 𝕗{I} V1. U1.
+ T1 = ⓕ{I} V1. U1.
/2 width=3/ qed-.
-lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] 𝕔{I} V. T ≡ V → False.
+lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False.
#d #e #J #V elim V -V
[ * #i #T #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
]
qed-.
-lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] 𝕔{I} V. T ≡ T → False.
+lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → False.
#J #T elim T -T
[ * #i #V #d #e #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
(* Basic_1: includes: csubst1_bind *)
inductive ltps: nat → nat → relation lenv ≝
| ltps_atom: ∀d,e. ltps d e (⋆) (⋆)
-| ltps_pair: ∀L,I,V. ltps 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
+| ltps_pair: ∀L,I,V. ltps 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
| ltps_tps2: ∀L1,L2,I,V1,V2,e.
ltps 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶ V2 →
- ltps 0 (e + 1) (L1. 𝕓{I} V1) L2. 𝕓{I} V2
+ ltps 0 (e + 1) (L1. ⓑ{I} V1) L2. ⓑ{I} V2
| ltps_tps1: ∀L1,L2,I,V1,V2,d,e.
ltps d e L1 L2 → L2 ⊢ V1 [d, e] ▶ V2 →
- ltps (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
+ ltps (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
.
interpretation "parallel substritution (local environment)"
lemma ltps_tps2_lt: ∀L1,L2,I,V1,V2,e.
L1 [0, e - 1] ▶ L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
- 0 < e → L1. 𝕓{I} V1 [0, e] ▶ L2. 𝕓{I} V2.
+ 0 < e → L1. ⓑ{I} V1 [0, e] ▶ L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
>(plus_minus_m_m e 1) /2 width=1/
qed.
lemma ltps_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
L1 [d - 1, e] ▶ L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
- 0 < d → L1. 𝕓{I} V1 [d, e] ▶ L2. 𝕓{I} V2.
+ 0 < d → L1. ⓑ{I} V1 [d, e] ▶ L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
>(plus_minus_m_m d 1) /2 width=1/
qed.
/2 width=5/ qed-.
fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
- ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+ ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
∃∃K2,V2. K1 [0, e - 1] ▶ K2 &
K2 ⊢ V1 [0, e - 1] ▶ V2 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #_ #K1 #I #V1 #H destruct
| #L1 #I #V #_ #H elim (lt_refl_false … H)
]
qed.
-lemma ltps_inv_tps21: ∀e,K1,I,V1,L2. K1. 𝕓{I} V1 [0, e] ▶ L2 → 0 < e →
+lemma ltps_inv_tps21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 [0, e] ▶ L2 → 0 < e →
∃∃K2,V2. K1 [0, e - 1] ▶ K2 & K2 ⊢ V1 [0, e - 1] ▶ V2 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
/2 width=5/ qed-.
fact ltps_inv_tps11_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
- ∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
+ ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
∃∃K2,V2. K1 [d - 1, e] ▶ K2 &
K2 ⊢ V1 [d - 1, e] ▶ V2 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K1 #V1 #H destruct
| #L #I #V #H elim (lt_refl_false … H)
]
qed.
-lemma ltps_inv_tps11: ∀d,e,I,K1,V1,L2. K1. 𝕓{I} V1 [d, e] ▶ L2 → 0 < d →
+lemma ltps_inv_tps11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 [d, e] ▶ L2 → 0 < d →
∃∃K2,V2. K1 [d - 1, e] ▶ K2 &
K2 ⊢ V1 [d - 1, e] ▶ V2 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
/2 width=3/ qed-.
fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
/2 width=5/ qed-.
fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
- ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
+ ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
∃∃K1,V1. K1 [0, e - 1] ▶ K2 &
K2 ⊢ V1 [0, e - 1] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #_ #K1 #I #V1 #H destruct
| #L1 #I #V #_ #H elim (lt_refl_false … H)
]
qed.
-lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. 𝕓{I} V2 → 0 < e →
+lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. ⓑ{I} V2 → 0 < e →
∃∃K1,V1. K1 [0, e - 1] ▶ K2 & K2 ⊢ V1 [0, e - 1] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
/2 width=5/ qed-.
fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+ ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
K2 ⊢ V1 [d - 1, e] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K2 #V2 #H destruct
| #L #I #V #H elim (lt_refl_false … H)
]
qed.
-lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. 𝕓{I} V2 → 0 < d →
+lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d →
∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
K2 ⊢ V1 [d - 1, e] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
/2 width=3/ qed-.
(* Basic_1: removed theorems 27:
]
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
- elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
+ elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
elim (IHVW2 … HL01) -IHVW2
elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
]
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
- elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
+ elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
elim (IHVW2 … HL10) -IHVW2
elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
inductive tps: nat → nat → lenv → relation term ≝
-| tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I})
+| tps_atom : ∀L,I,d,e. tps d e L (⓪{I}) (⓪{I})
| tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
- ⇩[0, i] L ≡ K. 𝕓{Abbr} V → ⇧[0, i + 1] V ≡ W → tps d e L (#i) W
+ ⇩[0, i] L ≡ K. ⓓV → ⇧[0, i + 1] V ≡ W → tps d e L (#i) W
| tps_bind : ∀L,I,V1,V2,T1,T2,d,e.
- tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 →
- tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+ tps d e L V1 V2 → tps (d + 1) e (L. ⓑ{I} V2) T1 T2 →
+ tps d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
| tps_flat : ∀L,I,V1,V2,T1,T2,d,e.
tps d e L V1 V2 → tps d e L T1 T2 →
- tps d e L (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+ tps d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
.
interpretation "parallel substritution (term)"
qed.
(* Basic_1: was: subst1_ex *)
-lemma tps_full: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. 𝕓{Abbr} V) →
+lemma tps_full: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) →
∃∃T2,T. L ⊢ T1 [d, 1] ▶ T2 & ⇧[d, 1] T ≡ T2.
#K #V #T1 elim T1 -T1
[ * #i #L #d #HLK /2 width=4/
elim (lift_split … HVW i i ? ? ?) // /3 width=4/
| * #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
- [ elim (IHU1 (L. 𝕓{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/
+ [ elim (IHU1 (L. ⓑ{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/
| elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
]
]
elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
-Hdi -Hide >arith_c1x #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/
+ lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
-Hdi -Hide /3 width=5/
(* Basic inversion lemmas ***************************************************)
-fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → ∀I. T1 = 𝕒{I} →
- T2 = 𝕒{I} ∨
+fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → ∀I. T1 = ⓪{I} →
+ T2 = ⓪{I} ∨
∃∃K,V,i. d ≤ i & i < d + e &
- ⇩[O, i] L ≡ K. 𝕓{Abbr} V &
+ ⇩[O, i] L ≡ K. ⓓV &
⇧[O, i + 1] V ≡ T2 &
I = LRef i.
#L #T1 #T2 #d #e * -L -T1 -T2 -d -e
]
qed.
-lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ▶ T2 →
- T2 = 𝕒{I} ∨
+lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶ T2 →
+ T2 = ⓪{I} ∨
∃∃K,V,i. d ≤ i & i < d + e &
- ⇩[O, i] L ≡ K. 𝕓{Abbr} V &
+ ⇩[O, i] L ≡ K. ⓓV &
⇧[O, i + 1] V ≡ T2 &
I = LRef i.
/2 width=3/ qed-.
lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶ T2 →
T2 = #i ∨
∃∃K,V. d ≤ i & i < d + e &
- ⇩[O, i] L ≡ K. 𝕓{Abbr} V &
+ ⇩[O, i] L ≡ K. ⓓV &
⇧[O, i + 1] V ≡ T2.
#L #T2 #i #d #e #H
elim (tps_inv_atom1 … H) -H /2 width=1/
qed-.
fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
- ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+ ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 &
- L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
- U2 = 𝕓{I} V2. T2.
+ L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
+ U2 = ⓑ{I} V2. T2.
#d #e #L #U1 #U2 * -d -e -L -U1 -U2
[ #L #k #d #e #I #V1 #T1 #H destruct
| #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct
]
qed.
-lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ▶ U2 →
+lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 [d, e] ▶ U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 &
- L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
- U2 = 𝕓{I} V2. T2.
+ L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
+ U2 = ⓑ{I} V2. T2.
/2 width=3/ qed-.
fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
- ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
+ ∀I,V1,T1. U1 = ⓕ{I} V1. T1 →
∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 & L ⊢ T1 [d, e] ▶ T2 &
- U2 = 𝕗{I} V2. T2.
+ U2 = ⓕ{I} V2. T2.
#d #e #L #U1 #U2 * -d -e -L -U1 -U2
[ #L #k #d #e #I #V1 #T1 #H destruct
| #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct
]
qed.
-lemma tps_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ▶ U2 →
+lemma tps_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 [d, e] ▶ U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 & L ⊢ T1 [d, e] ▶ T2 &
- U2 = 𝕗{I} V2. T2.
+ U2 = ⓕ{I} V2. T2.
/2 width=3/ qed-.
fact tps_inv_refl_O2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 0 → T1 = T2.
(* Advanced inversion lemmas ************************************************)
fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 1 →
- ∀K,V. ⇩[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
[ //
| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct
qed.
lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶ T2 →
- ∀K,V. ⇩[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
/2 width=8/ qed-.
(* Relocation properties ****************************************************)
]
| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
- lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V1) ?) -HT02 /2 width=1/ #HT02
+ lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
elim (IHV01 … HV02) -V0 #V #HV1 #HV2
elim (IHT01 … HT02) -T0 #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/
- lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/
+ lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+ lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
| #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
elim (IHV01 … HV02) -V0
elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
elim (IHT01 … HT02 ?) -T0
[ -H #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L2. 𝕓{I} V) ?) -HT1 /2 width=1/
- lapply (tps_lsubs_conf … HT2 (L1. 𝕓{I} V) ?) -HT2 /2 width=1/ /3 width=5/
+ lapply (tps_lsubs_conf … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
+ lapply (tps_lsubs_conf … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
| -HV1 -HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %); elim H -H #H
[ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3 / is too slow *)
]
<(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=4/
| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
- lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2 width=1/ #HT02
+ lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
lapply (IHT10 … HT02 He) -T0 #HT12
- lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
+ lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
| #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1/
]
<(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
- lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2 width=1/ #HT02
+ lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V
elim (IHT10 … HT02 ?) -T0 /2 width=1/ #T #HT1 #HT2
- lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/
- lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
+ lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+ lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
| #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
elim (IHV10 … HV02 ?) -V0 //
qed.
lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
- L ⊢ V1 [d, e] ≡ V2 → L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
- L ⊢ 𝕓{I} V1. T1 [d, e] ≡ 𝕓{I} V2. T2.
+ L ⊢ V1 [d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
+ L ⊢ ⓑ{I} V1. T1 [d, e] ≡ ⓑ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
qed.
lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e.
L ⊢ V1 [d, e] ≡ V2 → L ⊢ T1 [d, e] ≡ T2 →
- L ⊢ 𝕗{I} V1. T1 [d, e] ≡ 𝕗{I} V2. T2.
+ L ⊢ ⓕ{I} V1. T1 [d, e] ≡ ⓕ{I} V2. T2.
#I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/
qed.
>(lift_inv_gref2 … HU2) -HU2 //
qed-.
-lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕓{I} V1. T1 [d, e] ≡ U2 →
+lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
- L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
- U2 = 𝕓{I} V2. T2.
+ L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
+ U2 = ⓑ{I} V2. T2.
#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
qed-.
-lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕗{I} V1. T1 [d, e] ≡ U2 →
+lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
L ⊢ T1 [d, e] ≡ T2 &
- U2 = 𝕗{I} V2. T2.
+ U2 = ⓕ{I} V2. T2.
#I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct
elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/
lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
d ≤ i → i < d + e →
- ∃∃K,V1,V2. ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 &
+ ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
⇧[0, d] V2 ≡ U2.
#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
/2 width=3/ qed-.
lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 →
- ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 →
+ ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. ⓑ{I} V2 →
∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 &
⇩*[des1] K1 ≡ K2 &
⇧*[des1] V2 ≡ V1 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
#I #des #i #des2 #H elim H -des -i -des2
[ #i #L1 #K2 #V2 #H
>(ldrops_inv_nil … H) -L1 /2 width=7/
(* Basic properties *********************************************************)
lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
- ∀I. ⇩*[des + 1] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2.
+ ∀I. ⇩*[des + 1] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
#L1 #L2 #des #H elim H -L1 -L2 -des
[ #L #V1 #V2 #HV12 #I
>(lifts_inv_nil … HV12) -HV12 //
qed-.
(* Basic_1: was: lift1_bind *)
-lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 →
+lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] ⓑ{I} V1. U1 ≡ T2 →
∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 &
- T2 = 𝕓{I} V2. U2.
+ T2 = ⓑ{I} V2. U2.
#I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5/
qed-.
(* Basic_1: was: lift1_flat *)
-lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕗{I} V1. U1 ≡ T2 →
+lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] ⓕ{I} V1. U1 ≡ T2 →
∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 &
- T2 = 𝕗{I} V2. U2.
+ T2 = ⓕ{I} V2. U2.
#I #T2 #des elim des -des
[ #V1 #U1 #H
<(lifts_inv_nil … H) -H /2 width=5/
lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
∀T1. ⇧*[des + 1] T1 ≡ T2 →
- ⇧*[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
+ ⇧*[des] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2.
#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
∀T1. ⇧*[des] T1 ≡ T2 →
- ⇧*[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2.
+ ⇧*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
[ #V #T1 #H >(lifts_inv_nil … H) -H //
| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
(* Basic properties *********************************************************)
-lemma liftsv_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
- ∀T1,T2. ⇧*[des] T1 ≡ T2 →
- ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
+lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
+ ∀T1,T2. ⇧*[des] T1 ≡ T2 →
+ ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
#V1s #V2s #des #H elim H -V1s -V2s // /3 width=1/
qed.
/2 width=5/ qed-.
(*
fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
- ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
+ ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
∃∃K1,V1. K1 [0, e - 1] ▶ K2 &
K2 ⊢ V1 [0, e - 1] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
#d #e #L1 #L2 * -d e L1 L2
[ #d #e #_ #_ #K1 #I #V1 #H destruct
| #L1 #I #V #_ #H elim (lt_refl_false … H)
]
qed.
-lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. 𝕓{I} V2 → 0 < e →
+lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. ⓑ{I} V2 → 0 < e →
∃∃K1,V1. K1 [0, e - 1] ▶ K2 & K2 ⊢ V1 [0, e - 1] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
/2 width=5/ qed.
fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+ ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
K2 ⊢ V1 [d - 1, e] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
#d #e #L1 #L2 * -d e L1 L2
[ #d #e #_ #I #K2 #V2 #H destruct
| #L #I #V #H elim (lt_refl_false … H)
]
qed.
-lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. 𝕓{I} V2 → 0 < d →
+lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d →
∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
K2 ⊢ V1 [d - 1, e] ▶ V2 &
- L1 = K1. 𝕓{I} V1.
+ L1 = K1. ⓑ{I} V1.
/2 width=1/ qed.
*)
lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶* V2 →
- L1. 𝕓{I} V1 [0, e + 1] ▶* L2. 𝕓{I} V2.
+ L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
[ /2 width=1/
| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
- 0 < e → L1. 𝕓{I} V1 [0, e] ▶* L2. 𝕓{I} V2.
+ 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
>(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶* V2 →
- L1. 𝕓{I} V1 [d + 1, e] ▶* L2. 𝕓{I} V2.
+ L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
[ /2 width=1/
| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
- 0 < d → L1. 𝕓{I} V1 [d, e] ▶* L2. 𝕓{I} V2.
+ 0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
>(plus_minus_m_m d 1) // /2 width=1/
qed.
lemma ltpss_tps2: ∀L1,L2,I,e.
L1 [0, e] ▶* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 →
- L1. 𝕓{I} V1 [0, e + 1] ▶* L2. 𝕓{I} V2.
+ L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #e #H @(ltpss_ind … H) -L2
[ /3 width=1/
| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
- 0 < e → L1. 𝕓{I} V1 [0, e] ▶* L2. 𝕓{I} V2.
+ 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
>(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶* L2 →
∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →
- L1. 𝕓{I} V1 [d + 1, e] ▶* L2. 𝕓{I} V2.
+ L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2
[ /3 width=1/
| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
- 0 < d → L1. 𝕓{I} V1 [d, e] ▶* L2. 𝕓{I} V2.
+ 0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
>(plus_minus_m_m d 1) // /2 width=1/
qed.
(* Advanced forward lemmas **************************************************)
-lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ▶* L2 →
+lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶* L2 →
∃∃K2,V2. K1 [0, e - 1] ▶* K2 & K1 ⊢ V1 [0, e - 1] ▶* V2 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
#e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2
[ /2 width=5/
| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
]
qed-.
-lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ▶* L2 →
+lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶* L2 →
∃∃K2,V2. K1 [d - 1, e] ▶* K2 &
K1 ⊢ V1 [d - 1, e] ▶* V2 &
- L2 = K2. 𝕓{I} V2.
+ L2 = K2. ⓑ{I} V2.
#d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2
[ /2 width=5/
| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
/2 width=1/ qed.
lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ▶* V2 →
- ∀I,T1,T2. L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶* T2 →
- L ⊢ 𝕓{I} V1. T1 [d, e] ▶* 𝕓{I} V2. T2.
+ ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 →
+ L ⊢ ⓑ{I} V1. T1 [d, e] ▶* ⓑ{I} V2. T2.
#L #V1 #V2 #d #e #HV12 elim HV12 -V2
[ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -T2
[ /3 width=5/
| #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
| #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12
- lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2 width=1/ #HT12
+ lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
]
qed.
lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
L ⊢ V1 [d, e] ▶ * V2 → L ⊢ T1 [d, e] ▶* T2 →
- L ⊢ 𝕗{I} V1. T1 [d, e] ▶* 𝕗{I} V2. T2.
+ L ⊢ ⓕ{I} V1. T1 [d, e] ▶* ⓕ{I} V2. T2.
#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2
[ #V2 #HV12 #HT12 elim HT12 -T2
[ /3 width=1/
]
qed-.
-lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ▶* U2 →
+lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 [d, e] ▶* U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 &
- L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶* T2 &
- U2 = 𝕓{I} V2. T2.
+ L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 &
+ U2 = ⓑ{I} V2. T2.
#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
[ /2 width=5/
| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
- lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+ lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
]
qed-.
-lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ▶* U2 →
+lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 [d, e] ▶* U2 →
∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 & L ⊢ T1 [d, e] ▶* T2 &
- U2 = 𝕗{I} V2. T2.
+ U2 = ⓕ{I} V2. T2.
#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
[ /2 width=5/
| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
lemma tpss_subst: ∀L,K,V,U1,i,d,e.
d ≤ i → i < d + e →
- ⇩[0, i] L ≡ K. 𝕓{Abbr} V → K ⊢ V [0, d + e - i - 1] ▶* U1 →
+ ⇩[0, i] L ≡ K. ⓓV → K ⊢ V [0, d + e - i - 1] ▶* U1 →
∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ▶* U2.
#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
[ /3 width=4/
(* Advanced inverion lemmas *************************************************)
-lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ▶* T2 →
- T2 = 𝕒{I} ∨
+lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 →
+ T2 = ⓪{I} ∨
∃∃K,V1,V2,i. d ≤ i & i < d + e &
- ⇩[O, i] L ≡ K. 𝕓{Abbr} V1 &
+ ⇩[O, i] L ≡ K. ⓓV1 &
K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
⇧[O, i + 1] V2 ≡ T2 &
I = LRef i.
lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶* T2 →
T2 = #i ∨
∃∃K,V1,V2. d ≤ i & i < d + e &
- ⇩[O, i] L ≡ K. 𝕓{Abbr} V1 &
+ ⇩[O, i] L ≡ K. ⓓV1 &
K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
⇧[O, i + 1] V2 ≡ T2.
#L #T2 #i #d #e #H
qed-.
lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 →
- ∀K,V. ⇩[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+ ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
qed-.
lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01
[1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
- lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
- lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2 width=1/
+ lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+ lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
<key name="include">basics/pts.ma</key>
<key name="ex">2 1</key>
<key name="ex">2 2</key>
+ <key name="ex">2 3</key>
<key name="ex">3 1</key>
<key name="ex">3 2</key>
<key name="ex">3 3</key>
interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
+(* multiple existental quantifier (2, 3) *)
+
+inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝
+ | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1).
+
(* multiple existental quantifier (3, 1) *)
inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
non associative with precedence 20
for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }.
+(* multiple existental quantifier (2, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }.
+
(* multiple existental quantifier (3, 1) *)
notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
%.stats: CHARS = $(shell cat $(MAS) | wc -c)
%.stats:
- @printf '\e[1;40;37m'
+ @printf '\x1B[1;40;37m'
@printf '%-15s %-42s' 'Statistics for:' $*
- @printf '\e[0m\n'
- @printf '\e[1;40;35m'
+ @printf '\x1B[0m\n'
+ @printf '\x1B[1;40;35m'
@printf '%-8s %6i' Chars $(CHARS)
@printf ' %-8s %5i' Lines `cat $(MAS) | wc -l`
@printf ' %-6s %3i' Pages `echo $$(($(CHARS) / 5120))`
@printf ' %-10s' ''
- @printf '\e[0m\n'
- @printf '\e[1;40;36m'
+ @printf '\x1B[0m\n'
+ @printf '\x1B[1;40;36m'
@printf '%-8s %6i' Sources `ls $(MAS) | wc -l`
@printf ' %-40s' ''
# @printf ' %-8s %5i' Objs `ls *.vo | wc -l`
# @printf ' %-6s %3i' Files `ls *.v | wc -l`
- @printf '\e[0m\n'
- @printf '\e[1;40;32m'
+ @printf '\x1B[0m\n'
+ @printf '\x1B[1;40;32m'
@printf '%-8s %6i' Theorems `grep theorem $(MAS) | wc -l`
@printf ' %-8s %5i' Lemmas `grep lemma $(MAS) | wc -l`
@printf ' %-6s %3i' Facts `grep fact $(MAS) | wc -l`
@printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l`
- @printf '\e[0m\n'
- @printf '\e[1;40;33m'
+ @printf '\x1B[0m\n'
+ @printf '\x1B[1;40;33m'
@printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l`
@printf ' %-40s' ''
# @printf ' %-8s %5i' Local `grep "Local" *.v | wc -l`
- @printf '\e[0m\n'
- @printf '\e[1;40;31m'
+ @printf '\x1B[0m\n'
+ @printf '\x1B[1;40;31m'
@printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l`
@printf ' %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l`
@printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
@printf ' %-10s' ''
- @printf '\e[0m\n'
+ @printf '\x1B[0m\n'
projects / helm.git / commitdiff