internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof state before:
case node_next_right.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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
h : heapifyDown.OpSpec lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * i + 2) y
IH :
  ∀
    (heap_left :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 1))
    (heap_right :
      IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr }) (2 * (2 * i + 2) + 2)),
    let _hy_left :=
      (_ :
        ∀
          (hl :
            2 * (2 * i + 2) + 1 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 1] = false);
    let _hy_right :=
      (_ :
        ∀
          (hr_1 :
            2 * (2 * i + 2) + 2 <
              Subarray.size (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 2, isLt := hr })),
          lt y[2 * i + 2] y[2 * (2 * i + 2) + 2] = false);
    IsHeap lt y (2 * i + 2)
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt y[i] y[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_next_right x i y hi hl hr hx' hx h) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt y[i] y[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_next_right x i y hi hl hr hx' hx h) hr_1 heap_right
⊢ ↑{ val := i, isLt := hi } < 2 * (2 * i + 2) + 2
Tactic:
exact trans (lt_child_right i) (lt_child_right (2*i+2))
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof state before:
case node_end_right
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl => not_lt_left (node_end_right x i hi✝ hl✝ hr hx' hx) hl heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_end_right x i hi✝ hl✝ hr hx' hx) hr_1 heap_right
⊢ IsHeap lt x i
Tactic:
exact .node lt x i hr (LawfulLTBRel.ntrans hx hx') hx heap_left heap_right
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof state before:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ IsHeap lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl }) i
Tactic:
refine .node_odd lt _ i hl hr ?_
Proof state after:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof state before:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false
Tactic:
rewrite [Subarray.getElem_swap_left, Subarray.getElem_swap_right]
Proof state after:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt x[↑{ val := 2 * i + 1, isLt := hl }] x[↑{ val := i, isLt := hi }] = false
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof state before:
case node_odd_next
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 1] =
    false :=
  fun hl_1 => not_lt_left (node_odd_next x i hi hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x),
  lt (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[i]
      (Subarray.swap x { val := i, isLt := hi } { val := 2 * i + 1, isLt := hl })[2 * i + 2] =
    false :=
  fun hr_1 => not_lt_right (node_odd_next x i hi hl hr hx) hr_1 heap_right
⊢ lt x[↑{ val := 2 * i + 1, isLt := hl }] x[↑{ val := i, isLt := hi }] = false
Tactic:
exact LawfulLTBRel.asymm hx
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof state before:
case node_odd_end
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
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] = false
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (node_odd_end x i hi✝ hl hr hx) hl_1 heap_left
_hy_right : ∀ (hr_1 : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr_1 => not_lt_right (node_odd_end x i hi✝ hl hr hx) hr_1 heap_right
⊢ IsHeap lt x i
Tactic:
exact .node_odd lt x i hl hr hx
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapifyDown.OpSpec.is_heap
Proof state before:
case leaf
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
i✝ : Nat
y x : Subarray α
i : Nat
hl : 2 * i + 1 ≥ Subarray.size x
heap_left : IsHeap lt x (2 * i + 1)
heap_right : IsHeap lt x (2 * i + 2)
_hy_left : ∀ (hl_1 : 2 * i + 1 < Subarray.size x), lt x[i] x[2 * i + 1] = false :=
  fun hl_1 => not_lt_left (leaf x i hl) hl_1 heap_left
_hy_right : ∀ (hr : 2 * i + 2 < Subarray.size x), lt x[i] x[2 * i + 2] = false :=
  fun hr => not_lt_right (leaf x i hl) hr heap_right
⊢ IsHeap lt x i
Tactic:
exact .leaf lt x i hl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (mkHeap lt x) 0
Tactic:
rewrite [mkHeap_eq_foldRev]
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x) 0
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ IsHeap lt (Nat.foldRev (fun n x => heapifyDown lt x n) (Subarray.size x / 2) x) 0
Tactic:
refine Nat.foldRev_induction (motive:=fun n x => ∀ k, n ≤ k → IsHeap lt x k) _ _ x ?_ ?_ 0 .refl
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Tactic:
. show ∀ k, x.size / 2 ≤ k → IsHeap lt x k
  intro k hk
  refine .leaf lt x k ?_
  rewrite [← Nat.div_add_mod x.size 2]
  refine Nat.add_le_add ?_ ?_
  . exact Nat.mul_le_mul_left 2 hk
  . apply Nat.le_of_succ_le_succ
    exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Tactic:
. show ∀ (n : Nat) (x : Subarray α), (∀ k, n+1 ≤ k → IsHeap lt x k) → ∀ k, n ≤ k → IsHeap lt (heapifyDown lt x n) k
  clear x; intro n x IH k hk
  if hk' : Descendant n k then
    suffices IsHeap lt (heapifyDown lt x n) n from
      this.descend hk'
    have : n ≤ 2 * n := by
      rewrite [Nat.two_mul]; exact Nat.le_add_left n n
    refine is_heap_heapifyDown lt x n ?_ ?_
    all_goals apply IH; apply Nat.succ_le_succ
    . exact this
    . exact .step this
  else
    have : n < k := Nat.lt_of_not_le fun h => by
      cases Nat.le_antisymm hk h
      exact hk' (.refl _)
    refine .of_subext (IH k this) (Nat.le_of_eq <| size_heapifyDown lt x _) ?_
    intro i hi hki
    suffices ¬ Descendant n i from
      get_heapifyDown_not_descendant lt x n i this
    intro hni
    exact hk' <| Descendant.ascend_right hk hni hki
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (Subarray.size x / 2) x
Tactic:
show ∀ k, x.size / 2 ≤ k → IsHeap lt x k
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat), Subarray.size x / 2 ≤ k → IsHeap lt x k
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat), Subarray.size x / 2 ≤ k → IsHeap lt x k
Tactic:
intro k hk
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ IsHeap lt x k
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ IsHeap lt x k
Tactic:
refine .leaf lt x k ?_
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ Subarray.size x
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ Subarray.size x
Tactic:
rewrite [← Nat.div_add_mod x.size 2]
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ 2 * (Subarray.size x / 2) + Subarray.size x % 2
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * k + 1 ≥ 2 * (Subarray.size x / 2) + Subarray.size x % 2
Tactic:
refine Nat.add_le_add ?_ ?_
Proof state after:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * (Subarray.size x / 2) ≤ 2 * k

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * (Subarray.size x / 2) ≤ 2 * k

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Tactic:
. exact Nat.mul_le_mul_left 2 hk
Proof state after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Tactic:
. apply Nat.le_of_succ_le_succ
  exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 * (Subarray.size x / 2) ≤ 2 * k
Tactic:
exact Nat.mul_le_mul_left 2 hk
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Subarray.size x % 2 ≤ 1
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
case refine_1.refine_2.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Nat.succ (Subarray.size x % 2) ≤ Nat.succ 1
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1.refine_2.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ Nat.succ (Subarray.size x % 2) ≤ Nat.succ 1
Tactic:
exact show x.size % 2 < 2 from Nat.mod_lt x.size (by decide)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
k : Nat
hk : Subarray.size x / 2 ≤ k
⊢ 2 > 0
Tactic:
decide
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (k : Nat) (a : Subarray α),
    (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) (k + 1) a →
      (fun n x => ∀ (k : Nat), n ≤ k → IsHeap lt x k) k (heapifyDown lt a k)
Tactic:
show ∀ (n : Nat) (x : Subarray α), (∀ k, n+1 ≤ k → IsHeap lt x k) → ∀ k, n ≤ k → IsHeap lt (heapifyDown lt x n) k
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k
Tactic:
clear x
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
⊢ ∀ (n : Nat) (x : Subarray α),
    (∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k) → ∀ (k : Nat), n ≤ k → IsHeap lt (heapifyDown lt x n) k
Tactic:
intro n x IH k hk
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
⊢ IsHeap lt (heapifyDown lt x n) k
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
⊢ IsHeap lt (heapifyDown lt x n) k
Tactic:
if hk' : Descendant n k then
  suffices IsHeap lt (heapifyDown lt x n) n from
    this.descend hk'
  have : n ≤ 2 * n := by
    rewrite [Nat.two_mul]; exact Nat.le_add_left n n
  refine is_heap_heapifyDown lt x n ?_ ?_
  all_goals apply IH; apply Nat.succ_le_succ
  . exact this
  . exact .step this
else
  have : n < k := Nat.lt_of_not_le fun h => by
    cases Nat.le_antisymm hk h
    exact hk' (.refl _)
  refine .of_subext (IH k this) (Nat.le_of_eq <| size_heapifyDown lt x _) ?_
  intro i hi hki
  suffices ¬ Descendant n i from
    get_heapifyDown_not_descendant lt x n i this
  intro hni
  exact hk' <| Descendant.ascend_right hk hni hki
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) k
Tactic:
suffices IsHeap lt (heapifyDown lt x n) n from
  this.descend hk'
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) n
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
⊢ IsHeap lt (heapifyDown lt x n) n
Tactic:
have : n ≤ 2 * n := by
  rewrite [Nat.two_mul]; exact Nat.le_add_left n n
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt (heapifyDown lt x n) n
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt (heapifyDown lt x n) n
Tactic:
refine is_heap_heapifyDown lt x n ?_ ?_
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 2)
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 2)
Tactic:
all_goals apply IH; apply Nat.succ_le_succ
Proof state after:
case refine_1.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n

case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_1.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n

case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1
Tactic:
. exact this
Proof state after:
case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_2.a.a
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
k : Nat
hk : n ≤ k
hk' : Descendant n k
this : n ≤ 2 * n
⊢ n ≤ 2 * n + 1
Tactic:
. exact .step this
Proof state after:
no goals