lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
// qed.
+lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
+// qed.
+
lemma minus_le: ∀m,n. m - n ≤ m.
/2/ qed.
lemma plus_plus_minus_m_m: ∀e1,e2,d. e1 ≤ e2 → d + e1 + (e2 - e1) = d + e2.
/2/ qed.
+lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
+/2/ qed.
+
+lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
+/2/ qed.
+
lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → (m + n) - p = (m - p) + n.
#n #m #p #lepm @plus_to_minus <associative_plus
>(commutative_plus p) <plus_minus_m_m //
qed.
-lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
-#m #n elim (decidable_lt m n) /3/
+lemma minus_le_minus_minus_comm: ∀m,p,n.
+ p ≤ m → m - p ≤ n → n + p - m = n - (m - p).
+#m elim m -m
+[ #p #n #H >(le_O_to_eq_O … H) -H //
+| #m #IHm #p elim p -p //
+ #p #_ #n #Hpm <plus_n_Sm @IHm /2/
+]
qed.
lemma lt_refl_false: ∀n. n < n → False.
#n #H elim (lt_to_not_le … H) -H /2/
qed.
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /3/
+qed.
+
lemma plus_lt_false: ∀m,n. m + n < m → False.
#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.
-lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
-/2/ qed.
-
lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
#n #m <plus_n_Sm #H destruct
qed.
-lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
-// qed.
-
lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
/3/ qed.
-lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
-/2/ qed.
-
lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
/2/ qed.
-lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
-/3/ qed.
-
-lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
-/3/ qed.
+lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
+#m #n #H >minus_plus <minus_minus //
+qed.
lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
/2/ qed.
lemma arith5: ∀i,h,d. i + h ≤ d → d - i - h + (i + h) = d.
/2/ qed.
-lemma arith6: ∀m,n. m < n → n - (n - m - 1) = m + 1.
-#m #n #H >minus_plus <minus_minus //
-qed.
-
lemma arith7: ∀i,d. i ≤ d → d - i + i = d.
/2/ qed.
+
+lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
+/3/ qed.
+
+lemma arith3: ∀m,n,p. p ≤ m → m + n - (m - p + n) = p.
+/3/ qed.
+
interpretation "dropping" 'RLift L2 d e L1 = (drop L1 d e L2).
-(* the basic inversion lemmas ***********************************************)
+(* Basic properties *********************************************************)
-lemma drop_inv_drop1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → 0 < e → d = 0 →
- ∀K,I,V. L1 = K. 𝕓{I} V → ↑[d, e - 1] L2 ≡ K.
+lemma drop_drop_lt: ∀L1,L2,I,V,e.
+ ↑[0, e - 1] L2 ≡ L1 → 0 < e → ↑[0, e] L2 ≡ L1. 𝕓{I} V.
+#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma drop_inv_refl_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 → e = 0 → L1 = L2.
#d #e #L2 #L1 #H elim H -H d e L2 L1
-[ #L #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V #e #HL12 #_ #_ #_ #K #J #W #H destruct -L1 I V //
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #_ #H elim (plus_S_eq_O_false … H)
+[ //
+| #L1 #L2 #I #V #e #_ #_ #_ #H
+ elim (plus_S_eq_O_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H
+ elim (plus_S_eq_O_false … H)
]
qed.
-lemma drop_inv_drop1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e →
- ↑[0, e - 1] L2 ≡ K.
+lemma drop_inv_refl: ∀L2,L1. ↑[0, 0] L2 ≡ L1 → L1 = L2.
/2 width=5/ qed.
+lemma drop_inv_O1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → d = 0 →
+ ∀K,I,V. L1 = K. 𝕓{I} V →
+ (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+ (0 < e ∧ ↑[d, e - 1] L2 ≡ K).
+#d #e #L2 #L1 #H elim H -H d e L2 L1
+[ /3/
+| #L1 #L2 #I #V #e #HL12 #_ #_ #K #J #W #H destruct -L1 I V /3/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #H elim (plus_S_eq_O_false … H)
+]
+qed.
+
+lemma drop_inv_O1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V →
+ (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+ (0 < e ∧ ↑[0, e - 1] L2 ≡ K).
+/2/ qed.
+
+lemma drop_inv_drop1: ∀e,L2,K,I,V.
+ ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e → ↑[0, e - 1] L2 ≡ K.
+#e #L2 #K #I #V #H #He
+elim (drop_inv_O1 … H) -H * // #H destruct -e;
+elim (lt_refl_false … He)
+qed.
+
lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d →
∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
∃∃K1,V1. ↑[d - 1, e] K2 ≡ K1 &
lapply (transitive_le 1 … Hdee2) // #He2
lapply (drop_inv_drop1 … H ?) -H // -He2 #HL2
lapply (transitive_le (1+e) … Hdee2) // #Hee2
- >(plus_minus_m_m (e2-e) 1 ?) [ @drop_drop >minus_minus_comm /3/ | /2/ ]
+ @drop_drop_lt >minus_minus_comm /3/ (**) (* explicit constructor *)
]
qed.
-axiom drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
+lemma drop_conf_lt: ∀d1,e1,L,L1. ↑[d1, e1] L1 ≡ L →
∀e2,K2,I,V2. ↑[0, e2] K2. 𝕓{I} V2 ≡ L →
e2 < d1 → let d ≝ d1 - e2 - 1 in
∃∃K1,V1. ↑[0, e2] K1. 𝕓{I} V1 ≡ L1 &
↑[d, e1] K1 ≡ K2 & ↑[d,e1] V1 ≡ V2.
+#d1 #e1 #L #L1 #H elim H -H d1 e1 L L1
+[ #L0 #e2 #K2 #I #V2 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #I #V #e #_ #_ #e2 #K2 #J #V2 #_ #H
+ elim (lt_zero_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #K2 #J #V #H #He2d
+ elim (drop_inv_O1 … H) -H *
+ [ -IHL12 He2d #H1 #H2 destruct -e2 K2 J V /2 width=5/
+ | -HL12 -HV12 #He #HLK
+ elim (IHL12 … HLK ?) -IHL12 HLK [ <minus_minus /3 width=5/ | /2/ ] (**) (* a bit slow *)
+ ]
+]
+qed.
-axiom drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
+lemma drop_trans_le: ∀d1,e1,L1. ∀L:lenv. ↑[d1, e1] L ≡ L1 →
∀e2,L2. ↑[0, e2] L2 ≡ L → e2 ≤ d1 →
∃∃L0. ↑[0, e2] L0 ≡ L1 & ↑[d1 - e2, e1] L2 ≡ L0.
+#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
+[ #L #e2 #L2 #HL2 #H
+ lapply (le_O_to_eq_O … H) -H #H destruct -e2 /2/
+| #L1 #L2 #I #V #e #_ #IHL12 #e2 #L #HL2 #H
+ lapply (le_O_to_eq_O … H) -H #H destruct -e2;
+ elim (IHL12 … HL2 ?) -IHL12 HL2 // #L0 #H #HL0
+ lapply (drop_inv_refl … H) -H #H destruct -L1 /3 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #IHL12 #e2 #L #H #He2d
+ elim (drop_inv_O1 … H) -H *
+ [ -He2d IHL12 #H1 #H2 destruct -e2 L /3 width=5/
+ | -HL12 HV12 #He2 #HL2
+ elim (IHL12 … HL2 ?) -IHL12 HL2 L2
+ [ <minus_le_minus_minus_comm /3/ | /2/ ]
+ ]
+]
+qed.
axiom drop_trans_ge: ∀d1,e1,L1,L. ↑[d1, e1] L ≡ L1 →
∀e2,L2. ↑[0, e2] L2 ≡ L → d1 ≤ e2 → ↑[0, e1 + e2] L2 ≡ L1.
projects / helm.git / commitdiff