From cf1bc3567a2111f11eb45923d03d1e1ef3c01c52 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 30 Jun 2024 19:19:34 +0200
Subject: partial implementation of CompleteTree.get

---
 Common/BinaryHeap.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'Common')

diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean
index 1801122..bce59c4 100644
--- a/Common/BinaryHeap.lean
+++ b/Common/BinaryHeap.lean
@@ -363,6 +363,24 @@ def CompleteTree.indexOfAux {α : Type u} (heap : CompleteTree α o) (pred : α
 def CompleteTree.indexOf {α : Type u} (heap : CompleteTree α o) (pred : α → Bool) : Option (Fin o) :=
   indexOfAux heap pred 0
 
+def CompleteTree.get {α : Type u} {n : Nat} (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α :=
+  match h₁ : index, h₂ : n, heap with
+  | 0, (_+_), .branch v _ _ _ _ _ => v
+  | ⟨j+1,h₃⟩, (o+p), .branch _ l r _ _ _ =>
+    if h₄ : j < o then
+      match o with
+      | (oo+1) => get ⟨j, h₄⟩ l
+    else
+      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
+      match p with
+      | (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