(* Basic_1: was: sc3_arity_csubc *)
theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
+ ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
⦃L2, T0⦄ [RP] ϵ 〚A〛.
#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
(* Basic_1: was: sc3_arity *)
lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L,T,A. L ⊢ T ÷ A → ⦃L, T⦄ [RP] ϵ 〚A〛.
+ ∀L,T,A. L ⊢ T ⁝ A → ⦃L, T⦄ [RP] ϵ 〚A〛.
/2 width=8/ qed.
lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L,T,A. L ⊢ T ÷ A → RP L T.
+ ∀L,T,A. L ⊢ T ⁝ A → RP L T.
#RR #RS #RP #H1RP #H2RP #L #T #A #HT
lapply (aacr_acr … H1RP H2RP A) #HA
@(s1 … HA) /2 width=4/
(* Properties concerning atomic arity assignment ****************************)
-lemma csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⬇* T.
+lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬇* T.
#L #T #A #H
@(acp_aaa … csn_acp csn_acr … H)
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/cprs.ma".
+include "basic_2/computation/csn.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* alternative definition of csn *)
+definition csna: lenv → predicate term ≝ λL. SN … (cprs L) (eq …).
+
+interpretation
+ "context-sensitive strong normalization (term) alternative"
+ 'SNAlt L T = (csna L T).
+
+(* Basic eliminators ********************************************************)
+
+lemma csna_ind: ∀L. ∀R:predicate term.
+ (∀T1. L ⊢ ⬇⬇* T1 →
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1
+ ) →
+ ∀T. L ⊢ ⬇⬇* T → R T.
+#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
+@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: sn3_intro *)
+lemma csna_intro: ∀L,T1.
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1.
+#L #T1 #H
+@(SN_intro … H)
+qed.
+
+fact csna_intro_aux: ∀L,T1.
+ (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) → L ⊢ ⬇⬇* T1.
+/4 width=3/ qed-.
+
+(* Basic_1: was: sn3_pr3_trans (old version) *)
+lemma csna_cprs_trans: ∀L,T1. L ⊢ ⬇⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇⬇* T2.
+#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
+@csna_intro #T #HLT2 #HT2
+elim (term_eq_dec T1 T2) #HT12
+[ -IHT1 -HLT12 destruct /3 width=1/
+| -HT1 -HT2 /3 width=4/
+qed.
+
+(* Basic_1: was: sn3_pr2_intro (old version) *)
+lemma csna_intro_cpr: ∀L,T1.
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇⬇* T2) →
+ L ⊢ ⬇⬇* T1.
+#L #T1 #H
+@csna_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T
+[ -H #H destruct #H
+ elim (H ?) //
+| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct
+ elim (term_eq_dec T0 T) #HT0
+ [ -HLT1 -HLT2 -H /3 width=1/
+ | -IHT -HT12 /4 width=3/
+ ]
+]
+qed.
+
+(* Main properties **********************************************************)
+
+theorem csn_csna: ∀L,T. L ⊢ ⬇* T → L ⊢ ⬇⬇* T.
+#L #T #H @(csn_ind … H) -T /4 width=1/
+qed.
+
+theorem csna_csn: ∀L,T. L ⊢ ⬇⬇* T → L ⊢ ⬇* T.
+#L #T #H @(csna_ind … H) -T /4 width=1/
+qed.
+
+(* Basic_1: was: sn3_pr3_trans *)
+lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2.
+/4 width=3/ qed.
+
+(* Main eliminators *********************************************************)
+
+lemma csn_ind_alt: ∀L. ∀R:predicate term.
+ (∀T1. L ⊢ ⬇* T1 →
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1
+ ) →
+ ∀T. L ⊢ ⬇* T → R T.
+#L #R #H0 #T1 #H @(csna_ind … (csn_csna … H)) -T1 #T1 #HT1 #IHT1
+@H0 -H0 /2 width=1/ -HT1 /3 width=1/
+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/cprs.ma".
-include "basic_2/computation/csn.ma".
-
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-
-(* Properties concerning context-sensitive computation on terms *************)
-
-definition csns: lenv → predicate term ≝ λL. SN … (cprs L) (eq …).
-
-interpretation
- "context-sensitive strong normalization (term)"
- 'SNStar L T = (csns L T).
-
-(* Basic eliminators ********************************************************)
-
-lemma csns_ind: ∀L. ∀R:predicate term.
- (∀T1. L ⊢ ⬇** T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1
- ) →
- ∀T. L ⊢ ⬇** T → R T.
-#L #R #H0 #T1 #H elim H -T1 #T1 #HT1 #IHT1
-@H0 -H0 /3 width=1/ -IHT1 /4 width=1/
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: sn3_intro *)
-lemma csns_intro: ∀L,T1.
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → L ⊢ ⬇** T2) → L ⊢ ⬇** T1.
-#L #T1 #H
-@(SN_intro … H)
-qed.
-
-fact csns_intro_aux: ∀L,T1.
- (∀T,T2. L ⊢ T ➡* T2 → T1 = T → (T1 = T2 → False) → L ⊢ ⬇** T2) → L ⊢ ⬇** T1.
-/4 width=3/ qed-.
-
-(* Basic_1: was: sn3_pr3_trans (old version) *)
-lemma csns_cprs_trans: ∀L,T1. L ⊢ ⬇** T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇** T2.
-#L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12
-@csns_intro #T #HLT2 #HT2
-elim (term_eq_dec T1 T2) #HT12
-[ -IHT1 -HLT12 destruct /3 width=1/
-| -HT1 -HT2 /3 width=4/
-qed.
-
-(* Basic_1: was: sn3_pr2_intro (old version) *)
-lemma csns_intro_cpr: ∀L,T1.
- (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇** T2) →
- L ⊢ ⬇** T1.
-#L #T1 #H
-@csns_intro_aux #T #T2 #H @(cprs_ind_dx … H) -T
-[ -H #H destruct #H
- elim (H ?) //
-| #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct
- elim (term_eq_dec T0 T) #HT0
- [ -HLT1 -HLT2 -H /3 width=1/
- | -IHT -HT12 /4 width=3/
- ]
-]
-qed.
-
-(* Main properties **********************************************************)
-
-theorem csn_csns: ∀L,T. L ⊢ ⬇* T → L ⊢ ⬇** T.
-#L #T #H @(csn_ind … H) -T /4 width=1/
-qed.
-
-theorem csns_csn: ∀L,T. L ⊢ ⬇** T → L ⊢ ⬇* T.
-#L #T #H @(csns_ind … H) -T /4 width=1/
-qed.
-
-(* Basic_1: was: sn3_pr3_trans *)
-lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2.
-/4 width=3/ qed.
-
-(* Main eliminators *********************************************************)
-
-lemma csn_ind_cprs: ∀L. ∀R:predicate term.
- (∀T1. L ⊢ ⬇* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 = T2 → False) → R T2) → R T1
- ) →
- ∀T. L ⊢ ⬇* T → R T.
-#L #R #H0 #T1 #H @(csns_ind … (csn_csns … H)) -T1 #T1 #HT1 #IHT1
-@H0 -H0 /2 width=1/ -HT1 /3 width=1/
-qed-.
include "basic_2/computation/cprs_cprs.ma".
include "basic_2/computation/csn_lift.ma".
include "basic_2/computation/csn_cpr.ma".
-include "basic_2/computation/csn_cprs.ma".
+include "basic_2/computation/csn_alt.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* Advanced properties ******************************************************)
lemma csn_lcpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬇* T → L2 ⊢ ⬇* T.
-#L1 #L2 #HL12 #T #H @(csn_ind_cprs … H) -T #T #_ #IHT
+#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
@csn_intro #T0 #HLT0 #HT0
@IHT /2 width=2/ -IHT -HT0 /2 width=3/
qed.
lemma csn_abbr: ∀L,V. L ⊢ ⬇* V → ∀T. L. ⓓV ⊢ ⬇* T → L ⊢ ⬇* ⓓV. T.
-#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_cprs … HT) -T #T #HT #IHT
+#L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
elim (cpr_inv_abbr1 … H1) -H1 *
[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct
fact csn_appl_beta_aux: ∀L,W. L ⊢ ⬇* W → ∀U. L ⊢ ⬇* U →
∀V,T. U = ⓓV. T → L ⊢ ⬇* ⓐV. ⓛW. T.
-#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_cprs … H) -X #X #HVT #IHVT #V #T #H destruct
+#L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct
lapply (csn_fwd_pair_sn … HVT) #HV
lapply (csn_fwd_bind_dx … HVT) #HT -HVT
@csn_intro #X #H #H2
fact csn_appl_theta_aux: ∀L,U. L ⊢ ⬇* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
∀V,T. U = ⓓV. ⓐV2. T → L ⊢ ⬇* ⓐV1. ⓓV. T.
-#L #X #H @(csn_ind_cprs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+#L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
lapply (csn_fwd_pair_sn … HVT) #HV
lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
@csn_intro #X #HL #H
(* Properties about atomic arity assignment on terms ************************)
-lemma aaa_lcprs_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ÷ A.
+lemma aaa_lcprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A.
#L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. L ⊢ T ÷ A) … HT ? HL12) /2 width=3/
+@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/
qed.
-lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ÷ A.
+lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A.
#L #T1 #A #HT1 #T2 #HT12
@(TC_Conf3 … HT1 ? HT12) /2 width=3/
qed.
-lemma aaa_lcprs_cprs_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡* L2 →
- ∀T2. L2 ⊢ T1 ➡* T2 → L2 ⊢ T2 ÷ A.
+lemma aaa_lcprs_cprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ⊢ ➡* L2 →
+ ∀T2. L2 ⊢ T1 ➡* T2 → L2 ⊢ T2 ⁝ A.
/3 width=3/ qed.
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_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ÷ A →
+| lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ⁝ A →
lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW)
.
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 &
+ ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A &
K1 [RP] ⊑ K2 &
L2 = K2. ⓛW & I = Abbr.
#RP #L1 #L2 * -L1 -L2
(* 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 &
+ ∃∃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_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,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A &
K1 [RP] ⊑ K2 &
L1 = K1. ⓓV & I = Abst.
#RP #L1 #L2 * -L1 -L2
(* 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,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ⁝ A &
K1 [RP] ⊑ K2 &
L1 = K1. ⓓV & I = Abst.
/2 width=3/ qed-.
(* properties concerning lenv refinement for atomic arity assignment ********)
lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
- ∀L1,L2. L1 ÷⊑ L2 → L1 [RP] ⊑ L2.
+ ∀L1,L2. L1 ⁝⊑ L2 → L1 [RP] ⊑ L2.
#RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2
// /2 width=1/ /3 width=4/
qed.
(* Main properties about atomic arity assignment on terms *******************)
theorem aaa_lcpcs_mono: ∀L1,L2. L1 ⊢ ⬌* L2 →
- ∀T,A1. L1 ⊢ T ÷ A1 → ∀A2. L2 ⊢ T ÷ A2 →
+ ∀T,A1. L1 ⊢ T ⁝ A1 → ∀A2. L2 ⊢ T ⁝ A2 →
A1 = A2.
#L1 #L2 #HL12 #T #A1 #HT1 #A2 #HT2
elim (lcpcs_inv_lcprs … HL12) -HL12 #L #HL1 #HL2
qed-.
theorem aaa_cpcs_mono: ∀L,T1,T2. L ⊢ T1 ⬌* T2 →
- ∀A1. L ⊢ T1 ÷ A1 → ∀A2. L ⊢ T2 ÷ A2 →
+ ∀A1. L ⊢ T1 ⁝ A1 → ∀A2. L ⊢ T2 ⁝ A2 →
A1 = A2.
#L #T1 #T2 #HT12 #A1 #HA1 #A2 #HA2
elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
(* Static typing ************************************************************)
-notation "hvbox( L ⊢ break term 46 T ÷ break term 46 A )"
+notation "hvbox( L ⊢ break term 46 T ⁝ break term 46 A )"
non associative with precedence 45
for @{ 'AtomicArity $L $T $A }.
-notation "hvbox( T1 ÷ ⊑ break term 46 T2 )"
+notation "hvbox( T1 ⁝ ⊑ break term 46 T2 )"
non associative with precedence 45
for @{ 'CrSubEqA $T1 $T2 }.
+notation "hvbox( L ⊢ break term 46 T ÷ break term 46 A )"
+ non associative with precedence 45
+ for @{ 'BinaryArity $L $T $A }.
+
+notation "hvbox( T1 ÷ ⊑ break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqB $T1 $T2 }.
+
notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 • break term 46 T2 )"
non associative with precedence 45
for @{ 'StaticType $h $L $T1 $T2 }.
non associative with precedence 45
for @{ 'SN $L $T }.
-notation "hvbox( L ⊢ ⬇ * * term 46 T )"
+notation "hvbox( L ⊢ ⬇ ⬇ * term 46 T )"
non associative with precedence 45
- for @{ 'SNStar $L $T }.
+ for @{ 'SNAlt $L $T }.
notation "hvbox( ⦃ L, break T ⦄ break [ R ] ϵ break 〚 A 〛 )"
non associative with precedence 45
(* Properties about atomic arity assignment on terms ************************)
-lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ÷ A.
+lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ⁝ A.
#L1 #T #A #HT #L2 * /3 width=5/
qed.
-lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ÷ A.
+lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ⁝ A.
#L #T1 #A #HT1 #T2 * /3 width=5/
qed.
-lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡ L2 →
- ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ⊢ ➡ L2 →
+ ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
/3 width=3/ qed.
(* Properties about atomic arity assignment on terms ************************)
-fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ÷ A → L = L1 → T = T1 →
- ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+fact aaa_ltpr_tpr_conf_aux: ∀L,T,L1,T1,A. L1 ⊢ T1 ⁝ A → L = L1 → T = T1 →
+ ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
#L #T @(cw_wf_ind … L T) -L -T #L #T #IH
#L1 #T1 #A * -L1 -T1 -A
[ -IH #L1 #k #H1 #H2 #L2 #_ #T2 #H destruct
]
qed.
-lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ➡ L2 →
- ∀T2. T1 ➡ T2 → L2 ⊢ T2 ÷ A.
+lemma aaa_ltpr_tpr_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. L1 ➡ L2 →
+ ∀T2. T1 ➡ T2 → L2 ⊢ T2 ⁝ A.
/2 width=9/ qed.
-lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ÷ A.
+lemma aaa_ltpr_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ➡ L2 → L2 ⊢ T ⁝ A.
/2 width=5/ qed.
-lemma aaa_tpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. T1 ➡ T2 → L ⊢ T2 ÷ A.
+lemma aaa_tpr_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. T1 ➡ T2 → L ⊢ T2 ⁝ A.
/2 width=5/ qed.
(* Basic inversion lemmas ***************************************************)
-fact aaa_inv_sort_aux: ∀L,T,A. L ⊢ T ÷ A → ∀k. T = ⋆k → A = ⓪.
+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
]
qed.
-lemma aaa_inv_sort: ∀L,A,k. L ⊢ ⋆k ÷ A → A = ⓪.
+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.
+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/
]
qed.
-lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ÷ A →
- ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A.
+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.
+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
]
qed.
-lemma aaa_inv_abbr: ∀L,V,T,A. L ⊢ ⓓV. T ÷ A →
- ∃∃B. L ⊢ V ÷ B & L. ⓓV ⊢ T ÷ A.
+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.
+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
]
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.
+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.
+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
]
qed.
-lemma aaa_inv_appl: ∀L,V,T,A. L ⊢ ⓐV. T ÷ A →
- ∃∃B. L ⊢ V ÷ B & L ⊢ T ÷ ②B. A.
+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.
+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
]
qed.
-lemma aaa_inv_cast: ∀L,W,T,A. L ⊢ ⓣW. T ÷ A →
- L ⊢ W ÷ A ∧ L ⊢ T ÷ A.
+lemma aaa_inv_cast: ∀L,W,T,A. L ⊢ ⓣW. T ⁝ A →
+ L ⊢ W ⁝ A ∧ L ⊢ T ⁝ A.
/2 width=3/ qed-.
(* Main properties **********************************************************)
-theorem aaa_mono: ∀L,T,A1. L ⊢ T ÷ A1 → ∀A2. L ⊢ T ÷ A2 → A1 = A2.
+theorem aaa_mono: ∀L,T,A1. L ⊢ T ⁝ A1 → ∀A2. L ⊢ T ⁝ A2 → A1 = A2.
#L #T #A1 #H elim H -L -T -A1
[ #L #k #A2 #H
>(aaa_inv_sort … H) -H //
(* Properties concerning basic relocation ***********************************)
-lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T2. ⇧[d, e] T1 ≡ T2 → L2 ⊢ T2 ÷ A.
+lemma aaa_lift: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T2. ⇧[d, e] T1 ≡ T2 → L2 ⊢ T2 ⁝ A.
#L1 #T1 #A #H elim H -L1 -T1 -A
[ #L1 #k #L2 #d #e #_ #T2 #H
>(lift_inv_sort1 … H) -H //
]
qed.
-lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ÷ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
- ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ÷ A.
+lemma aaa_inv_lift: ∀L2,T2,A. L2 ⊢ T2 ⁝ A → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+ ∀T1. ⇧[d, e] T1 ≡ T2 → L1 ⊢ T1 ⁝ A.
#L2 #T2 #A #H elim H -L2 -T2 -A
[ #L2 #k #L1 #d #e #_ #T1 #H
>(lift_inv_sort2 … H) -H //
(* Properties concerning generic relocation *********************************)
lemma aaa_lifts: ∀L1,L2,T2,A,des. ⇩*[des] L2 ≡ L1 → ∀T1. ⇧*[des] T1 ≡ T2 →
- L1 ⊢ T1 ÷ A → L2 ⊢ T2 ÷ A.
+ L1 ⊢ T1 ⁝ A → L2 ⊢ T2 ⁝ A.
#L1 #L2 #T2 #A #des #H elim H -L1 -L2 -des
[ #L #T1 #H #HT1
<(lifts_inv_nil … H) -H //
(* Properties about parallel unfold *****************************************)
(* Note: lemma 500 *)
-lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
- ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ÷ A.
+lemma aaa_ltpss_tpss_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
+ ∀T2. L2 ⊢ T1 [d, e] ▶* T2 → L2 ⊢ T2 ⁝ A.
#L1 #T1 #A #H elim H -L1 -T1 -A
[ #L1 #k #L2 #d #e #_ #T2 #H
>(tpss_inv_sort1 … H) -H //
]
qed.
-lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
- ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ÷ A.
+lemma aaa_ltpss_tps_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2,d,e. L1 [d, e] ▶* L2 →
+ ∀T2. L2 ⊢ T1 [d, e] ▶ T2 → L2 ⊢ T2 ⁝ A.
/3 width=7/ qed.
-lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ÷ A →
- ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ÷ A.
+lemma aaa_ltpss_conf: ∀L1,T,A. L1 ⊢ T ⁝ A →
+ ∀L2,d,e. L1 [d, e] ▶* L2 → L2 ⊢ T ⁝ A.
/2 width=7/ qed.
-lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ÷ A →
- ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ÷ A.
+lemma aaa_tpss_conf: ∀L,T1,A. L ⊢ T1 ⁝ A →
+ ∀T2,d,e. L ⊢ T1 [d, e] ▶* T2 → L ⊢ T2 ⁝ A.
/2 width=7/ qed.
-lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ÷ A →
- ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ÷ A.
+lemma aaa_tps_conf: ∀L,T1,A. L ⊢ T1 ⁝ A →
+ ∀T2,d,e. L ⊢ T1 [d, e] ▶ T2 → L ⊢ T2 ⁝ A.
/2 width=7/ 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_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ÷ A → L2 ⊢ W ÷ A →
+| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ⁝ A → L2 ⊢ W ⁝ A →
lsuba L1 L2 → lsuba (L1. ⓓV) (L2. ⓛW)
.
(* Basic inversion lemmas ***************************************************)
-fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ÷⊑ L2 → L1 = ⋆ → L2 = ⋆.
+fact lsuba_inv_atom1_aux: ∀L1,L2. L1 ⁝⊑ L2 → L1 = ⋆ → L2 = ⋆.
#L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed.
-lemma lsuba_inv_atom1: ∀L2. ⋆ ÷⊑ L2 → L2 = ⋆.
+lemma lsuba_inv_atom1: ∀L2. ⋆ ⁝⊑ L2 → L2 = ⋆.
/2 width=3/ qed-.
-fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
- (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
+fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
+ (∃∃K2. K1 ⁝⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
L2 = K2. ⓛW & I = Abbr.
#L1 #L2 * -L1 -L2
[ #I #K1 #V #H destruct
]
qed.
-lemma lsuba_inv_pair1: ∀I,K1,L2,V. K1. ⓑ{I} V ÷⊑ L2 →
- (∃∃K2. K1 ÷⊑ K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
+lemma lsuba_inv_pair1: ∀I,K1,L2,V. K1. ⓑ{I} V ⁝⊑ L2 →
+ (∃∃K2. K1 ⁝⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+ ∃∃K2,W,A. K1 ⊢ V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
L2 = K2. ⓛW & I = Abbr.
/2 width=3/ qed-.
-fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ÷⊑ L2 → L2 = ⋆ → L1 = ⋆.
+fact lsuba_inv_atom2_aux: ∀L1,L2. L1 ⁝⊑ L2 → L2 = ⋆ → L1 = ⋆.
#L1 #L2 * -L1 -L2
[ //
| #I #L1 #L2 #V #_ #H destruct
]
qed.
-lemma lsubc_inv_atom2: ∀L1. L1 ÷⊑ ⋆ → L1 = ⋆.
+lemma lsubc_inv_atom2: ∀L1. L1 ⁝⊑ ⋆ → L1 = ⋆.
/2 width=3/ qed-.
-fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
- (∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨
- ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
+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. ⓓV & I = Abst.
#L1 #L2 * -L1 -L2
[ #I #K2 #W #H destruct
]
qed.
-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 &
+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. ⓓV & I = Abst.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
-lemma lsuba_refl: ∀L. L ÷⊑ L.
+lemma lsuba_refl: ∀L. L ⁝⊑ L.
#L elim L -L // /2 width=1/
qed.
(* Properties concerning atomic arity assignment ****************************)
-lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ÷ A → ∀L2. L1 ÷⊑ L2 → L2 ⊢ V ÷ A.
+lemma lsuba_aaa_conf: ∀L1,V,A. L1 ⊢ V ⁝ A → ∀L2. L1 ⁝⊑ L2 → L2 ⊢ V ⁝ A.
#L1 #V #A #H elim H -L1 -V -A
[ //
| #I #L1 #K1 #V1 #B #i #HLK1 #HV1B #IHV1 #L2 #HL12
]
qed.
-lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ÷ A → ∀L1. L1 ÷⊑ L2 → L1 ⊢ V ÷ A.
+lemma lsuba_aaa_trans: ∀L2,V,A. L2 ⊢ V ⁝ A → ∀L1. L1 ⁝⊑ L2 → L1 ⊢ V ⁝ A.
#L2 #V #A #H elim H -L2 -V -A
[ //
| #I #L2 #K2 #V2 #B #i #HLK2 #HV2B #IHV2 #L1 #HL12
(* Note: the constant 0 cannot be generalized *)
-lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ÷⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
- ∃∃K2. K1 ÷⊑ K2 & ⇩[0, e] L2 ≡ K2.
+lemma lsuba_ldrop_O1_conf: ∀L1,L2. L1 ⁝⊑ L2 → ∀K1,e. ⇩[0, e] L1 ≡ K1 →
+ ∃∃K2. K1 ⁝⊑ K2 & ⇩[0, e] L2 ≡ K2.
#L1 #L2 #H elim H -L1 -L2
[ /2 width=3/
| #I #L1 #L2 #V #_ #IHL12 #K1 #e #H
]
qed-.
-lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ÷⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
- ∃∃K1. K1 ÷⊑ K2 & ⇩[0, e] L1 ≡ K1.
+lemma lsuba_ldrop_O1_trans: ∀L1,L2. L1 ⁝⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+ ∃∃K1. K1 ⁝⊑ K2 & ⇩[0, e] L1 ≡ K1.
#L1 #L2 #H elim H -L1 -L2
[ /2 width=3/
| #I #L1 #L2 #V #_ #IHL12 #K2 #e #H
(* Main properties **********************************************************)
-theorem lsuba_trans: ∀L1,L. L1 ÷⊑ L → ∀L2. L ÷⊑ L2 → L1 ÷⊑ L2.
+theorem lsuba_trans: ∀L1,L. L1 ⁝⊑ L → ∀L2. L ⁝⊑ L2 → L1 ⁝⊑ L2.
#L1 #L #H elim H -L1 -L
[ #X #H >(lsuba_inv_atom1 … H) -H //
| #I #L1 #L #V #HL1 #IHL1 #X #H
;;
let predefined_classes = [
+ [":"; "⁝"; ];
["."; "•"; "◦"; ];
["#"; "⌘"; ];
["-"; "÷"; "⊢"; ];
projects / helm.git / commitdiff