internlm/Lean-Github huggingface dataset:
Theorem: project.children_IsMinHeap
Proof state before:
case mk.cons.heap.nil.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt :
  IsMinTree le { val := val, rank := rank, children := Heap.heap nodes }.val
    (Heap.nodes { val := val, rank := rank, children := Heap.heap nodes }.children)
⊢ IsMinHeap le (Heap.heap nodes)
Tactic:
dsimp at mt
Proof state after:
case mk.cons.heap.nil.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinHeap le (Heap.heap nodes)
Theorem: project.children_IsMinHeap
Proof state before:
case mk.cons.heap.nil.mk
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinHeap le (Heap.heap nodes)
Tactic:
apply IsMinHeap_of_IsMinTree
Proof state after:
case mk.cons.heap.nil.mk.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinTree le ?mk.cons.heap.nil.mk.val nodes

case mk.cons.heap.nil.mk.val
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ α
Theorem: project.children_IsMinHeap
Proof state before:
case mk.cons.heap.nil.mk.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinTree le ?mk.cons.heap.nil.mk.val nodes

case mk.cons.heap.nil.mk.val
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ α
Tactic:
repeat assumption
Proof state after:
no goals
Theorem: project.children_IsMinHeap
Proof state before:
case mk.cons.heap.nil.mk.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ IsMinTree le ?mk.cons.heap.nil.mk.val nodes

case mk.cons.heap.nil.mk.val
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
val : α
rank : ℕ
nodes : List (HeapNodeAux α (Heap α))
mt : IsMinTree le val nodes
⊢ α
Tactic:
assumption
Proof state after:
no goals
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
id : ℕ
⊢ IsHeapForest' r (List.eraseIdx [] id)
Tactic:
simp
Proof state after:
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
id : ℕ
⊢ IsHeapForest' r []
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
id : ℕ
⊢ IsHeapForest' r []
Tactic:
constructor
Proof state after:
no goals
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
id : ℕ
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
⊢ IsHeapForest' r (List.eraseIdx (t :: ts) id)
Tactic:
unfold List.eraseIdx
Proof state after:
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
id : ℕ
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
⊢ IsHeapForest' r
    (match t :: ts, id with
    | [], x => []
    | head :: as, 0 => as
    | a :: as, Nat.succ n => a :: List.eraseIdx as n)
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
id : ℕ
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
⊢ IsHeapForest' r
    (match t :: ts, id with
    | [], x => []
    | head :: as, 0 => as
    | a :: as, Nat.succ n => a :: List.eraseIdx as n)
Tactic:
split
Proof state after:
case h_1
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝² : ℕ
x✝¹ : List (BinTree α✝)
x✝ : ℕ
heq✝ : t :: ts = []
⊢ IsHeapForest' r []

case h_2
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
head✝ : BinTree α✝
as✝ : List (BinTree α✝)
heq✝ : t :: ts = head✝ :: as✝
⊢ IsHeapForest' r as✝

case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
case h_1
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝² : ℕ
x✝¹ : List (BinTree α✝)
x✝ : ℕ
heq✝ : t :: ts = []
⊢ IsHeapForest' r []

case h_2
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
head✝ : BinTree α✝
as✝ : List (BinTree α✝)
heq✝ : t :: ts = head✝ :: as✝
⊢ IsHeapForest' r as✝

case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)
Tactic:
. constructor
Proof state after:
case h_2
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
head✝ : BinTree α✝
as✝ : List (BinTree α✝)
heq✝ : t :: ts = head✝ :: as✝
⊢ IsHeapForest' r as✝

case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
case h_2
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
head✝ : BinTree α✝
as✝ : List (BinTree α✝)
heq✝ : t :: ts = head✝ :: as✝
⊢ IsHeapForest' r as✝

case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)
Tactic:
. simp_all
  apply IsHeapForest'_weaken
  . assumption
  . apply le_of_lt 
    assumption
Proof state after:
case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
case h_3
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (a✝ :: List.eraseIdx as✝ n✝)
Tactic:
. rename_i eq
  have hf : IsHeapForest' r (t ::ts) := by
    apply IsHeapForest'_of_IsHeapForest' <;> assumption
  constructor
  . simp_all
  . simp_all
  . rw[eq] at hf
    cases hf
    apply IsHeapForest'_eraseIdx
    assumption
Proof state after:
no goals
Theorem: project.IsHeapForest'_eraseIdx
Proof state before:
α : Sort ?u.32649
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
r : ℕ
α✝ : Type u_1
a : List (BinTree α✝)
t : BinTree α✝
ts : List (BinTree α✝)
lt : r < t.rank
bt : IsBinTree t
h₁ : IsHeapForest' t.rank ts
x✝¹ : List (BinTree α✝)
x✝ : ℕ
a✝ : BinTree α✝
as✝ : List (BinTree α✝)
n✝ : ℕ
eq : t :: ts = a✝ :: as✝
⊢ IsHeapForest' r (t :: ts)
Tactic:
apply IsHeapForest'_of_IsHeapForest' <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_delete_BinTree
Proof state before:
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
⊢ IsHeap (Heap.heap (a :: b)) → IsHeap (Heap.heap (a :: List.eraseIdx b id))
Tactic:
intros h₁
Proof state after:
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
h₁ : IsHeap (Heap.heap (a :: b))
⊢ IsHeap (Heap.heap (a :: List.eraseIdx b id))
Theorem: project.IsHeap_delete_BinTree
Proof state before:
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
h₁ : IsHeap (Heap.heap (a :: b))
⊢ IsHeap (Heap.heap (a :: List.eraseIdx b id))
Tactic:
cases h₁
Proof state after:
case cons
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeap (Heap.heap (a :: List.eraseIdx b id))
Theorem: project.IsHeap_delete_BinTree
Proof state before:
case cons
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeap (Heap.heap (a :: List.eraseIdx b id))
Tactic:
constructor
Proof state after:
case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ 0 < a.rank

case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsBinTree a

case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeapForest' a.rank (List.eraseIdx b id)
Theorem: project.IsHeap_delete_BinTree
Proof state before:
case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ 0 < a.rank

case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsBinTree a

case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeapForest' a.rank (List.eraseIdx b id)
Tactic:
. assumption
Proof state after:
case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsBinTree a

case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeapForest' a.rank (List.eraseIdx b id)
Theorem: project.IsHeap_delete_BinTree
Proof state before:
case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsBinTree a

case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeapForest' a.rank (List.eraseIdx b id)
Tactic:
. assumption
Proof state after:
case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeapForest' a.rank (List.eraseIdx b id)
Theorem: project.IsHeap_delete_BinTree
Proof state before:
case cons.a
α : Sort ?u.102122
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
α✝ : Type u_1
a : HeapNodeAux α✝ (Heap α✝)
b : List (HeapNodeAux α✝ (Heap α✝))
id : ℕ
a✝² : IsBinTree a
a✝¹ : 0 < a.rank
a✝ : IsHeapForest' a.rank b
⊢ IsHeapForest' a.rank (List.eraseIdx b id)
Tactic:
. apply IsHeapForest'_eraseIdx
  assumption
Proof state after:
no goals
Theorem: project.IsMinHeap_eraseIdx
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
⊢ IsMinHeap le (Heap.heap (List.eraseIdx [] id))
Tactic:
simp
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
⊢ IsMinHeap le (Heap.heap [])
Theorem: project.IsMinHeap_eraseIdx
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
⊢ IsMinHeap le (Heap.heap [])
Tactic:
constructor
Proof state after:
no goals
Theorem: project.IsMinHeap_eraseIdx
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le (Heap.heap (List.eraseIdx (t :: ts) id))
Tactic:
unfold List.eraseIdx
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le
    (Heap.heap
      (match t :: ts, id with
      | [], x => []
      | head :: as, 0 => as
      | a :: as, Nat.succ n => a :: List.eraseIdx as n))
Theorem: project.IsMinHeap_eraseIdx
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
id : ℕ
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
⊢ IsMinHeap le
    (Heap.heap
      (match t :: ts, id with
      | [], x => []
      | head :: as, 0 => as
      | a :: as, Nat.succ n => a :: List.eraseIdx as n))
Tactic:
split
Proof state after:
case h_1
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝² : ℕ
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
heq✝ : t :: ts = []
⊢ IsMinHeap le (Heap.heap [])

case h_2
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
head✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
heq✝ : t :: ts = head✝ :: as✝
⊢ IsMinHeap le (Heap.heap as✝)

case h_3
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
le_trans : ∀ (x y z : α), le x y = true → le y z = true → le x z = true
le_rfl : ∀ (z : α), le z z = true
b : List (HeapNodeAux α (Heap α))
t : BinTree α
ts : List (HeapNodeAux α (Heap α))
st : IsSearchTree le t
mh : IsMinHeap le (Heap.heap ts)
x✝¹ : List (HeapNodeAux α (Heap α))
x✝ : ℕ
a✝ : HeapNodeAux α (Heap α)
as✝ : List (HeapNodeAux α (Heap α))
n✝ : ℕ
heq✝ : t :: ts = a✝ :: as✝
⊢ IsMinHeap le (Heap.heap (a✝ :: List.eraseIdx as✝ n✝))