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 +++++++------
 Common/Nat.lean        |  8 ++++++++
 2 files changed, 15 insertions(+), 6 deletions(-)

(limited to 'Common')

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
diff --git a/Common/Nat.lean b/Common/Nat.lean
index 1721653..0a0f1f4 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -166,3 +166,11 @@ theorem Nat.sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) :
   have h₇ : 1 + (a-b) ≤ c := h₆.subst (motive := λx ↦ x ≤ c) h₅
   have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇
   Nat.lt_of_succ_le h₈
+
+theorem Nat.sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a - b < c - b) := by
+  apply Nat.sub_lt_of_lt_add
+  case h₂ => assumption
+  case h₁ =>
+    have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂
+    rw[Nat.sub_add_cancel h₃]
+    assumption
-- 
cgit v1.2.3