pr1/props pr1_comp
pr1/props pr1_eta
pr2/clen pr2_gen_ctail
-pr2/subst1 pr2_gen_cabbr
-
-# check ######################################################################
-
pr2/fwd pr2_gen_void
pr2/props pr2_ctail
-
-# waiting ####################################################################
-
+pr2/subst1 pr2_gen_cabbr
pr3/fwd pr3_gen_sort
pr3/fwd pr3_gen_abst
pr3/fwd pr3_gen_cast
sty1/props sty1_correct
sty1/props sty1_abbr
sty1/props sty1_cast2
-subst0/dec dnf_dec2
-subst0/dec dnf_dec
-subst1/props subst1_ex
subst/fwd subst_sort
subst/fwd subst_lref_lt
subst/fwd subst_lref_eq
subst/fwd subst_head
subst/props subst_lift_SO
subst/props subst_subst0
-T/dec bind_dec_not
T/dec binder_dec
T/dec abst_dec
tlist/props tslt_wf__q_ind
tlist/props theads_tapp
tlist/props tcons_tapp_ex
tlist/props tlist_ind_rev
-T/props not_abbr_abst
-T/props not_void_abst
-T/props not_abbr_void
-T/props not_abst_void
-T/props tweight_lt
ty3/arity ty3_arity
ty3/arity_props ty3_predicative
ty3/arity_props ty3_repellent
wf3/ty3 wf3_pr3_conf
wf3/ty3 wf3_pc3_conf
wf3/ty3 wf3_ty3_conf
+
+# check ######################################################################
(* Basic_1: was: kind_dec *)
axiom item2_eq_dec: ∀I1,I2:item2. Decidable (I1 = I2).
-(* Basic_1: removed theorems 19:
+(* Basic_1: removed theorems 21:
s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc
s_arith0 s_arith1
r_S r_plus r_plus_sym r_minus r_dis s_r r_arith0 r_arith1
+ not_abbr_abst bind_dec_not
*)
]
qed.
-lemma lsubs_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
- L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
+lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
+ L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
#L1 #L2 #e #HL12 #I #V elim I -I /2/
qed.
qed.
lemma lsubs_fwd_length_full1: ∀L1,L2. L1 [0, |L1|] ≼ L2 → |L1| ≤ |L2|.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact lsubs_fwd_length_full2_aux: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
d = 0 → e = |L2| → |L2| ≤ |L1|.
qed.
lemma lsubs_fwd_length_full2: ∀L1,L2. L1 [0, |L2|] ≼ L2 → |L2| ≤ |L1|.
-/2 width=5/ qed.
+/2 width=5/ qed-.
(generalize in match e1) -e1 >e0 normalize
*) -I /2/ (**) (* destruct: one quality is not simplified, the destucted equality is not erased *)
]
-qed.
+qed-.
(* Basic_1: was: thead_x_y_y *)
lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False.
[ #J #H destruct
| #J #W #U #_ #IHU #H destruct -I V /2/ (**) (* destruct: the destucted equality is not erased *)
]
-qed.
+qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: term_dec *)
axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2).
+
+(* Basic_1: removed theorems 3:
+ not_void_abst not_abbr_void not_abst_void
+*)
qed.
lemma simple_inv_bind: ∀I,V,T. 𝕊[𝕓{I} V. T] → False.
-/2 width=6/ qed.
+/2 width=6/ qed-.
(* Basic properties *********************************************************)
+(* Basic_1: was: tweight_lt *)
lemma tw_pos: ∀T. 1 ≤ #[T].
#T elim T -T /2/
qed.
#T1 #T2 #H elim H -H T1 T2 //
#V1 #V2 #T1 #T2 #H
elim (simple_inv_bind … H)
-qed.
+qed. (**) (* remove from index *)
lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1].
-/3/ qed.
+/3/ qed-.
(* Basic inversion lemmas ***************************************************)
non associative with precedence 45
for @{ 'PSubstStar $L $T1 $d $e $T2 }.
+notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )"
+ non associative with precedence 45
+ for @{ 'TSubst $L $T1 $d $e $T2 }.
+
(* Reducibility *************************************************************)
notation "hvbox( ℝ [ T ] )"
lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
#T1 #T2 * #T #HT normalize #HT2
<(tpss_inv_refl_O2 … HT2) -HT2 //
-qed.
+qed-.
(* Basic_1: was: pr2_gen_sort *)
lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k.
#L #T2 #k * #X #H
>(tpr_inv_atom1 … H) -H #H
>(tpss_inv_sort1 … H) -H //
-qed.
+qed-.
(* Basic_1: was: pr2_gen_cast *)
lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ⇒ U2 → (
elim (tpr_inv_cast1 … H) -H /3/
* #V #T #HV1 #HT1 #H destruct -X;
elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct -U2 /4 width=5/
-qed.
+qed-.
(* Basic_1: removed theorems 5:
pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
#L elim L -L
-[ /2/
-| normalize /3/
+[ #T1 #T2 #HT12 @(cpr_inv_atom … HT12)
+| normalize /3 width=1/
].
-qed.
+qed-.
(* Main properties **********************************************************)
elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/
qed.
-
↓[0, i] L ≡ K. 𝕓{Abbr} 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
-@ex2_1_intro [2: // | skip | @tpss_subst /2 width=6/ ] (**) (* /4 width=6/ is too slow *)
+lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
+@ex2_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *)
qed.
(* Advanced inversion lemmas ************************************************)
>(tpr_inv_atom1 … H) -H #H
elim (tpss_inv_lref1 … H) -H /2/
* /3 width=6/
-qed.
+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.
-/2/ qed.
+/2/ qed-.
(* Relocation properties ****************************************************)
(* Basic_1: was: wcpr0_gen_sort *)
lemma ltpr_inv_atom1: ∀L2. ⋆ ⇒ L2 → L2 = ⋆.
-/2/ qed.
+/2/ 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.
(* 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.
-/2/ qed.
+/2/ qed-.
fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ⇒ L2 → L2 = ⋆ → L1 = ⋆.
#L1 #L2 * -L1 L2
qed.
lemma ltpr_inv_atom2: ∀L1. L1 ⇒ ⋆ → L1 = ⋆.
-/2/ qed.
+/2/ 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.
lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ⇒ K2. 𝕓{I} V2 →
∃∃K1,V1. K1 ⇒ K2 & V1 ⇒ V2 & L1 = K1. 𝕓{I} V1.
-/2/ qed.
+/2/ qed-.
(* Basic forward lemmas *****************************************************)
lemma ltpr_fwd_length: ∀L1,L2. L1 ⇒ L2 → |L1| = |L2|.
#L1 #L2 #H elim H -H L1 L2; normalize //
-qed.
+qed-.
(* Basic_1: removed theorems 2: wcpr0_getl wcpr0_getl_back *)
(* Basic_1: was: wcpr0_ldrop *)
lemma ltpr_ldrop_conf: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀L2. L1 ⇒ L2 →
- ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2.
+ ∃∃K2. ↓[d, e] L2 ≡ K2 & K1 ⇒ K2.
#L1 #K1 #d #e #H elim H -H L1 K1 d e
[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
| #K1 #I #V1 #X #H
(* Basic_1: was: wcpr0_ldrop_back *)
lemma ltpr_ldrop_trans: ∀L1,K1,d,e. ↓[d, e] L1 ≡ K1 → ∀K2. K1 ⇒ K2 →
- ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2.
+ ∃∃L2. ↓[d, e] L2 ≡ K2 & L1 ⇒ L2.
#L1 #K1 #d #e #H elim H -H L1 K1 d e
[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2/
| #K1 #I #V1 #X #H
[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2/ -HV2 #H destruct -V1 T1 //
| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2/ -HT2 #H destruct -V1 T1 //
]
-qed.
+qed-.
lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
#V1 #T1 #HVT1 @and3_intro
lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2/ -HV12 #H destruct
| lapply (H (𝕔{Abbr}V1.U1) ?) -H /2/ #H destruct
]
+qed-.
+
+lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
+#V #T #H elim (is_lift_dec T 0 1)
+[ * #U #HTU
+ lapply (H U ?) -H /2 width=3/ #H destruct -U;
+ 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/ -HT2 #H destruct -T /3 width=2/
+]
qed.
-axiom tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
-
lemma tnf_inv_cast: ∀V,T. ℕ[𝕔{Cast}V.T] → False.
-#V #T #H lapply (H T ?) -H /2/
-qed.
+#V #T #H lapply (H T ?) -H /2 width=1/ #H
+@(discr_tpair_xy_y … H)
+qed-.
(* Basic properties *********************************************************)
(* *)
(**************************************************************************)
+include "Basic_2/grammar/term_simple.ma".
include "Basic_2/substitution/tps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* 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/ qed.
(* Basic_1: was by definition: pr0_refl *)
(* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
-/2/ qed.
+/2/ qed-.
fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
(∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
U2 = 𝕓{I} V2. T
) ∨
∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
-/2/ qed.
+/2/ qed-.
(* Basic_1: was pr0_gen_abbr *)
lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 … H) -H * /3 width=7/
-qed.
+qed-.
fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 →
∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
I = Appl
| (U0 ⇒ U2 ∧ I = Cast).
-/2/ qed.
+/2/ qed-.
(* Basic_1: was pr0_gen_appl *)
lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
#V1 #U0 #U2 #H
elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
-qed.
+qed-.
+
+(* Note: the main property of simple terms *)
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ⇒ U → 𝕊[T1] →
+ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 &
+ U = 𝕔{Appl} V2. T2.
+#V1 #T1 #U #H #HT1
+elim (tpr_inv_appl1 … H) -H *
+[ /2 width=5/
+| #V2 #W #W1 #W2 #_ #_ #H #_ destruct -T1;
+ elim (simple_inv_bind … HT1)
+| #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct -T1;
+ elim (simple_inv_bind … HT1)
+]
+qed-.
(* Basic_1: was: pr0_gen_cast *)
lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
[ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
| #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
]
-qed.
+qed-.
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.
-/2/ qed.
+/2/ qed-.
(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
(* 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.
-/2/ qed.
+/2/ qed-.
qed.
lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
-/2/ qed.
+/2/ qed-.
fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
#W #U #T * -T
qed.
lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
-/2/ qed.
+/2/ qed-.
fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T = 𝕔{Appl} W. U →
∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
qed.
lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
-/2/ qed.
+/2/ qed-.
lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
-/2/ qed.
+/2/ qed-.
lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
-/4/ qed.
+/4/ qed-.
lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
#V #T #HVT @and3_intro /3/
generalize in match HVT -HVT; elim T -T //
* // * #U #T #_ #_ #H elim (H ?) -H /2/
-qed.
+qed-.
lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
-/2/ qed.
+/2/ qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: ldrop_gen_refl *)
lemma ldrop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ →
L2 = ⋆.
(* Basic_1: was: ldrop_gen_sort *)
lemma ldrop_inv_atom1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆.
-/2 width=5/ qed.
+/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 →
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/ qed.
+/2/ qed-.
(* Basic_1: was: ldrop_gen_ldrop *)
lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
#e #K #I #V #L2 #H #He
elim (ldrop_inv_O1 … H) -H * // #H destruct -e;
elim (lt_refl_false … He)
-qed.
+qed-.
fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L2 = K2. 𝕓{I} V2.
-/2/ qed.
+/2/ qed-.
fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
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.
-/2/ qed.
+/2/ 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/
qed.
| @ldrop_ldrop >(plus_minus_m_m e 1) /2/
]
]
-qed.
+qed-.
lemma ldrop_fwd_lw: ∀L1,L2,d,e. ↓[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
#L1 #L2 #d #e #H elim H -H L1 L2 d e // normalize
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
>(tw_lift … HV21) -HV21 /2/
]
-qed.
+qed-.
lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
↓[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|.
| lapply (IHL1 … H) -IHL1 H #HeK1 whd in ⊢ (? ? %) /2/
]
]
-qed.
+qed-.
lemma ldrop_fwd_O1_length: ∀L1,L2,e. ↓[0, e] L1 ≡ L2 → |L2| = |L1| - e.
#L1 elim L1 -L1
>minus_le_minus_minus_comm //
]
]
-qed.
+qed-.
(* Basic_1: removed theorems 49:
ldrop_skip_flat
>(lift_inj … HVT1 … HVT2) -HVT1 HVT2
>(IHLK1 … HLK2) -IHLK1 HLK2 //
]
-qed.
+qed-.
(* Basic_1: was: ldrop_conf_ge *)
theorem ldrop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2).
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: lift_lref_gt *)
-lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i.
-#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3/
-qed.
-
-(* Basic_1: was: lift_r *)
-lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T.
-#T elim T -T
-[ * #i // #d elim (lt_or_ge i d) /2/
-| * /2/
-]
-qed.
-
-lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
-#T1 elim T1 -T1
-[ * #i /2/ #d #e elim (lt_or_ge i d) /3/
-| * #I #V1 #T1 #IHV1 #IHT1 #d #e
- elim (IHV1 d e) -IHV1 #V2 #HV12
- [ elim (IHT1 (d+1) e) -IHT1 /3/
- | elim (IHT1 d e) -IHT1 /3/
- ]
-]
-qed.
-
-(* Basic_1: was: lift_free (right to left) *)
-lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 → ∀d2,e1.
- d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
- ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2.
-#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
-[ /3/
-| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
- lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/
-| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
- lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
- <(arith_d1 i e2 e1) // /3/
-| /3/
-| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
- elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
- elim (IHT (d2+1) … ? ? He12) /3 width = 5/
-| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
- elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
- elim (IHT d2 … ? ? He12) /3 width = 5/
-]
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #[T1] = #[T2].
-#d #e #T1 #T2 #H elim H -d e T1 T2; normalize //
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
qed.
lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2.
-/2/ qed.
+/2/ qed-.
fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
#d #e #T1 #T2 * -d e T1 T2 //
qed.
lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i →
(i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 →
(i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
-/2/ qed.
+/2/ qed-.
lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i.
#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
elim (lt_refl_false … Hdd)
-qed.
+qed-.
lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e).
#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
elim (lt_refl_false … Hdd)
-qed.
+qed-.
fact lift_inv_gref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T1 = §p → T2 = §p.
#d #e #T1 #T2 * -d e T1 T2 //
qed.
lemma lift_inv_gref1: ∀d,e,T2,p. ↑[d,e] §p ≡ T2 → T2 = §p.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
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.
-/2/ qed.
+/2/ qed-.
fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
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.
-/2/ qed.
+/2/ qed-.
fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
#d #e #T1 #T2 * -d e T1 T2 //
(* Basic_1: was: lift_gen_sort *)
lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
(i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
(* Basic_1: was: lift_gen_lref *)
lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
(i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
-/2/ qed.
+/2/ qed-.
(* Basic_1: was: lift_gen_lref_lt *)
lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i.
#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
elim (plus_lt_false … Hdd)
-qed.
+qed-.
(* Basic_1: was: lift_gen_lref_false *)
+lemma lift_inv_lref2_be: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
+ d ≤ i → i < d + e → False.
+#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H *
+[ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ]
+lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
+elim (lt_refl_false … H)
+qed-.
(* Basic_1: was: lift_gen_lref_ge *)
lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e).
#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
elim (plus_lt_false … Hdd)
-qed.
+qed-.
fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p.
#d #e #T1 #T2 * -d e T1 T2 //
qed.
lemma lift_inv_gref2: ∀d,e,T1,p. ↑[d,e] T1 ≡ §p → T1 = §p.
-/2 width=5/ qed.
+/2 width=5/ qed-.
fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
∀I,V2,U2. T2 = 𝕓{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.
-/2/ qed.
+/2/ qed-.
fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
∀I,V2,U2. T2 = 𝕗{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.
-/2/ qed.
+/2/ qed-.
+
+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
+ | elim (lift_inv_lref2 … H) -H * #_ #H destruct
+ | lapply (lift_inv_gref2 … H) -H #H destruct
+ ]
+| * #I #W2 #U2 #IHW2 #_ #T #H
+ [ elim (lift_inv_bind2 … H) -H #W1 #U1 #HW12 #_ #H destruct -J T W1 /2/
+ | elim (lift_inv_flat2 … H) -H #W1 #U1 #HW12 #_ #H destruct -J T W1 /2/
+ ]
+]
+qed-.
+
+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
+ | elim (lift_inv_lref2 … H) -H * #_ #H destruct
+ | lapply (lift_inv_gref2 … H) -H #H destruct
+ ]
+| * #I #W2 #U2 #_ #IHU2 #V #d #e #H
+ [ elim (lift_inv_bind2 … H) -H #W1 #U1 #_ #HU12 #H destruct -J U1 W1 /2/
+ | elim (lift_inv_flat2 … H) -H #W1 #U1 #_ #HU12 #H destruct -J U1 W1 /2/
+ ]
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #[T1] = #[T2].
+#d #e #T1 #T2 #H elim H -d e T1 T2; normalize //
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: lift_lref_gt *)
+lemma lift_lref_ge_minus: ∀d,e,i. d + e ≤ i → ↑[d, e] #(i - e) ≡ #i.
+#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %) /3 width=2/
+qed.
+
+(* Basic_1: was: lift_r *)
+lemma lift_refl: ∀T,d. ↑[d, 0] T ≡ T.
+#T elim T -T
+[ * #i // #d elim (lt_or_ge i d) /2/
+| * /2/
+]
+qed.
+
+lemma lift_total: ∀T1,d,e. ∃T2. ↑[d,e] T1 ≡ T2.
+#T1 elim T1 -T1
+[ * #i /2/ #d #e elim (lt_or_ge i d) /3/
+| * #I #V1 #T1 #IHV1 #IHT1 #d #e
+ elim (IHV1 d e) -IHV1 #V2 #HV12
+ [ elim (IHT1 (d+1) e) -IHT1 /3/
+ | elim (IHT1 d e) -IHT1 /3/
+ ]
+]
+qed.
+
+(* Basic_1: was: lift_free (right to left) *)
+lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 →
+ ∀d2,e1. d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
+ ∃∃T. ↑[d1, e1] T1 ≡ T & ↑[d2, e2 - e1] T ≡ T2.
+#d1 #e2 #T1 #T2 #H elim H -H d1 e2 T1 T2
+[ /3/
+| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
+ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4/
+| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
+ lapply (transitive_le …(i+e1) Hd21 ?) /2/ -Hd21 #Hd21
+ <(arith_d1 i e2 e1) // /3/
+| /3/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+ elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+ elim (IHT (d2+1) … ? ? He12) /3 width=5/
+| #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
+ elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b
+ elim (IHT d2 … ? ? He12) /3 width=5/
+]
+qed.
+
+(* Basic_1: was only: dnf_dec2 dnf_dec *)
+lemma is_lift_dec: ∀T2,d,e. Decidable (∃T1. ↑[d,e] T1 ≡ T2).
+#T1 elim T1 -T1
+[ * [1,3: /3 width=2/ ] #i #d #e
+ elim (lt_dec i d) #Hid
+ [ /4 width=2/
+ | lapply (false_lt_to_le … Hid) -Hid #Hid
+ elim (lt_dec i (d + e)) #Hide
+ [ @or_intror * #T1 #H
+ elim (lift_inv_lref2_be … H Hid Hide)
+ | lapply (false_lt_to_le … Hide) -Hide /4 width=2/
+ ]
+ ]
+| * #I #V2 #T2 #IHV2 #IHT2 #d #e
+ [ elim (IHV2 d e) -IHV2
+ [ * #V1 #HV12 elim (IHT2 (d+1) e) -IHT2
+ [ * #T1 #HT12 @or_introl /3/
+ | -V1 #HT2 @or_intror * #X #H
+ elim (lift_inv_bind2 … H) -H /3 width=2/
+ ]
+ | -IHT2 #HV2 @or_intror * #X #H
+ elim (lift_inv_bind2 … H) -H /3 width=2/
+ ]
+ | elim (IHV2 d e) -IHV2
+ [ * #V1 #HV12 elim (IHT2 d e) -IHT2
+ [ * #T1 #HT12 /4 width=2/
+ | -V1 #HT2 @or_intror * #X #H
+ elim (lift_inv_flat2 … H) -H /3 width=2/
+ ]
+ | -IHT2 #HV2 @or_intror * #X #H
+ elim (lift_inv_flat2 … H) -H /3 width=2/
+ ]
+ ]
+]
+qed.
(* Basic_1: removed theorems 7:
lift_head lift_gen_head
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
elim (lift_inv_flat2 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
]
-qed.
+qed-.
(* Basic_1: was: lift_gen_lift *)
theorem lift_div_le: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #X #HX
elim (lift_inv_flat1 … HX) -HX #V #T #HV1 #HT1 #HX destruct -X /3/
]
-qed.
+qed-.
(* Basic_1: was: lift_free (left to right) *)
theorem lift_trans_be: ∀d1,e1,T1,T. ↑[d1, e1] T1 ≡ T →
qed.
lemma ltps_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫ L2 → L1 = L2.
-/2/ qed.
+/2/ qed-.
fact ltps_inv_atom1_aux: ∀d,e,L1,L2.
L1 [d, e] ≫ L2 → L1 = ⋆ → L2 = ⋆.
qed.
lemma ltps_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫ L2 → L2 = ⋆.
-/2 width=5/ 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 →
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.
-/2 width=5/ qed.
+/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 →
∃∃K2,V2. K1 [d - 1, e] ≫ K2 &
K2 ⊢ V1 [d - 1, e] ≫ V2 &
L2 = K2. 𝕓{I} V2.
-/2/ qed.
+/2/ qed-.
fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆.
qed.
lemma ltps_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
-/2 width=5/ 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 →
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.
-/2 width=5/ qed.
+/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 →
∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
K2 ⊢ V1 [d - 1, e] ≫ V2 &
L1 = K1. 𝕓{I} V1.
-/2/ qed.
+/2/ qed-.
(* Basic_1: removed theorems 27:
csubst0_clear_O csubst0_ldrop_lt csubst0_ldrop_gt csubst0_ldrop_eq
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
qed.
lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
qed.
lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
qed.
lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
qed.
lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/
| /2/
qed.
lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2/
| /2/
#I elim I -I /2/
qed.
+(* Basic_1: was: subst1_ex *)
+lemma tps_full: ∀K,V,T1,L,d. ↓[0, d] L ≡ (K. 𝕓{Abbr} V) →
+ ∃∃T2,T. L ⊢ T1 [d, 1] ≫ T2 & ↑[d, 1] T ≡ T2.
+#K #V #T1 elim T1 -T1
+[ * #i #L #d #HLK /2/
+ elim (lt_or_eq_or_gt i d) #Hid [ /3/ |3: /3/ ]
+ destruct -d;
+ elim (lift_total V 0 (i+1)) #W #HVW
+ elim (lift_split … HVW i i ? ? ?) // <minus_plus_m_m_comm /3/
+| * #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/ -HLK /3 width=8/
+ | elim (IHU1 … HLK) -IHU1 HLK /3 width=8/
+ ]
+]
+qed.
+
lemma tps_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫ T2 →
∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
L ⊢ T1 [d2, e2] ≫ T2.
↓[O, i] L ≡ K. 𝕓{Abbr} V &
↑[O, i + 1] V ≡ T2 &
I = LRef i.
-/2/ qed.
+/2/ qed-.
(* Basic_1: was: subst1_gen_sort *)
#L #T2 #k #d #e #H
elim (tps_inv_atom1 … H) -H //
* #K #V #i #_ #_ #_ #_ #H destruct
-qed.
+qed-.
(* Basic_1: was: subst1_gen_lref *)
lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫ T2 →
#L #T2 #i #d #e #H
elim (tps_inv_atom1 … H) -H /2/
* #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct -i /3/
-qed.
+qed-.
fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
∀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.
-/2/ qed.
+/2/ qed-.
fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
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.
-/2/ qed.
+/2/ qed-.
fact tps_inv_refl_O2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 0 → T1 = T2.
#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
qed.
lemma tps_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2.
-/2 width=6/ qed.
+/2 width=6/ qed-.
(* Basic forward lemmas *****************************************************)
| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
| /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3/ is too slow *)
]
-qed.
+qed-.
(* Basic_1: removed theorems 25:
subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
-/2 width=8/ qed.
+/2 width=8/ qed-.
(* Relocation properties ****************************************************)
(le d i) -> (lt i (plus d h)) ->
(EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)).
*)
-
lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
(∀L,L2. L1 [d, e] ≫* L → L [d, e] ≫ L2 → R L → R L2) →
∀L2. L1 [d, e] ≫* L2 → R L2.
#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
-qed.
+qed-.
(* Basic properties *********************************************************)
lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫* L2 → L1 = L2.
#d #L1 #L2 #H @(ltpss_ind … H) -L2 //
#L #L2 #_ #HL2 #IHL <(ltps_inv_refl_O2 … HL2) -HL2 //
-qed.
+qed-.
lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫* L2 → L2 = ⋆.
#d #e #L2 #H @(ltpss_ind … H) -L2 //
#L #L2 #_ #HL2 #IHL destruct -L
>(ltps_inv_atom1 … HL2) -HL2 //
-qed.
+qed-.
fact ltpss_inv_atom2_aux: ∀d,e,L1,L2.
L1 [d, e] ≫* L2 → L2 = ⋆ → L1 = ⋆.
qed.
lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ≫* ⋆ → L1 = ⋆.
-/2 width=5/ 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 →
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 /3 width=6/
qed.
lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/
qed.
lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
[ /2/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
qed.
lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
[ /2/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
qed.
lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
[ /2/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
qed.
lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
- ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L.
+ ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
[ /2/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
]
-qed.
+qed-.
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 &
lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
]
-qed.
+qed-.
(∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫ T2 → R T → R T2) →
∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2.
#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
-qed.
+qed-.
(* Basic properties *********************************************************)
| #T #T2 #_ #HT2 #IHT destruct -T
>(tps_inv_sort1 … HT2) -HT2 //
]
-qed.
+qed-.
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 &
elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/
]
-qed.
+qed-.
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 &
| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
elim (tps_inv_flat1 … HU2) -HU2 /3 width=5/
]
-qed.
+qed-.
lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫* T2 → T1 = T2.
#L #T1 #T2 #d #H @(tpss_ind … H) -H T2
[ //
| #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
]
-qed.
+qed-.
@or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2/ (**) (* /4 width=10/ is too slow *)
]
]
-qed.
+qed-.
lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 →
T2 = #i ∨
#L #T2 #i #d #e #H
elim (tpss_inv_atom1 … H) -H /2/
* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct -i /3 width=6/
-qed.
+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.
#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -H T2 //
#T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
-qed.
+qed-.
(* Relocation properties ****************************************************)
--- /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/unfold/tpss.ma".
+
+(* SUBSTITUTION ON TERMS ****************************************************)
+
+definition tsubst: nat → nat → lenv → relation term ≝
+ λd,e,L,T1,T2. ∃∃T. L ⊢ T1 [d, e] ≫* T & ↑[d, e] T2 ≡ T.
+
+interpretation "substitution (term)"
+ 'TSubst L T1 d e T2 = (tsubst d e L T1 T2).
(* ARITHMETICAL PROPERTIES **************************************************)
+lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
+#x #y #H elim (decidable_lt x y) [2: /2 width=1/ ]
+#Hxy elim (H Hxy)
+qed-.
+
axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
#n #m <plus_n_Sm #H destruct
-qed.
+qed-.
lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
#n #m #p <plus_n_Sm #H @(lt_to_le_to_lt … H) //
lemma lt_refl_false: ∀n. n < n → False.
#n #H elim (lt_to_not_eq … H) -H /2/
-qed.
+qed-.
lemma lt_zero_false: ∀n. n < 0 → False.
#n #H elim (lt_to_not_le … H) -H /2/
-qed.
+qed-.
lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
#m #n elim (decidable_lt m n) /3/
| #m #IHm * [ /2/ ]
#n elim (IHm n) -IHm #H
[ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] /2/ (**) (* /3/ is slow *)
- qed.
+qed.
lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
/2/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *)
#m #n #H1 lapply (le_plus_n_r n m) #H2
lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
elim (lt_refl_false … H)
-qed.
+qed-.
lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
#m1 #m2 #H elim H -H m1
projects / helm.git / commitdiff