internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
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
Tactic:
. exact Nat.ne_of_lt hki.le
Proof state after:
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
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
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
Tactic:
. 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_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
Tactic:
exact Nat.ne_of_lt hki.le
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
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
Tactic:
refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
Proof state after:
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
⊢ 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) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
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
⊢ 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) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }
Tactic:
simp only [Subarray.size_shrinkOne', Subarray.size_swap]
Proof state after:
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
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
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
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1
Tactic:
exact .refl
Proof state after:
no goals
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 ?_ ?_
Proof state after:
case refine_2.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_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)),
    Descendant (2 * 0 + 2) 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_2.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_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)),
    Descendant (2 * 0 + 2) 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_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)),
    Descendant (2 * 0 + 2) 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_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)),
    Descendant (2 * 0 + 2) 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
  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_2.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_2.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_2.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_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)),
    Descendant (2 * 0 + 2) 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_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 + 2) 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_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 + 2) 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:
refine Subarray.getElem_swap_ne _ _ _ k ?_ ?_
Proof state after:
case refine_2.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 + 2) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_2.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 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_2.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 + 2) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k

case refine_2.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 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
. exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
Proof state after:
case refine_2.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 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_2.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 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
. 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_2.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 + 2) k
⊢ ↑{ val := 0, isLt := (_ : 0 < x.stop - x.start) } ≠ k
Tactic:
exact Nat.ne_of_lt <| Nat.lt_trans Nat.zero_lt_one hki.le
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_2.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 + 2) k
⊢ ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) } ≠ k
Tactic:
refine Nat.ne_of_gt <| Nat.lt_of_lt_of_le hk ?_
Proof state after:
case refine_2.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 + 2) 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) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_2.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 + 2) 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) ≤
    ↑{ val := Subarray.size x - 1, isLt := (_ : Nat.pred (Subarray.size x) < Subarray.size x) }
Tactic:
simp only [Subarray.size_shrinkOne', Subarray.size_swap]
Proof state after:
case refine_2.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 + 2) k
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1
Theorem: Algdata.BinaryHeap.IsHeap.popMax
Proof state before:
case refine_2.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 + 2) k
⊢ Subarray.size x - 1 ≤ Subarray.size x - 1
Tactic:
exact .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
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_neg 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 x 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 x 0
Tactic:
exact h
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
⊢ lt (BinaryHeap.popMax lt x).as[i] (BinaryHeap.popMax lt x)[k] = false
Tactic:
have ⟨k',hk',_ ,h⟩ := exists_get_popMax lt x k (size_popMax lt x ▸ hk)
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h✝ : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
h : (BinaryHeap.popMax lt x)[k] = x[k']
⊢ lt (BinaryHeap.popMax lt x).as[i] (BinaryHeap.popMax lt x)[k] = false
Theorem: Algdata.BinaryHeap.heapSort.Intermed.popMax
Proof state before:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h✝ : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
h : (BinaryHeap.popMax lt x)[k] = x[k']
⊢ lt (BinaryHeap.popMax lt x).as[i] (BinaryHeap.popMax lt x)[k] = false
Tactic:
rewrite [h]
Proof state after:
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h✝ : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
h : (BinaryHeap.popMax lt x)[k] = x[k']
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false