internlm/Lean-Github huggingface dataset:
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
⊢ n ≤ 2 * n
Tactic:
rewrite [Nat.two_mul]
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
⊢ n ≤ 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
⊢ n ≤ n + n
Tactic:
exact Nat.le_add_left n n
Proof state after:
no goals
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
hk' : Descendant n k
this : n ≤ 2 * n
⊢ IsHeap lt x (2 * n + 2)
Tactic:
apply IH
Proof state after:
case refine_2.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 + 1 ≤ 2 * n + 2
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refine_2.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 + 1 ≤ 2 * n + 2
Tactic:
apply Nat.succ_le_succ
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_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
Tactic:
exact this
Proof state after:
no goals
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
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:
have : n < k := Nat.lt_of_not_le fun h => by
  cases Nat.le_antisymm hk h
  exact hk' (.refl _)
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 < k
⊢ IsHeap lt (heapifyDown lt x n) k
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 < k
⊢ IsHeap lt (heapifyDown lt x n) k
Tactic:
refine .of_subext (IH k this) (Nat.le_of_eq <| size_heapifyDown lt x _) ?_
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 < k
⊢ ∀ (k_1 : Nat) (hk : k_1 < Subarray.size (heapifyDown lt x n)), Descendant k k_1 → (heapifyDown lt x n)[k_1] = x[k_1]
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 < k
⊢ ∀ (k_1 : Nat) (hk : k_1 < Subarray.size (heapifyDown lt x n)), Descendant k k_1 → (heapifyDown lt x n)[k_1] = x[k_1]
Tactic:
intro i hi hki
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 < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ (heapifyDown lt x n)[i] = x[i]
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 < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ (heapifyDown lt x n)[i] = x[i]
Tactic:
suffices ¬ Descendant n i from
  get_heapifyDown_not_descendant lt x n i this
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 < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ ¬Descendant n i
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 < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
⊢ ¬Descendant n i
Tactic:
intro hni
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 < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
hni : Descendant n i
⊢ False
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 < k
i : Nat
hi : i < Subarray.size (heapifyDown lt x n)
hki : Descendant k i
hni : Descendant n i
⊢ False
Tactic:
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
h : k ≤ n
⊢ False
Tactic:
cases Nat.le_antisymm hk h
Proof state after:
case refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
hk : n ≤ n
hk' : ¬Descendant n n
h : n ≤ n
⊢ False
Theorem: Algdata.BinaryHeap.is_heap_mkHeap
Proof state before:
case refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
n : Nat
x : Subarray α
IH : ∀ (k : Nat), n + 1 ≤ k → IsHeap lt x k
hk : n ≤ n
hk' : ¬Descendant n n
h : n ≤ n
⊢ False
Tactic:
exact hk' (.refl _)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
⊢ IsHeap lt (BinaryHeap.popMax lt x) 0
Tactic:
dsimp [BinaryHeap.popMax]
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
Tactic:
if hsize : x.start < x.stop then
  simp only [dif_pos hsize]
  refine is_heap_heapifyDown lt _ 0 ?_ ?_
  . refine h.left.of_subext ?_ ?_
    . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
    . intro k hk hki
      rewrite [Subarray.getElem_shrinkOne']
      refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
      . exact Nat.ne_of_lt hki.le
      . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
        simp only [Subarray.size_shrinkOne', Subarray.size_swap]
        exact .refl
  . refine h.right.of_subext ?_ ?_
    . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
    . intro k hk hki
      refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
      . exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
      . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
        simp only [Subarray.size_shrinkOne', Subarray.size_swap]
        exact .refl
else
  simp only [dif_neg hsize]; exact h
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (if h : x.start < x.stop then
      heapifyDown lt
        (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
          h)
        0
    else x)
    0
Tactic:
simp only [dif_pos hsize]
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (heapifyDown lt
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
      0)
    0
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (heapifyDown lt
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
      0)
    0
Tactic:
refine is_heap_heapifyDown lt _ 0 ?_ ?_
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 1)

case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)
Tactic:
. refine h.left.of_subext ?_ ?_
  . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
  . intro k hk hki
    rewrite [Subarray.getElem_shrinkOne']
    refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
    . exact Nat.ne_of_lt hki.le
    . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
      simp only [Subarray.size_shrinkOne', Subarray.size_swap]
      exact .refl
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 2)
Tactic:
. refine h.right.of_subext ?_ ?_
  . rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
  . intro k hk hki
    refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
    . exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
    . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
      simp only [Subarray.size_shrinkOne', Subarray.size_swap]
      exact .refl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ IsHeap lt
    (Subarray.shrinkOne'
      (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
      hsize)
    (2 * 0 + 1)
Tactic:
refine h.left.of_subext ?_ ?_
Proof state after:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x

case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
. rewrite [Subarray.size_shrinkOne', Subarray.size_swap]; exact x.size.pred_le
Proof state after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
. intro k hk hki
  rewrite [Subarray.getElem_shrinkOne']
  refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
  . exact Nat.ne_of_lt hki.le
  . refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
    simp only [Subarray.size_shrinkOne', Subarray.size_swap]
    exact .refl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize) ≤
    Subarray.size x
Tactic:
rewrite [Subarray.size_shrinkOne', Subarray.size_swap]
Proof state after:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size x - 1 ≤ Subarray.size x
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ Subarray.size x - 1 ≤ Subarray.size x
Tactic:
exact x.size.pred_le
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
⊢ ∀ (k : Nat)
    (hk :
      k <
        Subarray.size
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)),
    Descendant (2 * 0 + 1) k →
      (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
            hsize)[k] =
        x[k]
Tactic:
intro k hk hki
Proof state after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)[k] =
    x[k]
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)[k] =
    x[k]
Tactic:
rewrite [Subarray.getElem_shrinkOne']
Proof state after:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })[k] =
    x[k]
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_1.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
        { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })[k] =
    x[k]
Tactic:
refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
Proof state after:
case refine_1.refine_2.refine_1
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_1.refine_2.refine_2
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
h : IsHeap lt x 0
hsize : x.start < x.stop
k : Nat
hk :
  k <
    Subarray.size
      (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) })
        hsize)
hki : Descendant (2 * 0 + 1) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k