internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[i] =
    x.as[i]

α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i <
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).start
Tactic:
all_goals simp only [Subarray.as_shrinkOne', Subarray.as_swap, Subarray.start_shrinkOne', Subarray.start_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ (Array.swap x.as (Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) })
        (Subarray.castIndex x
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }))[i] =
    x.as[i]

α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i < x.start
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ (Array.swap x.as (Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) })
        (Subarray.castIndex x
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }))[i] =
    x.as[i]

α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i < x.start
Tactic:
. refine Array.getElem_swap_ne x.as _ _ _ (Nat.ne_of_gt hlt) ?_
  exact Nat.ne_of_gt <| trans hlt (x.castIndex_ge_start _)
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i < x.start
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i < x.start
Tactic:
. exact hlt
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i <
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).start
Tactic:
simp only [Subarray.as_shrinkOne', Subarray.as_swap, Subarray.start_shrinkOne', Subarray.start_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i < x.start
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ (Array.swap x.as (Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) })
        (Subarray.castIndex x
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }))[i] =
    x.as[i]
Tactic:
refine Array.getElem_swap_ne x.as _ _ _ (Nat.ne_of_gt hlt) ?_
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }) ≠
    i
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }) ≠
    i
Tactic:
exact Nat.ne_of_gt <| trans hlt (x.castIndex_ge_start _)
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : x.start < x.stop
⊢ i < x.start
Tactic:
exact hlt
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_lt_start
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hlt : i < x.start
h : ¬x.start < x.stop
⊢ (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as[i] =
    x.as[i]
Tactic:
simp only [dif_neg h]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
⊢ (popMax lt x).as[i] = x.as[i]
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
⊢ (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as[i] =
    x.as[i]
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
⊢ (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as[i] =
    x.as[i]
Tactic:
if h : x.start < x.stop then
  simp only [dif_pos h]
  rewrite [get_as_heapifyDown_of_ge_stop lt _ 0 i]
  . simp only [Subarray.as_shrinkOne']
    refine Array.getElem_swap_ne x.as _ _ _ ?_ ?_
    . exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
    . exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
  . simp only [Subarray.stop_shrinkOne']
    exact Nat.le_trans x.stop.pred_le hge
else
  simp only [dif_neg h]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as[i] =
    x.as[i]
Tactic:
simp only [dif_pos h]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (heapifyDown lt
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
            (_ : x.start < x.stop))
          0).as[i] =
    x.as[i]
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (heapifyDown lt
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
            (_ : x.start < x.stop))
          0).as[i] =
    x.as[i]
Tactic:
rewrite [get_as_heapifyDown_of_ge_stop lt _ 0 i]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[i] =
    x.as[i]

α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ i ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[i] =
    x.as[i]

α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ i ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Tactic:
. simp only [Subarray.as_shrinkOne']
  refine Array.getElem_swap_ne x.as _ _ _ ?_ ?_
  . exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
  . exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ i ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ i ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Tactic:
. simp only [Subarray.stop_shrinkOne']
  exact Nat.le_trans x.stop.pred_le hge
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[i] =
    x.as[i]
Tactic:
simp only [Subarray.as_shrinkOne']
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).as[i] =
    x.as[i]
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).as[i] =
    x.as[i]
Tactic:
refine Array.getElem_swap_ne x.as _ _ _ ?_ ?_
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) }) ≠ i

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }) ≠
    i
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) }) ≠ i

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }) ≠
    i
Tactic:
. exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
Proof state after:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }) ≠
    i
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }) ≠
    i
Tactic:
. exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) }) ≠ i
Tactic:
exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ ↑(Subarray.castIndex x
        { val := Subarray.size x - 1,
          isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }) ≠
    i
Tactic:
exact Nat.ne_of_lt <| trans (x.castIndex_lt_stop _) hge
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ i ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Tactic:
simp only [Subarray.stop_shrinkOne']
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ i ≥
    (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).stop -
      1
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : x.start < x.stop
⊢ i ≥
    (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }).stop -
      1
Tactic:
exact Nat.le_trans x.stop.pred_le hge
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_of_ge_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Array.size (popMax lt x).as
hge : i ≥ x.stop
h : ¬x.start < x.stop
⊢ (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as[i] =
    x.as[i]
Tactic:
simp only [dif_neg h]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (popMax lt x).as[x.stop - 1] = x[0]
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as[x.stop - 1] =
    x[0]
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (if h : x.start < x.stop then
          let_fun this := (_ : 0 < x.stop - x.start);
          let x :=
            Subarray.swap x { val := 0, isLt := this }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
          heapifyDown lt (Subarray.shrinkOne' x h) 0
        else x).as[x.stop - 1] =
    x[0]
Tactic:
simp only [dif_pos hs]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (heapifyDown lt
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
            (_ : x.start < x.stop))
          0).as[x.stop - 1] =
    x[0]
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (heapifyDown lt
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
            (_ : x.start < x.stop))
          0).as[x.stop - 1] =
    x[0]
Tactic:
rewrite [get_as_heapifyDown_of_ge_stop lt _ 0 (x.stop-1)]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[x.stop - 1] =
    x[0]

α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[x.stop - 1] =
    x[0]

α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Tactic:
. simp only [Subarray.as_shrinkOne', Subarray.as_swap]
  simp only [Array.getElem_swap, Subarray.castIndex]
  rw [if_pos]; rfl
  rewrite [Subarray.size, ← Nat.add_sub_assoc (Nat.sub_pos_of_lt hs), Nat.add_sub_cancel' x.h₁]
  rfl
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop
Tactic:
. simp only [Subarray.stop_shrinkOne', Subarray.stop_swap]
  exact .refl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.get_as_popMax_stop_sub_one
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[x.stop - 1] =
    x[0]
Tactic:
simp only [Subarray.as_shrinkOne', Subarray.as_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (Array.swap x.as (Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) })
        (Subarray.castIndex x
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }))[x.stop - 1] =
    x[0]