From 93c883d5332469d90a4f1c42d45c66e2b6a89eb8 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 12 Oct 2025 18:19:52 +0200 Subject: Lean 4.19 --- BinaryHeap/Aux.lean | 2 +- .../AdditionalProofs/HeapUpdateAt.lean | 37 ++-- BinaryHeap/CompleteTree/HeapOperations.lean | 2 +- .../CompleteTree/HeapProofs/HeapUpdateAt.lean | 244 +++++++++++---------- BinaryHeap/CompleteTree/NatLemmas.lean | 2 +- lake-manifest.json | 2 +- lean-toolchain | 2 +- 7 files changed, 151 insertions(+), 140 deletions(-) diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean index e922a32..b57130a 100644 --- a/BinaryHeap/Aux.lean +++ b/BinaryHeap/Aux.lean @@ -42,7 +42,7 @@ def pushList {α : Type u} {n : Nat} {le : α → α → Bool} (heap : BinaryHea match l with | [] => heap | a :: as => - have : n + 1 + as.length = n + (a :: as).length := by simp +arith[List.length_cons a as] + have : n + 1 + as.length = n + (a :: as).length := by simp +arith only [List.length_cons] this▸pushList (heap.push a) as private def ofForInAux [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : (h : Nat) ×' BinaryHeap α le h := Id.run do diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean index c233355..8b5c5e3 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean @@ -10,17 +10,17 @@ theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : Co unfold heapUpdateAt heapUpdateAtAux rfl -theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) : heap.get index = (heap.heapUpdateAt le index val).snd := by +private theorem heapUpdateAtReturnsElementAt_Aux {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) (h₁ : n > 0) : get index heap = (heapUpdateAtAux le index val heap h₁).snd := by cases index rename_i i isLt cases i case mk.zero => - rw[←get_zero_eq_root, heapUpdatAtRootEqUpdateRoot] + rw[←heapUpdateAt,←get_zero_eq_root, heapUpdatAtRootEqUpdateRoot] exact Eq.symm $ heapUpdateRootReturnsRoot le val heap isLt case mk.succ j => - unfold heapUpdateAt heapUpdateAtAux + have : 0 < n := Nat.zero_lt_of_lt isLt + unfold heapUpdateAtAux generalize hj : (⟨j + 1, isLt⟩ : Fin n) = index -- otherwise split fails... - generalize heapUpdateAt.proof_1 index = h₁ -- this sounds fragile... It's the n > 0 proof split case isTrue h => simp only [←hj, beq_iff_eq, Fin.mk.injEq, Nat.add_one_ne_zero] at h --contradiction case isFalse => @@ -34,17 +34,19 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → case h₃ => rw[leftLen_unfold _ _ _ _ _ _ (Nat.succ_pos _)] exact h₂ - apply heapUpdateAtReturnsElementAt + apply heapUpdateAtReturnsElementAt_Aux case isFalse h₂ => rw[get_right] case h₂ => simp only [Nat.not_le] at h₂ simp only [leftLen_unfold, gt_iff_lt, h₂] - apply heapUpdateAtReturnsElementAt + apply heapUpdateAtReturnsElementAt_Aux -theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value).fst.contains value := by - unfold heapUpdateAt heapUpdateAtAux - generalize heapUpdateAt.proof_1 index = h₁ +theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (index : Fin n) : heap.get index = (heap.heapUpdateAt le index val).snd := + heapUpdateAtReturnsElementAt_Aux le val heap index _ + +theorem heapUpdateAtContainsValue_Aux {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) (h₁ : n > 0) : (heapUpdateAtAux le index value heap h₁).fst.contains value := by + unfold heapUpdateAtAux split case isTrue h₂ => apply heapUpdateRootContainsUpdatedElement @@ -70,8 +72,10 @@ theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bo right rewrite[right_unfold] all_goals - apply heapUpdateAtContainsValue -termination_by n + apply heapUpdateAtContainsValue_Aux + +theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value).fst.contains value := + heapUpdateAtContainsValue_Aux le heap value index (Nat.zero_lt_of_lt index.isLt) theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (updateIndex : Fin n) (otherIndex : Fin n) (h₂ : updateIndex ≠ otherIndex) : (heap.heapUpdateAt le updateIndex val).fst.contains $ heap.get otherIndex := have h₁ : n > 0 := Nat.zero_lt_of_lt otherIndex.isLt @@ -83,8 +87,9 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo else if h₄ : otherIndex = ⟨0, h₁⟩ then by subst h₄ rw[←get_zero_eq_root] - unfold heapUpdateAt heapUpdateAtAux - generalize heapUpdateAt.proof_1 updateIndex = h₁ + have : heapUpdateAt le updateIndex val heap = heapUpdateAtAux le updateIndex val heap h₁ := rfl + rw[this] + unfold heapUpdateAtAux --cannot use h₃ here already - it makes split fail. So, splitting twice it is... split case isTrue h => exact absurd (beq_iff_eq.mp h) h₃ @@ -114,8 +119,9 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo rewrite[root_unfold] apply heapUpdateAtContainsValue else by - unfold heapUpdateAt heapUpdateAtAux - generalize heapUpdateAt.proof_1 updateIndex = h₁ + have : heapUpdateAt le updateIndex val heap = heapUpdateAtAux le updateIndex val heap h₁ := rfl + rw[this] + unfold heapUpdateAtAux split case isTrue hx => exact absurd (beq_iff_eq.mp hx) h₃ case isFalse => @@ -172,4 +178,3 @@ theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bo --rw[leftLen_unfold] have h₅ : index.val ≥ o + 1 := Nat.gt_of_not_le h₅ exact (Nat.sub_ne_of_ne h₅ h₆).mp $ Fin.val_ne_iff.mpr h₂ -termination_by n diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index b5d8f01..28115b0 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -20,7 +20,7 @@ private theorem power_of_two_mul_two_lt {n m : Nat} (h₁ : m.isPowerOfTwo) (h /--Adds a new element to a given CompleteTree.-/ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : CompleteTree α (o+1) := match o, heap with - | 0, .leaf => .branch elem (.leaf) (.leaf) (Nat.le_refl 0) (by decide) (Or.inl Nat.one_isPowerOfTwo) + | 0, .leaf => .branch elem (.leaf) (.leaf) (Nat.le_refl 0) (by decide) (Or.inl Nat.isPowerOfTwo_one) | (n+m+1), .branch a left right p max_height_difference subtree_complete => let (elem, a) := if le elem a then (a, elem) else (elem, a) -- okay, based on n and m we know if we want to add left or right. diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean index 86d2499..17a40e9 100644 --- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean +++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean @@ -5,128 +5,134 @@ import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot namespace BinaryHeap.CompleteTree -private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) (h₄ : total_le le) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateAt le index value heap).fst := by - unfold heapUpdateAt heapUpdateAtAux - split - case isTrue => exact CompleteTree.heapUpdateRootIsHeapLeRootAux le value heap h₁ h₂ h₃ - case isFalse hi => - generalize heapUpdateAt.proof_1 index = h₂ +private theorem heapUpdateAtIsHeapLeRootAux_RootLeValue {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le (root heap h₂) value) (h₄ : total_le le) : HeapPredicate.leOrLeaf le (root heap h₂) (heapUpdateAt le index value heap).fst := + heapUpdateAtIsHeapLeRootAux_RootLeValue_Aux h₂ --factored out to avoid having to generalize an automatically named proof +where + heapUpdateAtIsHeapLeRootAux_RootLeValue_Aux (h₂ : n > 0) : HeapPredicate.leOrLeaf le (heap.root h₂) (heapUpdateAtAux le index value heap h₂).fst := by + unfold heapUpdateAtAux split - rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ - cases h₉ : le v value <;> simp only - case false => rw[root_unfold] at h₃; exact absurd h₃ ((Bool.not_eq_true (le v value)).substr h₉) - case true => - rw[root_unfold] + case isTrue => exact CompleteTree.heapUpdateRootIsHeapLeRootAux le value heap h₁ h₂ h₃ + case isFalse hi => split - <;> simp![reflexive_le, h₄] + rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ + cases h₉ : le v value <;> simp only + case false => rw[root_unfold] at h₃; exact absurd h₃ ((Bool.not_eq_true (le v value)).substr h₉) + case true => + rw[root_unfold] + split + <;> simp![reflexive_le, h₄] -private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le value (root heap h₂)) (h₄ : total_le le) (h₅ : transitive_le le) : HeapPredicate.leOrLeaf le value (heapUpdateAt le index value heap).fst := by - unfold heapUpdateAt heapUpdateAtAux - generalize heapUpdateAt.proof_1 index = h₂ - split - <;> rename_i h₉ - case isTrue => - unfold heapUpdateRoot +private theorem heapUpdateAtIsHeapLeRootAux_ValueLeRoot {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₁ : HeapPredicate heap le) (h₂ : n > 0) (h₃ : le value (root heap h₂)) (h₄ : total_le le) (h₅ : transitive_le le) : HeapPredicate.leOrLeaf le value (heapUpdateAt le index value heap).fst := + heapUpdateAtIsHeapLeRootAux_ValueLeRoot_Aux h₂ +where + heapUpdateAtIsHeapLeRootAux_ValueLeRoot_Aux (h₂ : n > 0): HeapPredicate.leOrLeaf le value (heapUpdateAtAux le index value heap h₂).fst := by + unfold heapUpdateAtAux split - rename_i o p v l r h₆ h₇ h₈ h₂ - cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, Nat.add_one_ne_zero, root_unfold, h₄, reflexive_le] - <;> unfold HeapPredicate at h₁ - <;> have h₁₀ : le value $ l.root (by omega) := h₅ value v (l.root _) ⟨h₃, h₁.right.right.left⟩ - simp only [↓reduceIte, Nat.add_zero, h₁₀, root_unfold, h₄, reflexive_le] - have h₁₁ : le value $ r.root (by omega) := h₅ value v (r.root _) ⟨h₃, h₁.right.right.right⟩ - simp only [↓reduceIte, h₁₀, h₁₁, and_self, root_unfold, h₄, reflexive_le] - case isFalse => - split - rename_i o p v l r h₆ h₇ h₈ index h₂ hi - cases le v value - <;> simp +ground only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢ - <;> split - <;> unfold HeapPredicate.leOrLeaf - <;> simp only [reduceIte, root_unfold, h₃, h₄, reflexive_le] + <;> rename_i h₉ + case isTrue => + unfold heapUpdateRoot + split + rename_i o p v l r h₆ h₇ h₈ h₂ + cases o <;> cases p <;> simp [↓reduceDIte,HeapPredicate.leOrLeaf, Nat.add_one_ne_zero, root_unfold, h₄, reflexive_le] + <;> unfold HeapPredicate at h₁ + <;> have h₁₀ : le value $ l.root (by omega) := h₅ value v (l.root _) ⟨h₃, h₁.right.right.left⟩ + simp only [↓reduceIte, Nat.add_zero, h₁₀, root_unfold, h₄, reflexive_le] + have h₁₁ : le value $ r.root (by omega) := h₅ value v (r.root _) ⟨h₃, h₁.right.right.right⟩ + simp only [↓reduceIte, h₁₀, h₁₁, and_self, root_unfold, h₄, reflexive_le] + case isFalse => + split + rename_i o p v l r h₆ h₇ h₈ index h₂ hi + cases le v value + <;> simp +ground only [root_unfold, Nat.pred_eq_sub_one] at h₃ ⊢ + <;> split + <;> unfold HeapPredicate.leOrLeaf + <;> simp only [reduceIte, root_unfold, h₃, h₄, reflexive_le] -theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateAt le index value).fst le := by - unfold heapUpdateAt heapUpdateAtAux - generalize heapUpdateAt.proof_1 index = h₁ - split - case isTrue h₅ => - exact heapUpdateRootIsHeap le value heap _ h₂ h₃ h₄ - case isFalse h₅ => +theorem heapUpdateAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin n) (value : α) (heap : CompleteTree α n) (h₂ : HeapPredicate heap le) (h₃ : transitive_le le) (h₄ : total_le le) : HeapPredicate (heap.heapUpdateAt le index value).fst le := + heapUpdateAtIsHeap_Aux (Fin.pos index) +where + heapUpdateAtIsHeap_Aux (h₁ : n > 0) : HeapPredicate (heapUpdateAtAux le index value heap h₁).fst le := by + unfold heapUpdateAtAux split - rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ - cases h₁₀ : le v value <;> simp +ground -- this could probably be solved without this split, but readability... - <;> split - <;> rename_i h -- h is the same name as used in the function - <;> unfold HeapPredicate at h₂ ⊢ - <;> simp only [h₂, and_true, true_and] - case false.isFalse => - have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀) - have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _ - apply And.intro <;> try apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ v r h₂.right.left h₃ h₄ - case right.left => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.left - case right.right => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le := - (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄) - cases h₁₂ : le v (r.root h₁₄) - case false => - cases p - exact absurd (Nat.lt_succ.mp index.isLt) h - exact absurd h₂.right.right.right ((Bool.eq_false_iff).mp h₁₂) - case true => - have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left (by omega) h₁₂ h₄ h₃ - apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ - exact h₁₀ - case false.isTrue => - have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀) - have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ - apply And.intro <;> try apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ v l h₂.left h₃ h₄ - case right.right => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.right - case right.left => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (_)⟩ v l).fst le := - (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄) - cases h₁₂ : le v (l.root h₁₄) - case false => - cases o - contradiction -- h₁₄ is False - exact absurd h₂.right.right.left ((Bool.eq_false_iff).mp h₁₂) - case true => - have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ v l h₂.left (by omega) h₁₂ h₄ h₃ - apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ - exact h₁₀ - case true.isFalse => - have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _ - apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ value r h₂.right.left h₃ h₄ - case right => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le := - (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄) - cases h₁₂ : le value (r.root h₁₄) - case false => - have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) (not_le_imp_le h₄ value (r.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄ - apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ - cases p - contradiction -- h₁₄ is False - exact h₂.right.right.right - case true => - have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) h₁₂ h₄ h₃ - apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ - exact h₁₀ - case true.isTrue => - have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ - apply And.intro - case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ value l h₂.left h₃ h₄ - case right => - have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (by omega)⟩ v l).fst le := - (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄) - cases h₁₂ : le value (l.root h₁₄) - case false => - have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) (not_le_imp_le h₄ value (l.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄ - apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ - cases o - contradiction -- h₁₄ is False - exact h₂.right.right.left - case true => - have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) h₁₂ h₄ h₃ - apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ - exact h₁₀ + case isTrue h₅ => + exact heapUpdateRootIsHeap le value heap _ h₂ h₃ h₄ + case isFalse h₅ => + split + rename_i o p v l r h₆ h₇ h₈ index h₁ h₅ + cases h₁₀ : le v value <;> simp +ground -- this could probably be solved without this split, but readability... + <;> split + <;> rename_i h -- h is the same name as used in the function + <;> unfold HeapPredicate at h₂ ⊢ + <;> simp only [h₂, and_true, true_and] + case false.isFalse => + have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀) + have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _ + apply And.intro <;> try apply And.intro + case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ v r h₂.right.left h₃ h₄ + case right.left => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.left + case right.right => + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le := + (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄) + cases h₁₂ : le v (r.root h₁₄) + case false => + cases p + exact absurd (Nat.lt_succ.mp index.isLt) h + exact absurd h₂.right.right.right ((Bool.eq_false_iff).mp h₁₂) + case true => + have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left (by omega) h₁₂ h₄ h₃ + apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ + exact h₁₀ + case false.isTrue => + have h₁₀ := not_le_imp_le h₄ v value (Bool.eq_false_iff.mp h₁₀) + have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ + apply And.intro <;> try apply And.intro + case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ v l h₂.left h₃ h₄ + case right.right => exact HeapPredicate.leOrLeaf_transitive h₃ h₁₀ h₂.right.right.right + case right.left => + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (_)⟩ v l).fst le := + (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄) + cases h₁₂ : le v (l.root h₁₄) + case false => + cases o + contradiction -- h₁₄ is False + exact absurd h₂.right.right.left ((Bool.eq_false_iff).mp h₁₂) + case true => + have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ v l h₂.left (by omega) h₁₂ h₄ h₃ + apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ + exact h₁₀ + case true.isFalse => + have h₁₄ : p > 0 := by cases p; exact absurd (Nat.lt_succ.mp index.isLt) h; exact Nat.zero_lt_succ _ + apply And.intro + case left => exact heapUpdateAtIsHeap le ⟨index.val - o - 1, _⟩ value r h₂.right.left h₃ h₄ + case right => + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - o - 1, (by omega)⟩ v r).fst le := + (heapUpdateAtIsHeap le ⟨index.val - o - 1, (by omega)⟩ v r h₂.right.left h₃ h₄) + cases h₁₂ : le value (r.root h₁₄) + case false => + have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) (not_le_imp_le h₄ value (r.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄ + apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ + cases p + contradiction -- h₁₄ is False + exact h₂.right.right.right + case true => + have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - o - 1, (by omega)⟩ value r h₂.right.left (by omega) h₁₂ h₄ h₃ + apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ + exact h₁₀ + case true.isTrue => + have h₁₄ : o > 0 := by cases o; simp at h₅ h; exact absurd (Fin.val_inj.mp h : index = 0) h₅; exact Nat.zero_lt_succ _ + apply And.intro + case left => exact heapUpdateAtIsHeap le ⟨index.val - 1, _⟩ value l h₂.left h₃ h₄ + case right => + have h₁₁: HeapPredicate (heapUpdateAt le ⟨index.val - 1, (by omega)⟩ v l).fst le := + (heapUpdateAtIsHeap le ⟨index.val - 1, (by omega)⟩ v l h₂.left h₃ h₄) + cases h₁₂ : le value (l.root h₁₄) + case false => + have h₁₃ := heapUpdateAtIsHeapLeRootAux_RootLeValue le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) (not_le_imp_le h₄ value (l.root h₁₄) (Bool.eq_false_iff.mp h₁₂)) h₄ + apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ + cases o + contradiction -- h₁₄ is False + exact h₂.right.right.left + case true => + have h₁₃ := heapUpdateAtIsHeapLeRootAux_ValueLeRoot le ⟨index.val - 1, (by omega)⟩ value l h₂.left (by omega) h₁₂ h₄ h₃ + apply HeapPredicate.leOrLeaf_transitive h₃ _ h₁₃ + exact h₁₀ diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean index 56b3203..1050c17 100644 --- a/BinaryHeap/CompleteTree/NatLemmas.lean +++ b/BinaryHeap/CompleteTree/NatLemmas.lean @@ -40,7 +40,7 @@ private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.n unfold Nat.nextPowerOfTwo apply power_of_two_go_one_eq case h₁ => assumption - case h₂ => exact Nat.one_isPowerOfTwo + case h₂ => exact Nat.isPowerOfTwo_one case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁) private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by diff --git a/lake-manifest.json b/lake-manifest.json index 644812c..c1148ad 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,4 +1,4 @@ -{"version": "1.0.0", +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [], "name": "BinaryHeap", diff --git a/lean-toolchain b/lean-toolchain index 9f78e65..a0922e9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:4.18.0 +leanprover/lean4:4.19.0 -- cgit v1.2.3