(* 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 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr 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: â\88\80I,V1,V2,T1,T2. V1 â\87\92 V2 â\86\92 T1 â\87\92 T2 →
- 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+lemma tpr_bind: â\88\80I,V1,V2,T1,T2. V1 â\9e¡ V2 â\86\92 T1 â\9e¡ T2 →
+ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
-lemma tpr_refl: â\88\80T. T â\87\92 T.
+lemma tpr_refl: â\88\80T. T â\9e¡ T.
#T elim T -T //
#I elim I -I /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
-fact tpr_inv_atom1_aux: â\88\80U1,U2. U1 â\87\92 U2 â\86\92 â\88\80I. U1 = ð\9d\95\92{I} â\86\92 U2 = ð\9d\95\92{I}.
+fact tpr_inv_atom1_aux: â\88\80U1,U2. U1 â\9e¡ U2 â\86\92 â\88\80I. U1 = â\93ª{I} â\86\92 U2 = â\93ª{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: â\88\80U1,U2. U1 â\87\92 U2 â\86\92 â\88\80I,V1,T1. U1 = ð\9d\95\93{I} V1. T1 →
- (â\88\83â\88\83V2,T2,T. V1 â\87\92 V2 & T1 â\87\92 T2 &
- ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕓{I} V2. T
+fact tpr_inv_bind1_aux: â\88\80U1,U2. U1 â\9e¡ U2 â\86\92 â\88\80I,V1,T1. U1 = â\93\91{I} V1. T1 →
+ (â\88\83â\88\83V2,T2,T. V1 â\9e¡ V2 & T1 â\9e¡ T2 &
+ ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ U2 = ⓑ{I} V2. T
) ∨
- â\88\83â\88\83T. â\87\91[0,1] T â\89¡ T1 & T â\87\92 U2 & I = Abbr.
+ â\88\83â\88\83T. â\87§[0,1] T â\89¡ T1 & T â\9e¡ U2 & I = Abbr.
#U1 #U2 * -U1 -U2
[ #J #I #V #T #H destruct
| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
]
qed.
-lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
- (â\88\83â\88\83V2,T2,T. V1 â\87\92 V2 & T1 â\87\92 T2 &
- ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕓{I} V2. T
+lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
+ (â\88\83â\88\83V2,T2,T. V1 â\9e¡ V2 & T1 â\9e¡ T2 &
+ ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+ U2 = ⓑ{I} V2. T
) ∨
- â\88\83â\88\83T. â\87\91[0,1] T â\89¡ T1 & T â\87\92 U2 & I = Abbr.
+ â\88\83â\88\83T. â\87§[0,1] T â\89¡ T1 & T â\9e¡ U2 & I = Abbr.
/2 width=3/ qed-.
(* Basic_1: was pr0_gen_abbr *)
-lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
- (â\88\83â\88\83V2,T2,T. V1 â\87\92 V2 & T1 â\87\92 T2 &
- ⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕓{Abbr} V2. T
+lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
+ (â\88\83â\88\83V2,T2,T. V1 â\9e¡ V2 & T1 â\9e¡ T2 &
+ ⋆. ⓓV2 ⊢ T2 [0, 1] ▶ T &
+ U2 = ⓓV2. T
) ∨
- â\88\83â\88\83T. â\87\91[0,1] T â\89¡ T1 & T â\87\92 U2.
+ â\88\83â\88\83T. â\87§[0,1] T â\89¡ T1 & T â\9e¡ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 … H) -H * /3 width=7/
qed-.
-fact tpr_inv_flat1_aux: â\88\80U1,U2. U1 â\87\92 U2 â\86\92 â\88\80I,V1,U0. U1 = ð\9d\95\97{I} V1. U0 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. V1 â\87\92 V2 & U0 â\87\92 T2 &
- U2 = 𝕗{I} V2. T2
- | â\88\83â\88\83V2,W,T1,T2. V1 â\87\92 V2 & T1 â\87\92 T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2 & I = Appl
- | â\88\83â\88\83V2,V,W1,W2,T1,T2. V1 â\87\92 V2 & W1 â\87\92 W2 & T1 â\87\92 T2 &
- â\87\91[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+fact tpr_inv_flat1_aux: â\88\80U1,U2. U1 â\9e¡ U2 â\86\92 â\88\80I,V1,U0. U1 = â\93\95{I} V1. U0 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & U0 â\9e¡ T2 &
+ U2 = ⓕ{I} V2. T2
+ | â\88\83â\88\83V2,W,T1,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 &
+ U0 = ⓛW. T1 &
+ U2 = ⓓV2. T2 & I = Appl
+ | â\88\83â\88\83V2,V,W1,W2,T1,T2. V1 â\9e¡ V2 & W1 â\9e¡ W2 & T1 â\9e¡ T2 &
+ â\87§[0,1] V2 ≡ V &
+ U0 = ⓓW1. T1 &
+ U2 = ⓓW2. ⓐV. T2 &
I = Appl
- | (U0 â\87\92 U2 ∧ I = Cast).
+ | (U0 â\9e¡ U2 ∧ I = Cast).
#U1 #U2 * -U1 -U2
[ #I #J #V #T #H destruct
| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
]
qed.
-lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. V1 â\87\92 V2 & U0 â\87\92 T2 &
- U2 = 𝕗{I} V2. T2
- | â\88\83â\88\83V2,W,T1,T2. V1 â\87\92 V2 & T1 â\87\92 T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2 & I = Appl
- | â\88\83â\88\83V2,V,W1,W2,T1,T2. V1 â\87\92 V2 & W1 â\87\92 W2 & T1 â\87\92 T2 &
- â\87\91[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+lemma tpr_inv_flat1: ∀V1,U0,U2,I. ⓕ{I} V1. U0 ➡ U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & U0 â\9e¡ T2 &
+ U2 = ⓕ{I} V2. T2
+ | â\88\83â\88\83V2,W,T1,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 &
+ U0 = ⓛW. T1 &
+ U2 = ⓓV2. T2 & I = Appl
+ | â\88\83â\88\83V2,V,W1,W2,T1,T2. V1 â\9e¡ V2 & W1 â\9e¡ W2 & T1 â\9e¡ T2 &
+ â\87§[0,1] V2 ≡ V &
+ U0 = ⓓW1. T1 &
+ U2 = ⓓW2. ⓐV. T2 &
I = Appl
- | (U0 â\87\92 U2 ∧ I = Cast).
+ | (U0 â\9e¡ U2 ∧ I = Cast).
/2 width=3/ qed-.
(* Basic_1: was pr0_gen_appl *)
-lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. V1 â\87\92 V2 & U0 â\87\92 T2 &
- U2 = 𝕔{Appl} V2. T2
- | â\88\83â\88\83V2,W,T1,T2. V1 â\87\92 V2 & T1 â\87\92 T2 &
- U0 = 𝕔{Abst} W. T1 &
- U2 = 𝕔{Abbr} V2. T2
- | â\88\83â\88\83V2,V,W1,W2,T1,T2. V1 â\87\92 V2 & W1 â\87\92 W2 & T1 â\87\92 T2 &
- â\87\91[0,1] V2 ≡ V &
- U0 = 𝕔{Abbr} W1. T1 &
- U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
+lemma tpr_inv_appl1: ∀V1,U0,U2. ⓐV1. U0 ➡ U2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & U0 â\9e¡ T2 &
+ U2 = ⓐV2. T2
+ | â\88\83â\88\83V2,W,T1,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 &
+ U0 = ⓛW. T1 &
+ U2 = ⓓV2. T2
+ | â\88\83â\88\83V2,V,W1,W2,T1,T2. V1 â\9e¡ V2 & W1 â\9e¡ W2 & T1 â\9e¡ T2 &
+ â\87§[0,1] V2 ≡ V &
+ 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] →
- â\88\83â\88\83V2,T2. V1 â\87\92 V2 & T1 â\87\92 T2 &
- U = 𝕔{Appl} V2. T2.
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝕊[T1] →
+ â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ 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 →
- (â\88\83â\88\83V2,T2. V1 â\87\92 V2 & T1 â\87\92 T2 & U2 = ð\9d\95\94{Cast} V2. T2)
- â\88¨ T1 â\87\92 U2.
+lemma tpr_inv_cast1: ∀V1,T1,U2. ⓣV1. T1 ➡ U2 →
+ (â\88\83â\88\83V2,T2. V1 â\9e¡ V2 & T1 â\9e¡ T2 & U2 = â\93£V2. T2)
+ â\88¨ T1 â\9e¡ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_flat1 … H) -H * /3 width=5/
[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
]
qed-.
-fact tpr_inv_lref2_aux: â\88\80T1,T2. T1 â\87\92 T2 → ∀i. T2 = #i →
+fact tpr_inv_lref2_aux: â\88\80T1,T2. T1 â\9e¡ T2 → ∀i. T2 = #i →
∨∨ T1 = #i
- | â\88\83â\88\83V,T,T0. â\87\91[O,1] T0 â\89¡ T & T0 â\87\92 #i &
- T1 = 𝕔{Abbr} V. T
- | â\88\83â\88\83V,T. T â\87\92 #i & T1 = ð\9d\95\94{Cast} V. T.
+ | â\88\83â\88\83V,T,T0. â\87§[O,1] T0 â\89¡ T & T0 â\9e¡ #i &
+ T1 = ⓓV. T
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
#T1 #T2 * -T1 -T2
[ #I #i #H destruct /2 width=1/
| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
]
qed.
-lemma tpr_inv_lref2: â\88\80T1,i. T1 â\87\92 #i →
+lemma tpr_inv_lref2: â\88\80T1,i. T1 â\9e¡ #i →
∨∨ T1 = #i
- | â\88\83â\88\83V,T,T0. â\87\91[O,1] T0 â\89¡ T & T0 â\87\92 #i &
- T1 = 𝕔{Abbr} V. T
- | â\88\83â\88\83V,T. T â\87\92 #i & T1 = ð\9d\95\94{Cast} V. T.
+ | â\88\83â\88\83V,T,T0. â\87§[O,1] T0 â\89¡ T & T0 â\9e¡ #i &
+ T1 = ⓓV. T
+ | â\88\83â\88\83V,T. T â\9e¡ #i & T1 = â\93£V. T.
/2 width=3/ qed-.
(* Basic_1: removed theorems 3: