include "Basic_2/grammar/lsubs.ma".
include "Basic_2/substitution/lift.ma".
-(* DROPPING *****************************************************************)
+(* LOCAL ENVIRONMENT SLICING ************************************************)
(* Basic_1: includes: ldrop_skip_bind *)
inductive ldrop: nat → nat → relation lenv ≝
(* Basic inversion lemmas ***************************************************)
fact ldrop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
[ //
| //
| #L1 #L2 #I #V #e #_ #_ #H
fact ldrop_inv_atom1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ →
L2 = ⋆.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
[ //
| #L #I #V #H destruct
| #L1 #L2 #I #V #e #_ #H destruct
∀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 #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #K #I #V #H destruct
-| #L #I #V #_ #K #J #W #HX destruct -L I V /3/
-| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct -L1 I V /3/
+| #L #I #V #_ #K #J #W #HX destruct /3 width=1/
+| #L1 #L2 #I #V #e #HL12 #_ #K #J #W #H destruct /3 width=1/
| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
]
qed.
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 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.
#e #K #I #V #L2 #H #He
-elim (ldrop_inv_O1 … H) -H * // #H destruct -e;
+elim (ldrop_inv_O1 … H) -H * // #H destruct
elim (lt_refl_false … He)
qed-.
∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L2 = K2. 𝕓{I} V2.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K #V #H destruct
| #L #I #V #H elim (lt_refl_false … H)
| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct -X Y Z
- /2 width=5/
+| #X #L2 #Y #Z #V2 #d #e #HL12 #HV12 #_ #I #L1 #V1 #H destruct /2 width=5/
]
qed.
∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L2 = K2. 𝕓{I} V2.
-/2/ qed-.
+/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 →
∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.
-#d #e #L1 #L2 * -d e L1 L2
+#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K #V #H destruct
| #L #I #V #H elim (lt_refl_false … H)
| #L1 #L2 #I #V #e #_ #H elim (lt_refl_false … H)
-| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct -X Y Z
- /2 width=5/
+| #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #I #L2 #V2 #H destruct /2 width=5/
]
qed.
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 width=3/ qed-.
(* Basic properties *********************************************************)
lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
↓[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/
+#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 →
d ≤ i → i < d + e →
∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
↓[0, i] L2 ≡ K2. 𝕓{Abbr} V.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e
+#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
| #L1 #L2 #K1 #V #i #_ #_ #H
elim (lt_zero_false … H)
| #L1 #L2 #V #e #HL12 #IHL12 #K1 #W #i #H #_ #Hie
elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
- [ -IHL12 Hie; destruct -i K1 W;
- <minus_n_O <minus_plus_m_m /2/
- | -HL12;
- elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
+ [ -IHL12 -Hie destruct
+ <minus_n_O <minus_plus_m_m // /2 width=3/
+ | -HL12
+ elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
]
| #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
- [ -IHL12 Hie Hi; destruct
- | elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 // [2: /2/ ] -Hie >arith_g1 // /3/
+ [ -IHL12 -Hie -Hi destruct
+ | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
]
| #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
lapply (plus_S_le_to_pos … Hdi) #Hi
lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1
- elim (IHL12 … HLK1 ? ?) -IHL12 HLK1 [2: /2/ |3: /2/ ] -Hdi Hide >arith_g1 // /3/
+ elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 /2 width=1/ -Hdi -Hide >arith_g1 // /3 width=3/
]
qed.
[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
elim (ldrop_inv_O1 … H) -H * #He #H
- [ -IHL1; destruct -e K2 I2 V2 /2/
- | @ldrop_ldrop >(plus_minus_m_m e 1) /2/
+ [ -IHL1 destruct /2 width=1/
+ | @ldrop_ldrop >(plus_minus_m_m e 1) // /2 width=3/
]
]
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
-[ /2/
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
+[ /2 width=1/
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
- >(tw_lift … HV21) -HV21 /2/
+ >(tw_lift … HV21) -HV21 /2 width=1/
]
qed-.
[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
elim (ldrop_inv_O1 … H) -H * #He #H
- [ -IHL1; destruct -e K2 I2 V2 //
- | lapply (IHL1 … H) -IHL1 H #HeK1 whd in ⊢ (? ? %) /2/
+ [ -IHL1 destruct //
+ | lapply (IHL1 … H) -IHL1 -H #HeK1 whd in ⊢ (? ? %); /2 width=1/
]
]
qed-.
[ #L2 #e #H >(ldrop_inv_atom1 … H) -H //
| #K1 #I1 #V1 #IHL1 #L2 #e #H
elim (ldrop_inv_O1 … H) -H * #He #H
- [ -IHL1; destruct -e L2 //
- | lapply (IHL1 … H) -IHL1 H #H >H -H; normalize
+ [ -IHL1 destruct //
+ | lapply (IHL1 … H) -IHL1 -H #H >H -H normalize
>minus_le_minus_minus_comm //
]
]