internlm/Lean-Github huggingface dataset:
Theorem: Algdata.BinaryHeap.exists_get_mkHeap_loop
Proof state before:
case zero
α : Type u
lt : α → α → Bool
k : Nat
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt x Nat.zero)[k] = x[l]
Tactic:
exact ⟨k,hk,rfl⟩
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.exists_get_mkHeap_loop
Proof state before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt x (Nat.succ n))[k] = x[l]
Tactic:
dsimp [mkHeap.loop]
Proof state after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]
Theorem: Algdata.BinaryHeap.exists_get_mkHeap_loop
Proof state before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]
Tactic:
have ⟨l',hl',IH⟩ := IH (heapifyDown lt x n) (size_heapifyDown lt x n ▸ hk)
Proof state after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]
Theorem: Algdata.BinaryHeap.exists_get_mkHeap_loop
Proof state before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (mkHeap.loop lt (heapifyDown lt x n) n)[k] = x[l]
Tactic:
simp only [IH]
Proof state after:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (heapifyDown lt x n)[l'] = x[l]
Theorem: Algdata.BinaryHeap.exists_get_mkHeap_loop
Proof state before:
case succ
α : Type u
lt : α → α → Bool
k n : Nat
IH✝ : ∀ (x : Subarray α) (hk : k < Subarray.size x), ∃ l hl, (mkHeap.loop lt x n)[k] = x[l]
x : Subarray α
hk : k < Subarray.size x
l' : Nat
hl' : l' < Subarray.size (heapifyDown lt x n)
IH : (mkHeap.loop lt (heapifyDown lt x n) n)[k] = (heapifyDown lt x n)[l']
⊢ ∃ l hl, (heapifyDown lt x n)[l'] = x[l]
Tactic:
exact exists_get_heapifyDown lt x n l' (size_heapifyDown lt x n ▸ hl')
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.size_as_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Array.size (popMax lt x).as = Array.size x.as
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Array.size
      (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 =
    Array.size x.as
Theorem: Algdata.BinaryHeap.size_as_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Array.size
      (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 =
    Array.size x.as
Tactic:
if h : x.start < x.stop then
  simp only [dif_pos h, size_as_heapifyDown, Subarray.size_as_shrinkOne', Subarray.size_as_swap]
else
  simp only [dif_neg h]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.size_as_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ Array.size
      (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 =
    Array.size x.as
Tactic:
simp only [dif_pos h, size_as_heapifyDown, Subarray.size_as_shrinkOne', Subarray.size_as_swap]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.size_as_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : ¬x.start < x.stop
⊢ Array.size
      (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 =
    Array.size x.as
Tactic:
simp only [dif_neg h]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.start_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ (popMax lt x).start = x.start
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ (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).start =
    x.start
Theorem: Algdata.BinaryHeap.start_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ (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).start =
    x.start
Tactic:
if h : x.start < x.stop then
  simp only [dif_pos h, start_heapifyDown, Subarray.start_shrinkOne', Subarray.start_swap]
else
  simp only [dif_neg h]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.start_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
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).start =
    x.start
Tactic:
simp only [dif_pos h, start_heapifyDown, Subarray.start_shrinkOne', Subarray.start_swap]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.start_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
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).start =
    x.start
Tactic:
simp only [dif_neg h]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.stop_popMax_le_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ (popMax lt x).stop ≤ x.stop
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ (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).stop ≤
    x.stop
Theorem: Algdata.BinaryHeap.stop_popMax_le_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ (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).stop ≤
    x.stop
Tactic:
if h : x.start < x.stop then
  simp only [dif_pos h, stop_heapifyDown, Subarray.stop_shrinkOne', Subarray.stop_swap]
  exact x.stop.pred_le
else
  simp only [dif_neg h]; exact .refl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.stop_popMax_le_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
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).stop ≤
    x.stop
Tactic:
simp only [dif_pos h, stop_heapifyDown, Subarray.stop_shrinkOne', Subarray.stop_swap]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ x.stop - 1 ≤ x.stop
Theorem: Algdata.BinaryHeap.stop_popMax_le_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ x.stop - 1 ≤ x.stop
Tactic:
exact x.stop.pred_le
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.stop_popMax_le_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
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).stop ≤
    x.stop
Tactic:
simp only [dif_neg h]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
h : ¬x.start < x.stop
⊢ x.stop ≤ x.stop
Theorem: Algdata.BinaryHeap.stop_popMax_le_stop
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : ¬x.start < x.stop
⊢ x.stop ≤ x.stop
Tactic:
exact .refl
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.size_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Subarray.size (popMax lt x) = Subarray.size x - 1
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Subarray.size
      (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) =
    Subarray.size x - 1
Theorem: Algdata.BinaryHeap.size_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
⊢ Subarray.size
      (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) =
    Subarray.size x - 1
Tactic:
cases Nat.lt_or_eq_of_le x.h₁ with
| inl hlt =>
  simp only [dif_pos hlt, size_heapifyDown, Subarray.size_shrinkOne', Subarray.size_swap]
| inr heq =>
  rewrite [dif_neg (c:=x.start < x.stop) (heq ▸ x.start.lt_irrefl)]
  simp only [Subarray.size, heq, x.stop.sub_self]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.size_popMax
Proof state before:
case inl
α : Type u
lt : α → α → Bool
x : Subarray α
hlt : x.start < x.stop
⊢ Subarray.size
      (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) =
    Subarray.size x - 1
Tactic:
simp only [dif_pos hlt, size_heapifyDown, Subarray.size_shrinkOne', Subarray.size_swap]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.size_popMax
Proof state before:
case inr
α : Type u
lt : α → α → Bool
x : Subarray α
heq : x.start = x.stop
⊢ Subarray.size
      (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) =
    Subarray.size x - 1
Tactic:
rewrite [dif_neg (c:=x.start < x.stop) (heq ▸ x.start.lt_irrefl)]
Proof state after:
case inr
α : Type u
lt : α → α → Bool
x : Subarray α
heq : x.start = x.stop
⊢ Subarray.size x = Subarray.size x - 1
Theorem: Algdata.BinaryHeap.size_popMax
Proof state before:
case inr
α : Type u
lt : α → α → Bool
x : Subarray α
heq : x.start = x.stop
⊢ Subarray.size x = Subarray.size x - 1
Tactic:
simp only [Subarray.size, heq, x.stop.sub_self]
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.stop_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ (popMax lt x).stop = x.stop - 1
Tactic:
delta popMax
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
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).stop =
    x.stop - 1
Theorem: Algdata.BinaryHeap.stop_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
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).stop =
    x.stop - 1
Tactic:
simp only [dif_pos h, stop_heapifyDown]
Proof state after:
α : Type u
lt : α → α → Bool
x : Subarray α
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)).stop =
    x.stop - 1
Theorem: Algdata.BinaryHeap.stop_popMax
Proof state before:
α : Type u
lt : α → α → Bool
x : Subarray α
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)).stop =
    x.stop - 1
Tactic:
refine Eq.trans (Subarray.stop_shrinkOne' _ ?_) ?_
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
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) }).start <
    (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

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
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) }).stop -
      1 =
    x.stop - 1
Theorem: Algdata.BinaryHeap.stop_popMax
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
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) }).start <
    (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

case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
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) }).stop -
      1 =
    x.stop - 1
Tactic:
all_goals simp only [Subarray.stop_swap, Subarray.start_swap]
Proof state after:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ x.start < x.stop
Theorem: Algdata.BinaryHeap.stop_popMax
Proof state before:
case refine_1
α : Type u
lt : α → α → Bool
x : Subarray α
h : x.start < x.stop
⊢ x.start < x.stop
Tactic:
exact h
Proof state after:
no goals
Theorem: Algdata.BinaryHeap.stop_popMax
Proof state before:
case refine_2
α : Type u
lt : α → α → Bool
x : Subarray α
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) }).stop -
      1 =
    x.stop - 1
Tactic:
simp only [Subarray.stop_swap, Subarray.start_swap]
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
⊢ (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
hlt : i < x.start
⊢ (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_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
⊢ (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_lt_start lt _ 0 i]
  all_goals simp only [Subarray.as_shrinkOne', Subarray.as_swap, Subarray.start_shrinkOne', Subarray.start_swap]
  . refine Array.getElem_swap_ne x.as _ _ _ (Nat.ne_of_gt hlt) ?_
    exact Nat.ne_of_gt <| trans hlt (x.castIndex_ge_start _)
  . exact hlt
else
  simp only [dif_neg h]
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_pos h]
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
⊢ (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_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
⊢ (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_lt_start lt _ 0 i]
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.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