From 97e8285eaaacf54fd3689fc2862a1faea81694dd Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
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

