diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 105 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/NatLemmas.lean | 31 |
2 files changed, 84 insertions, 52 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 364cbf3..866cc7a 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -2,6 +2,7 @@ import BinaryHeap.CompleteTree.HeapOperations import BinaryHeap.CompleteTree.HeapProofs.HeapRemoveLast import BinaryHeap.CompleteTree.AdditionalProofs.Contains import BinaryHeap.CompleteTree.AdditionalProofs.Get +import BinaryHeap.CompleteTree.NatLemmas namespace BinaryHeap.CompleteTree.AdditionalProofs @@ -46,8 +47,8 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N --but first, let's get rid of mm and nn, and vv while at it. -- which are equal to m, n, v, but we need to deduce this from he₃... - have : n = nn := heqSameLeftLen (congrArg (·+1) he₂) (by simp_arith) he₃ - have : m = mm := heqSameRightLen (congrArg (·+1) he₂) (by simp_arith) he₃ + have : n = nn := heqSameLeftLen (congrArg (·+1) he₂) (Nat.succ_pos _) he₃ + have : m = mm := heqSameRightLen (congrArg (·+1) he₂) (Nat.succ_pos _) he₃ subst nn mm simp only [heq_eq_eq, branch.injEq] at he₃ -- yeah, no more HEq fuglyness! @@ -93,8 +94,8 @@ private theorem lens_see_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 = case zero => simp only [Nat.add_zero] case succ pp hp => have h₂ := hp (q := q+1) - have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := by simp_arith - have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := by simp_arith + have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := Nat.add_comm_right q 1 (pp + 1) + have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := (Nat.add_comm_right (q+1) 1 pp).substr $ Nat.add_assoc (q+1) pp 1 rw[h₃, h₄] at h₂ revert hb ha heap h₁ assumption @@ -104,8 +105,8 @@ private theorem left_sees_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 = case zero => simp only [Nat.add_zero, heq_eq_eq] case succ pp hp => have h₂ := hp (q := q+1) - have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := by simp_arith - have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := by simp_arith + have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := Nat.add_comm_right q 1 (pp + 1) + have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := (Nat.add_comm_right (q+1) 1 pp).substr $ Nat.add_assoc (q+1) pp 1 rw[h₃, h₄] at h₂ revert hb ha heap h₁ assumption @@ -115,8 +116,8 @@ private theorem right_sees_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 case zero => simp only [Nat.add_zero, heq_eq_eq] case succ pp hp => have h₂ := hp (q := q+1) - have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := by simp_arith - have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := by simp_arith + have h₃ : (q + 1 + pp + 1) = q + (pp + 1) + 1 := Nat.add_comm_right q 1 (pp + 1) + have h₄ : (q + 1 + 1 + pp) = q + 1 + (pp + 1) := (Nat.add_comm_right (q+1) 1 pp).substr $ Nat.add_assoc (q+1) pp 1 rw[h₃, h₄] at h₂ revert hb ha heap h₁ assumption @@ -759,21 +760,20 @@ private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat rw[this] case succ pp hp => have hp₂ := hp (o := o+1) - have hp₃ : (o + 1 + pp + 1) = o + (pp + 1) + 1 := by simp_arith - have hp₄ : (o + 1 + 1 + pp) = o + 1 + (pp + 1) := by simp_arith + have hp₃ : (o + 1 + pp + 1) = o + (pp + 1) + 1 := Nat.add_comm_right o 1 (pp + 1) + have hp₄ : (o + 1 + 1 + pp) = o + 1 + (pp + 1) := (Nat.add_comm_right (o+1) 1 pp).substr $ Nat.add_assoc (o+1) pp 1 rw[hp₃, hp₄] at hp₂ - have hp₅ := hp₂ (index.cast (by simp_arith)) h₁ tree h₂ h₃ (by simp_arith at h₄ ⊢; omega) h₅ h₆ (by simp_arith at h₇ ⊢; omega) - simp at hp₅ - assumption + have : o + 1 + (pp + 1) + 1 = o + 1 + 1 + pp + 1 := Nat.add_comm_right (o + 1) (pp + 1) 1 + exact hp₂ (index.cast this) h₁ tree h₂ h₃ h₄ h₅ h₆ h₇ -private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {oo p : Nat} (index : Fin (oo + 1 + p)) (tree : CompleteTree α (oo + p + 1)) (h₁ : oo + p + 1 = oo + 1 + p) (h₂ : oo + 1 + p > 0) (h₃ : oo + p + 1 > 0) (h₄ : index.val < oo + p + 1) : get index (h₁▸tree) h₂ = get ⟨index.val,h₄⟩ tree h₃ := by - induction p generalizing oo +private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {o p : Nat} (index : Fin (o + 1 + p)) (tree : CompleteTree α (o + p + 1)) (h₁ : o + p + 1 = o + 1 + p) (h₂ : o + 1 + p > 0) (h₃ : o + p + 1 > 0) (h₄ : index.val < o + p + 1) : get index (h₁▸tree) h₂ = get ⟨index.val,h₄⟩ tree h₃ := by + induction p generalizing o case zero => simp case succ pp hp => - have hp₂ := hp (oo := oo+1) - have hp₃ : (oo + 1 + pp + 1) = oo + (pp + 1) + 1 := by simp_arith - have hp₄ : (oo + 1 + 1 + pp) = oo + 1 + (pp + 1) := by simp_arith + have hp₂ := hp (o := o+1) + have hp₃ : (o + 1 + pp + 1) = o + (pp + 1) + 1 := Nat.add_comm_right o 1 (pp + 1) + have hp₄ : (o + 1 + 1 + pp) = o + 1 + (pp + 1) := (Nat.add_comm_right (o+1) 1 pp).substr $ Nat.add_assoc (o+1) pp 1 rw[hp₃, hp₄] at hp₂ exact hp₂ index tree h₁ h₂ h₃ h₄ @@ -806,24 +806,14 @@ case isFalse h₃ => simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt] rw[Fin.lt_iff_val_lt_val] at h₁ simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁ - omega - have h₆ : index > o := by - simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt] at h₅ - omega - have h₇ : ↑index - o - 1 < pp + 1 := by - have : ↑index < o.add (pp + 1) + 1 := index.isLt - unfold Fin.pred Fin.subNat at h₅ - simp only [Nat.add_eq, gt_iff_lt] at h₅ - generalize index.val = i at h₅ h₆ this ⊢ - simp only [Nat.add_eq] at this - omega - have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd := by - unfold Internal.heapRemoveLastWithIndex - simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one, gt_iff_lt] - rw[Fin.lt_iff_val_lt_val] at h₁ ⊢ - simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁ ⊢ - generalize Fin.val (Internal.heapRemoveLastAux (β := λn ↦ α × Fin n) r _ _ _).2.snd = indexInR at h₁ ⊢ - omega + exact Nat.lt_of_add_right $ Nat.lt_pred_of_succ_lt h₁ + have h₆ : index > o := Nat.lt_of_add_left $ Nat.succ_lt_of_lt_pred h₅ + have h₇ : ↑index - o - 1 < pp + 1 := + have : ↑index < (o + 1) + (pp + 1) := (Nat.add_comm_right o (pp+1) 1).subst index.isLt + have : ↑index < (pp + 1) + (o + 1) := (Nat.add_comm (o+1) (pp+1)).subst this + (Nat.sub_lt_of_lt_add this (Nat.succ_le_of_lt h₆) : ↑index - (o + 1) < pp + 1) + have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd := + Nat.lt_sub_of_add_lt (b := o+1) h₁ rw[get_right' _ h₅] rw[get_right' _ h₆] at hold rw[←hold] @@ -832,8 +822,12 @@ case isFalse h₃ => unfold Fin.pred Fin.subNat at h₉ simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one] at h₉ simp only [Nat.add_eq, Fin.coe_pred, Fin.isValue] - have : ↑index - 1 - o - 1 = ↑index - o - 1 - 1 := by omega - simp only [this, Nat.add_eq, Fin.isValue, h₉] + have : ↑index - 1 - o - 1 = ↑index - o - 1 - 1 := + (rfl : ↑index - (o + 1 + 1) = ↑index - (o + 1 + 1)) + |> (Nat.add_comm o 1).subst (motive := λx ↦ ↑index - (x + 1) = ↑index - (o + 1 + 1)) + |> (Nat.sub_sub ↑index 1 (o+1)).substr + --exact this.substr h₉ --seems to run into a Lean 4.9 bug when proving termination + simp only [this, Nat.add_eq, Fin.isValue, h₉] --no idea why simp avoids the same issue... case isTrue h₃ => --removed left simp only [h₃, and_self, ↓reduceDite, Fin.isValue] at h₁ ⊢ @@ -845,7 +839,7 @@ case isTrue h₃ => -- get goes into the right branch rw[get_right' _ h₄] have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁ - have h₆ : index.pred h₅ > oo := by simp; omega + have h₆ : index.pred h₅ > oo := Nat.lt_pred_iff_succ_lt.mpr h₄ rw[get_right] case h₂ => rw[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] @@ -855,27 +849,34 @@ case isTrue h₃ => Fin.coe_pred, Fin.isValue, ← lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _] simp only[leftLen_unfold] apply heapRemoveLastWithIndexRelationGt_Aux - case h₁ => simp_arith only + case h₁ => exact Nat.add_comm_right oo 1 p case h₅ => exact Nat.succ_pos _ else -- get goes into the left branch + have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁ rw[heapRemoveLastWithIndexRelationGt_Aux2] case h₃ => exact Nat.succ_pos _ - case h₄ => omega + case h₄ => exact + Nat.le_of_not_gt h₄ + |> (Nat.succ_pred (Fin.val_ne_of_ne h₅)).substr + |> Nat.succ_le.mp + |> Nat.lt_add_right p + |> (Nat.add_comm_right oo 1 p).subst generalize hold : get index (branch v l r _ _ _) _ = old - have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁ - have h₆ : index.pred h₅ ≤ oo := by - simp only [Nat.add_eq, Fin.coe_pred] - rw[Fin.lt_iff_val_lt_val] at h₁ - simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE] at h₁ - omega - have h₇ : ↑index - 1 < oo + p + 1 := - Nat.lt_of_le_of_lt ((Fin.coe_pred index h₅).subst (motive := λx ↦ x ≤ oo) h₆) (Nat.lt_succ_of_le (Nat.le_add_right oo p)) + have h₆ : index.pred h₅ ≤ oo := Nat.pred_le_iff_le_succ.mpr $ Nat.le_of_not_gt h₄ + have h₇ : ↑index - 1 ≤ oo := (Fin.coe_pred index h₅).subst (motive := λx↦x ≤ oo) h₆ + have h₈ : ↑index ≤ oo + 1 := Nat.le_succ_of_pred_le h₇ rw[get_left'] - <;> simp - case h₁ => sorry + case h₁ => exact Nat.zero_lt_of_lt $ Nat.lt_sub_of_add_lt h₁ case h₂ => exact h₆ - sorry + simp only [Fin.coe_pred, Fin.isValue] + rw[get_left'] at hold + case h₁ => exact Fin.pos_iff_ne_zero.mpr h₅ + case h₂ => exact h₈ + subst hold + have h₈ : ⟨↑index - 1, Nat.lt_succ.mpr h₇⟩ > (Internal.heapRemoveLastWithIndex l).snd.snd := + Nat.lt_sub_of_add_lt h₁ + exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt l ⟨↑index - 1, Nat.lt_succ.mpr h₇⟩ h₈ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)): let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean index 33e67eb..8038405 100644 --- a/BinaryHeap/CompleteTree/NatLemmas.lean +++ b/BinaryHeap/CompleteTree/NatLemmas.lean @@ -167,3 +167,34 @@ theorem add_eq_zero {a b : Nat} : a + b = 0 ↔ a = 0 ∧ b = 0 := by simp[h₁] case mp => cases a <;> simp_arith at *; assumption + +-- Yes, this is trivial. Still, I needed it so often, that it deserves its own lemma. +theorem add_comm_right (a b c : Nat) : a + b + c = a + c + b := + (rfl : a + b + c = a + b + c) + |> Eq.subst (Nat.add_comm a b) (motive := λx ↦ x + c = a + b + c) + |> Eq.subst (Nat.add_assoc b a c) (motive := λx ↦ x = a + b + c) + |> Eq.subst (Nat.add_comm b (a+c)) (motive := λx ↦ x = a + b + c) + |> Eq.symm + +theorem lt_of_add_left {a b c : Nat} : a + b < c → a < c := by + intro h₁ + induction b generalizing a + case zero => exact h₁ + case succ bb hb => + have hb := hb (a := a.succ) + rw[Nat.add_comm bb 1] at h₁ + rw[←Nat.add_assoc] at h₁ + have hb := hb h₁ + exact Nat.lt_of_succ_lt hb + +theorem lt_of_add_right {a b c : Nat} : a + b < c → b < c := by + rw[Nat.add_comm a b] + exact lt_of_add_left + +theorem lt_of_add {a b c : Nat} : a + b < c → a < c ∧ b < c := by + intro h₁ + constructor + case left => + exact lt_of_add_left h₁ + case right => + exact lt_of_add_right h₁ |