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
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)
Tactic:
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)
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
hi : i < Subarray.size x
hx : lt x[i] x[lhs] = true
⊢ 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:
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
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })
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
hi : i < Subarray.size x
hx : lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })
Tactic:
exact node_odd_next x i hi hl (Nat.le_of_not_lt hr) 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
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : ¬lt x[i] x[lhs] = true
⊢ 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:
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
hl : lhs < Subarray.size x
hi : i < Subarray.size x
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
hl : lhs < Subarray.size x
hi : i < Subarray.size x
hx : ¬lt x[i] x[lhs] = true
⊢ heapifyDown.OpSpec lt x i x
Tactic:
exact node_odd_end x i hi hl (Nat.le_of_not_lt hr) (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
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 only [dif_neg hr, dif_neg 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 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 x
Tactic:
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 α) ×' Nat
a✝¹ :
  ∀ (y : (_ : Subarray α) ×' Nat),
    (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1 y _x✝ →
      heapifyDown.OpSpec lt y.1 y.2 (heapifyDown lt y.1 y.2)
x : Subarray α
i : Nat
a✝ :
  ∀ (y : (_ : Subarray α) ×' Nat),
    (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1 y
        { fst := x, snd := i } →
      heapifyDown.OpSpec lt y.1 y.2 (heapifyDown lt y.1 y.2)
lhs : Nat := 2 * i + 1
rhs : Nat := lhs + 1
hr : rhs < Subarray.size x
j : Nat := if h : lt x[rhs] x[lhs] = true then lhs else rhs
_hdecreasing : Subarray.size x - j < Subarray.size x - i
⊢ (invImage (fun a => PSigma.casesOn a fun x snd => Subarray.size x - snd) instWellFoundedRelation).1
    {
      fst :=
        Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) } { val := j, isLt := (_ : j < Subarray.size x) },
      snd := j }
    { fst := x, snd := i }
Tactic:
exact _hdecreasing
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
y : Subarray α
h : heapifyDown.OpSpec lt x i y
⊢ y = heapifyDown lt x i
Tactic:
induction h with
| node_next_left x i y hi hl hr hx' hx _ IH =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_pos hx', if_pos hx]
  exact IH
| node_end_left x i hi hl hr hx' hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_pos hx', if_neg (Bool.eq_false_iff.mp hx)]
| node_next_right x i y hi hl hr hx' hx _ IH =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_pos hx]
  exact IH
| node_end_right x i hi hl hr hx' hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_neg (Bool.eq_false_iff.mp hx)]
| node_odd_next x i hi hl hr hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_pos hx]
| node_odd_end x i hi hl hr hx =>
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_pos hl, if_neg (Bool.eq_false_iff.mp hx)]
| leaf x i hl =>
  have hr : 2*i+2 ≥ x.size := .step hl
  unfold heapifyDown heapifyDownAux
  simp only [dif_neg (Nat.not_lt_of_le hr), dif_neg (Nat.not_lt_of_le hl)]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_next_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
Proof state after:
case node_next_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_next_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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 only [dif_pos hr, if_pos hx', if_pos hx]
Proof state after:
case node_next_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1, isLt := (_ : 2 * i + 1 < Subarray.size x) })
      (2 * i + 1)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_next_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) (2 * i + 1)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1, isLt := (_ : 2 * i + 1 < Subarray.size x) })
      (2 * i + 1)
Tactic:
exact IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_end_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = false
⊢ x = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
Proof state after:
case node_end_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = false
⊢ x =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_end_left
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = true
hx : lt x[i] x[2 * i + 1] = false
⊢ x =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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 only [dif_pos hr, if_pos hx', if_neg (Bool.eq_false_iff.mp hx)]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_next_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
Proof state after:
case node_next_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_next_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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 only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_pos hx]
Proof state after:
case node_next_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1 + 1, isLt := (_ : 2 * i + 1 + 1 < Subarray.size x) })
      (2 * i + 1 + 1)
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_next_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y✝ x : Subarray α
i : Nat
y : Subarray α
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = true
a✝ : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH : y = heapifyDown lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2)
⊢ y =
    heapifyDownAux lt
      (Subarray.swap x { val := i, isLt := (_ : i < Subarray.size x) }
        { val := 2 * i + 1 + 1, isLt := (_ : 2 * i + 1 + 1 < Subarray.size x) })
      (2 * i + 1 + 1)
Tactic:
exact IH
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_end_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = false
⊢ x = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
Proof state after:
case node_end_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = false
⊢ x =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_end_right
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 < Subarray.size x
hx' : lt x[2 * i + 2] x[2 * i + 1] = false
hx : lt x[i] x[2 * i + 2] = false
⊢ x =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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 only [dif_pos hr, if_neg (Bool.eq_false_iff.mp hx'), if_neg (Bool.eq_false_iff.mp hx)]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.to_eq
Proof state before:
case node_odd_next
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = true
⊢ Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl } = heapifyDown lt x i
Tactic:
unfold heapifyDown heapifyDownAux
Proof state after:
case node_odd_next
α : Type u
lt : α → α → Bool
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hi : i < Subarray.size x
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = true
⊢ Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl } =
    let lhs := 2 * i + 1;
    let rhs := lhs + 1;
    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