From 97e8285eaaacf54fd3689fc2862a1faea81694dd Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Sun, 30 Jun 2024 20:58:59 +0200 Subject: Finish CompleteTree.get implementation. Not proven to be correct yet. --- Common/BinaryHeap.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'Common/BinaryHeap.lean') diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index bce59c4..e7b552b 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -371,16 +371,17 @@ def CompleteTree.get {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : Complet match o with | (oo+1) => get ⟨j, h₄⟩ l else + have h₅ : n - o = p := Nat.sub_eq_of_eq_add $ (Nat.add_comm o p).subst h₂ have : p ≠ 0 := - have h₅ : o < n := Nat.lt_of_le_of_lt (Nat.ge_of_not_lt h₄) (Nat.lt_of_succ_lt_succ h₃) - have h₆ : n - o = p := Nat.sub_eq_of_eq_add $ (Nat.add_comm o p).subst h₂ - h₆.symm.substr $ Nat.sub_ne_zero_of_lt h₅ - have h₅ : j-o < p := sorry - have : j-o < index.val := sorry + have h₆ : o < n := Nat.lt_of_le_of_lt (Nat.ge_of_not_lt h₄) (Nat.lt_of_succ_lt_succ h₃) + h₅.symm.substr $ Nat.sub_ne_zero_of_lt h₆ + have h₆ : j - o < p := h₅.subst $ Nat.sub_lt_sub_right (Nat.ge_of_not_lt h₄) $ Nat.lt_of_succ_lt_succ h₃ + have : j - o < index.val := by simp_arith[h₁, Nat.sub_le] match p with - | (pp + 1) => get ⟨j - o, h₅⟩ r + | (pp + 1) => get ⟨j - o, h₆⟩ r termination_by _ => index.val + theorem two_n_not_zero_n_not_zero (n : Nat) (p : ¬2*n = 0) : (¬n = 0) := by cases n case zero => contradiction -- cgit v1.2.3