internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : lt x[rhs] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
have hjl : j = lhs := if_pos hx'
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
simp (config:={zeta:=false}) only [hjl] at IH ⊢
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)
Tactic:
if hx : lt x[i] x[lhs] then
  simp only [if_pos hx]
  exact node_next_left x i _ hi hl hr hx' hx IH
else
  simp only [if_neg hx]
  exact node_end_left x i hi hl hr hx' (Bool.of_not_eq_true hx)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)
Tactic:
simp only [if_pos hx]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := (_ : lhs < Subarray.size x) }) (2 * i + 1))
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := (_ : lhs < Subarray.size x) }) (2 * i + 1))
Tactic:
exact node_next_left x i _ hi hl hr hx' hx IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
        lhs
    else x)
Tactic:
simp only [if_neg hx]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i x
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : lt x[rhs] x[lhs] = true
hjl : j = lhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) })
    lhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := (_ : lhs < Subarray.size x) }) lhs)
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i x
Tactic:
exact node_end_left x i hi hl hr hx' (Bool.of_not_eq_true hx)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : ¬lt x[rhs] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
have hjr : j = rhs := if_neg hx'
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j)
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[j] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
    else x)
Tactic:
simp (config:={zeta:=false}) only [hjr] at IH ⊢
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)
Tactic:
if hx : lt x[i] x[rhs] then
  simp only [if_pos hx]
  exact node_next_right x i _ hi hl hr (Bool.of_not_eq_true hx') hx IH
else
  simp only [if_neg hx]
  exact node_end_right x i hi hl hr (Bool.of_not_eq_true hx') (Bool.of_not_eq_true hx)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)
Tactic:
simp only [if_pos hx]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1 + 1, isLt := (_ : rhs < Subarray.size x) })
      (2 * i + 1 + 1))
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1 + 1, isLt := (_ : rhs < Subarray.size x) })
      (2 * i + 1 + 1))
Tactic:
exact node_next_right x i _ hi hl hr (Bool.of_not_eq_true hx') hx IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : ¬lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[rhs] = true then
      heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
        rhs
    else x)
Tactic:
simp only [if_neg hx]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : ¬lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i x
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
hi : i < Subarray.size x
hl : lhs < Subarray.size x
j : Nat := if lt x[rhs] x[lhs] = true then lhs else rhs
hj : i < j ∧ j < Subarray.size x
this _hdecreasing : Subarray.size x - j < Subarray.size x - i
hx' : ¬lt x[rhs] x[lhs] = true
hjr : j = rhs
IH :
  heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) })
    rhs
    (heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := rhs, isLt := (_ : rhs < Subarray.size x) }) rhs)
hx : ¬lt x[i] x[rhs] = true
⊢ heapifyDown.OpSpec lt x i x
Tactic:
exact node_end_right x i hi hl hr (Bool.of_not_eq_true hx') (Bool.of_not_eq_true hx)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
if hl : lhs < x.size then
simp (config:={zeta:=false,beta:=false}) only [dif_neg hr, dif_pos hl]
takeout_lets; intro_let
if hx : lt x[i] x[lhs] then
simp only [if_pos hx]
exact node_odd_next x i hi hl (Nat.le_of_not_lt hr) hx
else
simp only [if_neg hx]
exact node_odd_end x i hi hl (Nat.le_of_not_lt hr) (Bool.of_not_eq_true hx)
else
simp only [dif_neg hr, dif_neg hl]
exact leaf x i (Nat.le_of_not_lt hl)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if hr : rhs < Subarray.size x then
      let_fun hi := (_ : i < Subarray.size x);
      let_fun hl := (_ : lhs < Subarray.size x);
      let j := if lt x[rhs] x[lhs] = true then lhs else rhs;
      let_fun hj := (_ : i < j ∧ j < Subarray.size x);
      if lt x[i] x[j] = true then
        let_fun this := (_ : Subarray.size x - j < Subarray.size x - i);
        heapifyDownAux lt (Subarray.swap x { val := i, isLt := hi } { val := j, isLt := (_ : j < Subarray.size x) }) j
      else x
    else
      if hl : lhs < Subarray.size x then
        let_fun hi := (_ : i < Subarray.size x);
        if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x
      else x)
Tactic:
simp (config:={zeta:=false,beta:=false}) only [dif_neg hr, dif_pos hl]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (let_fun hi := (_ : i < Subarray.size x);
    if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (let_fun hi := (_ : i < Subarray.size x);
    if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Tactic:
takeout_lets
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ let_fun hi := (_ : i < Subarray.size x);
  heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.mk
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
⊢ let_fun hi := (_ : i < Subarray.size x);
  heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)
Tactic:
intro_let
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : ¬rhs < Subarray.size x
hl : lhs < Subarray.size x
hi : i < Subarray.size x
⊢ heapifyDown.OpSpec lt x i
    (if lt x[i] x[lhs] = true then Subarray.swap x { val := i, isLt := hi } { val := lhs, isLt := hl } else x)