internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
⊢ IsHeap lt x i
Tactic:
have hright : IsHeap lt x (2*i+2) :=
  .out_of_range _ hr
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ IsHeap lt x i
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ IsHeap lt x i
Tactic:
refine .node' i _ (fun _ => hx) ?_ hleft hright
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
. intro hr'; exact absurd hr' (Nat.not_lt_of_le hr)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ IsHeap lt x (2 * i + 1)
Tactic:
refine .leaf lt x _ (Nat.le_trans hr ?_)
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * (2 * i + 1) + 1
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * (2 * i + 1) + 1
Tactic:
conv =>
  rhs
  rewrite [Nat.two_mul (2*i+1), Nat.add_assoc _ _ 1, Nat.add_comm (2*i+1) 1, ←Nat.add_assoc _ 1 _]
  change 2*i+2+(2*i+1)
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * i + 2 + (2 * i + 1)
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
⊢ 2 * i + 2 ≤ 2 * i + 2 + (2 * i + 1)
Tactic:
exact Nat.le_add_right (2*i+2) (2*i+1)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
⊢ ∀ (x_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false
Tactic:
intro hr'
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.node_odd
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hl : 2 * i + 1 < Subarray.size x
hr : 2 * i + 2 ≥ Subarray.size x
hx : lt x[i] x[2 * i + 1] = false
hleft : IsHeap lt x (2 * i + 1)
hright : IsHeap lt x (2 * i + 2)
hr' : 2 * i + 2 < Subarray.size x
⊢ lt x[i] x[2 * i + 2] = false
Tactic:
exact absurd hr' (Nat.not_lt_of_le hr)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.descend
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i j : Nat
h : IsHeap lt x i
hd : Descendant i j
⊢ IsHeap lt x j
Tactic:
induction hd with
| refl => exact h
| node_left j _ IH => exact IH h.left
| node_right j _ IH => exact IH h.right
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.descend
Proof state before:
case refl
α : Type u
lt : α → α → Bool
x : Subarray α
i j : Nat
h : IsHeap lt x j
⊢ IsHeap lt x j
Tactic:
exact h
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.descend
Proof state before:
case node_left
α : Type u
lt : α → α → Bool
x : Subarray α
i j✝ j : Nat
h✝ : Descendant (2 * j + 1) j✝
IH : IsHeap lt x (2 * j + 1) → IsHeap lt x j✝
h : IsHeap lt x j
⊢ IsHeap lt x j✝
Tactic:
exact IH h.left
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.descend
Proof state before:
case node_right
α : Type u
lt : α → α → Bool
x : Subarray α
i j✝ j : Nat
h✝ : Descendant (2 * j + 2) j✝
IH : IsHeap lt x (2 * j + 2) → IsHeap lt x j✝
h : IsHeap lt x j
⊢ IsHeap lt x j✝
Tactic:
exact IH h.right
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
α : Type u
lt : α → α → Bool
x y : Subarray α
i : Nat
h : IsHeap lt x i
hsize : Subarray.size y ≤ Subarray.size x
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
Tactic:
induction h with
| out_of_range i hi =>
  exact .out_of_range i <| Nat.le_trans hsize hi
| node' i _ lt_left lt_right _ _ IH₁ IH₂ =>
  specialize IH₁ fun k hk h => hext k hk (.node_left _ h)
  specialize IH₂ fun k hk h => hext k hk (.node_right _ h)
  if hiy : i < y.size then
    refine .node' i hiy ?_ ?_ IH₁ IH₂
    . intro hl
      rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
      exact lt_left <| Nat.lt_of_lt_of_le hl hsize
    . intro hr
      rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
      exact lt_right <| Nat.lt_of_lt_of_le hr hsize
  else
    exact .out_of_range i (Nat.le_of_not_lt hiy)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case out_of_range
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
hi : i ≥ Subarray.size x
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
Tactic:
exact .out_of_range i <| Nat.le_trans hsize hi
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
IH₁ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 1) k → y[k] = x[k]) → IsHeap lt y (2 * i + 1)
IH₂ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]) → IsHeap lt y (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
⊢ IsHeap lt y i
Tactic:
specialize IH₁ fun k hk h => hext k hk (.node_left _ h)
Proof state after:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
IH₂ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]) → IsHeap lt y (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
⊢ IsHeap lt y i
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
IH₂ : (∀ (k : Nat) (hk : k < Subarray.size y), Descendant (2 * i + 2) k → y[k] = x[k]) → IsHeap lt y (2 * i + 2)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
⊢ IsHeap lt y i
Tactic:
specialize IH₂ fun k hk h => hext k hk (.node_right _ h)
Proof state after:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
⊢ IsHeap lt y i
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case node'
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
⊢ IsHeap lt y i
Tactic:
if hiy : i < y.size then
  refine .node' i hiy ?_ ?_ IH₁ IH₂
  . intro hl
    rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
    exact lt_left <| Nat.lt_of_lt_of_le hl hsize
  . intro hr
    rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
    exact lt_right <| Nat.lt_of_lt_of_le hr hsize
else
  exact .out_of_range i (Nat.le_of_not_lt hiy)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ IsHeap lt y i
Tactic:
refine .node' i hiy ?_ ?_ IH₁ IH₂
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 1 < Subarray.size y), lt y[i] y[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 1 < Subarray.size y), lt y[i] y[2 * i + 1] = false

case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Tactic:
. intro hl
  rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
  exact lt_left <| Nat.lt_of_lt_of_le hl hsize
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Tactic:
. intro hr
  rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
  exact lt_right <| Nat.lt_of_lt_of_le hr hsize
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 1 < Subarray.size y), lt y[i] y[2 * i + 1] = false
Tactic:
intro hl
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt y[i] y[2 * i + 1] = false
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt y[i] y[2 * i + 1] = false
Tactic:
rewrite [hext i hiy (.refl i), hext (2*i+1) hl (.child_left i)]
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt x[i] x[2 * i + 1] = false
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hl : 2 * i + 1 < Subarray.size y
⊢ lt x[i] x[2 * i + 1] = false
Tactic:
exact lt_left <| Nat.lt_of_lt_of_le hl hsize
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
⊢ ∀ (x : 2 * i + 2 < Subarray.size y), lt y[i] y[2 * i + 2] = false
Tactic:
intro hr
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt y[i] y[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt y[i] y[2 * i + 2] = false
Tactic:
rewrite [hext i hiy (.refl i), hext (2*i+2) hr (.child_right i)]
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt x[i] x[2 * i + 2] = false
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : i < Subarray.size y
hr : 2 * i + 2 < Subarray.size y
⊢ lt x[i] x[2 * i + 2] = false
Tactic:
exact lt_right <| Nat.lt_of_lt_of_le hr hsize
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.of_subext
Proof state before:
α : Type u
lt : α → α → Bool
x y : Subarray α
i✝ : Nat
hsize : Subarray.size y ≤ Subarray.size x
i : Nat
x✝ : i < Subarray.size x
lt_left : ∀ (x_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false
lt_right : ∀ (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)
hext : ∀ (k : Nat) (hk : k < Subarray.size y), Descendant i k → y[k] = x[k]
IH₁ : IsHeap lt y (2 * i + 1)
IH₂ : IsHeap lt y (2 * i + 2)
hiy : ¬i < Subarray.size y
⊢ IsHeap lt y i
Tactic:
exact .out_of_range i (Nat.le_of_not_lt hiy)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.not_lt_of_descendant
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i : Nat
h : IsHeap lt x i
j : Nat
hj : j < Subarray.size x
hd : Descendant i j
⊢ lt x[i] x[j] = false
Tactic:
induction hd with
| refl => exact LawfulLTBRel.irrefl _
| node_left i hd IH =>
  exact LawfulLTBRel.ntrans (h.not_lt_left _) (IH h.left)
| node_right i hd IH =>
  exact LawfulLTBRel.ntrans (h.not_lt_right _) (IH h.right)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.not_lt_of_descendant
Proof state before:
case refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i j : Nat
hj : j < Subarray.size x
h : IsHeap lt x j
⊢ lt x[j] x[j] = false
Tactic:
exact LawfulLTBRel.irrefl _
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.not_lt_of_descendant
Proof state before:
case node_left
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i✝ j : Nat
hj : j < Subarray.size x
i : Nat
hd : Descendant (2 * i + 1) j
IH : IsHeap lt x (2 * i + 1) → lt x[2 * i + 1] x[j] = false
h : IsHeap lt x i
⊢ lt x[i] x[j] = false
Tactic:
exact LawfulLTBRel.ntrans (h.not_lt_left _) (IH h.left)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.not_lt_of_descendant
Proof state before:
case node_right
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
i✝ j : Nat
hj : j < Subarray.size x
i : Nat
hd : Descendant (2 * i + 2) j
IH : IsHeap lt x (2 * i + 2) → lt x[2 * i + 2] x[j] = false
h : IsHeap lt x i
⊢ lt x[i] x[j] = false
Tactic:
exact LawfulLTBRel.ntrans (h.not_lt_right _) (IH h.right)
Proof state after:
no goals