internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
h : IsHeap lt x i
j₁ j₂ : Fin (Subarray.size x)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
induction h with
| out_of_range _ h => refine .out_of_range _ h
| node' i hi hx₁ hx₂ _ _ IHl IHr =>
  specialize IHl (trans hj₁ (lt_child_left i)) (trans hj₂ (lt_child_left i))
  specialize IHr (trans hj₁ (lt_child_right i)) (trans hj₂ (lt_child_right i))
  refine node' i hi ?_ ?_ IHl IHr
  . intro hl; specialize hx₁ hl
    simp only [Subarray.getElem_swap]
    iterate rewrite [if_neg]
    exact hx₁
    all_goals apply Nat.ne_of_lt
    . exact trans hj₁ (lt_child_left i)
    . exact trans hj₂ (lt_child_left i)
    . exact hj₁
    . exact hj₂
  . intro hr; specialize hx₂ hr
    simp only [Subarray.getElem_swap]
    iterate rewrite [if_neg]
    exact hx₂
    all_goals apply Nat.ne_of_lt
    . exact trans hj₁ (lt_child_right i)
    . exact trans hj₂ (lt_child_right i)
    . exact hj₁
    . exact hj₂
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case out_of_range
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
j₁ j₂ : Fin (Subarray.size x)
i✝ : Nat
h : i✝ ≥ Subarray.size x
hj₁ : ↑j₁ < i✝
hj₂ : ↑j₂ < i✝
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i✝
Tactic:
refine .out_of_range _ h
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IHl : ↑j₁ < 2 * i + 1 → ↑j₂ < 2 * i + 1 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : ↑j₁ < 2 * i + 2 → ↑j₂ < 2 * i + 2 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
specialize IHl (trans hj₁ (lt_child_left i)) (trans hj₂ (lt_child_left i))
Proof state after:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IHr : ↑j₁ < 2 * i + 2 → ↑j₂ < 2 * i + 2 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
IHr : ↑j₁ < 2 * i + 2 → ↑j₂ < 2 * i + 2 → IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
specialize IHr (trans hj₁ (lt_child_right i)) (trans hj₂ (lt_child_right i))
Proof state after:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ IsHeap lt (Subarray.swap x j₁ j₂) i
Tactic:
refine node' i hi ?_ ?_ IHl IHr
Proof state after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false

case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false

case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
. intro hl; specialize hx₁ hl
  simp only [Subarray.getElem_swap]
  iterate rewrite [if_neg]
  exact hx₁
  all_goals apply Nat.ne_of_lt
  . exact trans hj₁ (lt_child_left i)
  . exact trans hj₂ (lt_child_left i)
  . exact hj₁
  . exact hj₂
Proof state after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
. intro hr; specialize hx₂ hr
  simp only [Subarray.getElem_swap]
  iterate rewrite [if_neg]
  exact hx₂
  all_goals apply Nat.ne_of_lt
  . exact trans hj₁ (lt_child_right i)
  . exact trans hj₂ (lt_child_right i)
  . exact hj₁
  . exact hj₂
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Tactic:
intro hl
Proof state after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Tactic:
specialize hx₁ hl
Proof state after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 1] = false
Tactic:
simp only [Subarray.getElem_swap]
Proof state after:
case node'.refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ lt (if ↑j₂ = i then x[↑j₁] else if ↑j₁ = i then x[↑j₂] else x[i])
      (if ↑j₂ = 2 * i + 1 then x[↑j₁] else if ↑j₁ = 2 * i + 1 then x[↑j₂] else x[2 * i + 1]) =
    false
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < 2 * i + 1

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
. exact trans hj₂ (lt_child_left i)
Proof state after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i

case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
. exact hj₁
Proof state after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
. exact hj₂
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ¬↑j₂ = i
Tactic:
apply Nat.ne_of_lt
Proof state after:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < 2 * i + 1
Tactic:
exact trans hj₁ (lt_child_left i)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < 2 * i + 1
Tactic:
exact trans hj₂ (lt_child_left i)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₁ < i
Tactic:
exact hj₁
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_1.hnc.h
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hl : 2 * i + 1 < Subarray.size (Subarray.swap x j₁ j₂)
hx₁ : lt x[i] x[2 * i + 1] = false
⊢ ↑j₂ < i
Tactic:
exact hj₂
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)),
    lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
intro hr
Proof state after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.swap
Proof state before:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
hx₂ : ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false
Tactic:
specialize hx₂ hr
Proof state after:
case node'.refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i✝ : Nat
j₁ j₂ : Fin (Subarray.size x)
i : Nat
hi : i < Subarray.size x
hx₁ : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
a✝¹ : IsHeap lt x (2 * i + 1)
a✝ : IsHeap lt x (2 * i + 2)
hj₁ : ↑j₁ < i
hj₂ : ↑j₂ < i
IHl : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 1)
IHr : IsHeap lt (Subarray.swap x j₁ j₂) (2 * i + 2)
hr : 2 * i + 2 < Subarray.size (Subarray.swap x j₁ j₂)
hx₂ : lt x[i] x[2 * i + 2] = false
⊢ lt (Subarray.swap x j₁ j₂)[i] (Subarray.swap x j₁ j₂)[2 * i + 2] = false