internlm/Lean-Github huggingface dataset:
Theorem: project.IsSearchTree_findMin
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
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsMinHeap le (Heap.heap (h :: hs))
hh' : IsSearchTree le h'
⊢ IsSearchTree le (findMin le (h :: hs) idx (h', idx')).fst
Tactic:
simp[findMin]
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
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsMinHeap le (Heap.heap (h :: hs))
hh' : IsSearchTree le h'
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Theorem: project.IsSearchTree_findMin
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
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hhs : IsMinHeap le (Heap.heap (h :: hs))
hh' : IsSearchTree le h'
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Tactic:
cases hhs
Proof state after:
case cons
α : 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
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hh' : IsSearchTree le h'
a✝¹ : IsSearchTree le h
a✝ : IsMinHeap le (Heap.heap hs)
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Theorem: project.IsSearchTree_findMin
Proof state before:
case cons
α : 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
h : HeapNodeAux α (Heap α)
hs : List (HeapNodeAux α (Heap α))
idx : ℕ
h' : BinTree α
idx' : ℕ
hh' : IsSearchTree le h'
a✝¹ : IsSearchTree le h
a✝ : IsMinHeap le (Heap.heap hs)
⊢ IsSearchTree le
    (if le h'.val h.val = true then findMin le hs (idx + 1) (h', idx') else findMin le hs (idx + 1) (h, idx)).fst
Tactic:
split <;> apply IsSearchTree_findMin <;> assumption
Proof state after:
no goals
Theorem: project.findMin_is_minimum_head
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
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (findMin le [] idx (h', idx')).fst.val h'.val = true
Tactic:
simp[findMin]
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
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le h'.val h'.val = true
Theorem: project.findMin_is_minimum_head
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
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le h'.val h'.val = true
Tactic:
apply le_rfl
Proof state after:
no goals
Theorem: project.findMin_is_minimum_head
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
Tactic:
unfold findMin
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (if le h'.val t.val = true then findMin le ts (idx + 1) (h', idx') else findMin le ts (idx + 1) (t, idx)).fst.val
      h'.val =
    true
Theorem: project.findMin_is_minimum_head
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (if le h'.val t.val = true then findMin le ts (idx + 1) (h', idx') else findMin le ts (idx + 1) (t, idx)).fst.val
      h'.val =
    true
Tactic:
split
Proof state after:
case inl
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
h✝ : le h'.val t.val = true
⊢ le (findMin le ts (idx + 1) (h', idx')).fst.val h'.val = true

case inr
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
h✝ : ¬le h'.val t.val = true
⊢ le (findMin le ts (idx + 1) (t, idx)).fst.val h'.val = true
Theorem: project.findMin_is_minimum_head
Proof state before:
case inl
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
h✝ : le h'.val t.val = true
⊢ le (findMin le ts (idx + 1) (h', idx')).fst.val h'.val = true

case inr
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
h✝ : ¬le h'.val t.val = true
⊢ le (findMin le ts (idx + 1) (t, idx)).fst.val h'.val = true
Tactic:
. apply findMin_is_minimum_head
Proof state after:
case inr
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
h✝ : ¬le h'.val t.val = true
⊢ le (findMin le ts (idx + 1) (t, idx)).fst.val h'.val = true
Theorem: project.findMin_is_minimum_head
Proof state before:
case inr
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
h✝ : ¬le h'.val t.val = true
⊢ le (findMin le ts (idx + 1) (t, idx)).fst.val h'.val = true
Tactic:
. have ih := findMin_is_minimum_head ts (idx + 1) t idx
  apply le_trans
  assumption
  apply not_le_le
  assumption
Proof state after:
no goals
Theorem: project.findMin_is_minimum_tail
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
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (findMin le [] idx (h', idx')).fst.val h'.val = true →
    ∀ (x : BinTree α), x ∈ [] → le (findMin le [] idx (h', idx')).fst.val x.val = true
Tactic:
intros _ _ hin
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
idx : ℕ
h' : BinTree α
idx' : ℕ
a✝ : le (findMin le [] idx (h', idx')).fst.val h'.val = true
x✝ : BinTree α
hin : x✝ ∈ []
⊢ le (findMin le [] idx (h', idx')).fst.val x✝.val = true
Theorem: project.findMin_is_minimum_tail
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
idx : ℕ
h' : BinTree α
idx' : ℕ
a✝ : le (findMin le [] idx (h', idx')).fst.val h'.val = true
x✝ : BinTree α
hin : x✝ ∈ []
⊢ le (findMin le [] idx (h', idx')).fst.val x✝.val = true
Tactic:
cases hin
Proof state after:
no goals
Theorem: project.findMin_is_minimum_tail
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true →
    ∀ (x : BinTree α), x ∈ t :: ts → le (findMin le (t :: ts) idx (h', idx')).fst.val x.val = true
Tactic:
intros hle t₂ hel
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
hel : t₂ ∈ t :: ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Theorem: project.findMin_is_minimum_tail
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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
hel : t₂ ∈ t :: ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Tactic:
cases hel
Proof state after:
case head
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t.val = true

case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Theorem: project.findMin_is_minimum_tail
Proof state before:
case head
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t.val = true

case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Tactic:
. unfold findMin
  split
  . unfold findMin at hle
    split at hle
    . apply le_trans <;> assumption
    . contradiction
  . apply findMin_is_minimum_head <;> assumption
Proof state after:
case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Theorem: project.findMin_is_minimum_tail
Proof state before:
case tail
α : 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
t : BinTree α
ts : List (BinTree α)
idx : ℕ
h' : BinTree α
idx' : ℕ
hle : le (findMin le (t :: ts) idx (h', idx')).fst.val h'.val = true
t₂ : BinTree α
a✝ : List.Mem t₂ ts
⊢ le (findMin le (t :: ts) idx (h', idx')).fst.val t₂.val = true
Tactic:
. unfold findMin
  split
  . unfold findMin at hle
    split at hle
    . apply findMin_is_minimum_tail <;> assumption
    . contradiction
  . apply findMin_is_minimum_tail
    . unfold findMin at hle
      split at hle
      . contradiction
      . apply findMin_is_minimum_head <;> assumption
    . assumption
Proof state after:
no goals
Theorem: project.findMin_is_minimum
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
⊢ ∀ (hs : List (BinTree α)) (idx : ℕ) (h' : BinTree α) (idx' : ℕ),
    le (findMin le hs idx (h', idx')).fst.val h'.val = true ∧
      ∀ (x : BinTree α), x ∈ hs → le (findMin le hs idx (h', idx')).fst.val x.val = true
Tactic:
intros
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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val h'✝.val = true ∧
    ∀ (x : BinTree α), x ∈ hs✝ → le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val x.val = true
Theorem: project.findMin_is_minimum
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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val h'✝.val = true ∧
    ∀ (x : BinTree α), x ∈ hs✝ → le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val x.val = true
Tactic:
apply And.intro
Proof state after:
case left
α : 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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val h'✝.val = true

case right
α : 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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ ∀ (x : BinTree α), x ∈ hs✝ → le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val x.val = true
Theorem: project.findMin_is_minimum
Proof state before:
case left
α : 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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val h'✝.val = true

case right
α : 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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ ∀ (x : BinTree α), x ∈ hs✝ → le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val x.val = true
Tactic:
. apply findMin_is_minimum_head <;> assumption
Proof state after:
case right
α : 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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ ∀ (x : BinTree α), x ∈ hs✝ → le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val x.val = true
Theorem: project.findMin_is_minimum
Proof state before:
case right
α : 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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ ∀ (x : BinTree α), x ∈ hs✝ → le (findMin le hs✝ idx✝ (h'✝, idx'✝)).fst.val x.val = true
Tactic:
. apply findMin_is_minimum_tail <;> try assumption
  apply findMin_is_minimum_head <;> assumption
Proof state after:
no goals
Theorem: project.findMin_is_minimum
Proof state before:
case right.le_rfl
α : 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
hs✝ : List (BinTree α)
idx✝ : ℕ
h'✝ : BinTree α
idx'✝ : ℕ
⊢ ∀ (z : α), le z z = true
Tactic:
assumption
Proof state after:
no goals
Theorem: project.deleteMin_empty_heap
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
xs : Heap α
⊢ deleteMin le xs = none → isEmpty xs = true
Tactic:
intro heq
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
xs : Heap α
heq : deleteMin le xs = none
⊢ isEmpty xs = true
Theorem: project.deleteMin_empty_heap
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
xs : Heap α
heq : deleteMin le xs = none
⊢ isEmpty xs = true
Tactic:
unfold deleteMin at heq
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
xs : Heap α
heq :
  (match xs with
    | Heap.heap [] => none
    | Heap.heap [h] => some (h.val, h.children)
    | Heap.heap hhs@h_1:(h :: hs) =>
      match findMin le hs 1 (h, 0) with
      | (min, minIdx) =>
        let rest := List.eraseIdx hhs minIdx;
        let tail := merge le (Heap.heap rest) min.children;
        some (min.val, tail)) =
    none
⊢ isEmpty xs = true
Theorem: project.deleteMin_empty_heap
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
xs : Heap α
heq :
  (match xs with
    | Heap.heap [] => none
    | Heap.heap [h] => some (h.val, h.children)
    | Heap.heap hhs@h_1:(h :: hs) =>
      match findMin le hs 1 (h, 0) with
      | (min, minIdx) =>
        let rest := List.eraseIdx hhs minIdx;
        let tail := merge le (Heap.heap rest) min.children;
        some (min.val, tail)) =
    none
⊢ isEmpty xs = true
Tactic:
cases xs with | heap ts =>
cases ts with 
| nil =>
  rfl
| cons _ ts =>
  dsimp at heq
  cases ts <;> contradiction
Proof state after:
no goals
Theorem: project.deleteMin_empty_heap
Proof state before:
case heap
α : 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
ts : List (HeapNodeAux α (Heap α))
heq :
  (match Heap.heap ts with
    | Heap.heap [] => none
    | Heap.heap [h] => some (h.val, h.children)
    | Heap.heap hhs@h_1:(h :: hs) =>
      match findMin le hs 1 (h, 0) with
      | (min, minIdx) =>
        let rest := List.eraseIdx hhs minIdx;
        let tail := merge le (Heap.heap rest) min.children;
        some (min.val, tail)) =
    none
⊢ isEmpty (Heap.heap ts) = true
Tactic:
cases ts with 
| nil =>
  rfl
| cons _ ts =>
  dsimp at heq
  cases ts <;> contradiction
Proof state after:
no goals
Theorem: project.deleteMin_empty_heap
Proof state before:
case heap.nil
α : 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
heq :
  (match Heap.heap [] with
    | Heap.heap [] => none
    | Heap.heap [h] => some (h.val, h.children)
    | Heap.heap hhs@h_1:(h :: hs) =>
      match findMin le hs 1 (h, 0) with
      | (min, minIdx) =>
        let rest := List.eraseIdx hhs minIdx;
        let tail := merge le (Heap.heap rest) min.children;
        some (min.val, tail)) =
    none
⊢ isEmpty (Heap.heap []) = true
Tactic:
rfl
Proof state after:
no goals
Theorem: project.deleteMin_empty_heap
Proof state before:
case heap.cons
α : 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
head✝ : HeapNodeAux α (Heap α)
ts : List (HeapNodeAux α (Heap α))
heq :
  (match Heap.heap (head✝ :: ts) with
    | Heap.heap [] => none
    | Heap.heap [h] => some (h.val, h.children)
    | Heap.heap hhs@h_1:(h :: hs) =>
      match findMin le hs 1 (h, 0) with
      | (min, minIdx) =>
        let rest := List.eraseIdx hhs minIdx;
        let tail := merge le (Heap.heap rest) min.children;
        some (min.val, tail)) =
    none
⊢ isEmpty (Heap.heap (head✝ :: ts)) = true
Tactic:
dsimp at heq
Proof state after:
case heap.cons
α : 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
head✝ : HeapNodeAux α (Heap α)
ts : List (HeapNodeAux α (Heap α))
heq :
  (match Heap.heap (head✝ :: ts) with
    | Heap.heap [] => none
    | Heap.heap [h] => some (h.val, h.children)
    | Heap.heap hhs@h_1:(h :: hs) =>
      some
        ((findMin le hs 1 (h, 0)).fst.val,
          merge le (Heap.heap (List.eraseIdx hhs (findMin le hs 1 (h, 0)).snd))
            (findMin le hs 1 (h, 0)).fst.children)) =
    none
⊢ isEmpty (Heap.heap (head✝ :: ts)) = true
Theorem: project.deleteMin_empty_heap
Proof state before:
case heap.cons
α : 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
head✝ : HeapNodeAux α (Heap α)
ts : List (HeapNodeAux α (Heap α))
heq :
  (match Heap.heap (head✝ :: ts) with
    | Heap.heap [] => none
    | Heap.heap [h] => some (h.val, h.children)
    | Heap.heap hhs@h_1:(h :: hs) =>
      some
        ((findMin le hs 1 (h, 0)).fst.val,
          merge le (Heap.heap (List.eraseIdx hhs (findMin le hs 1 (h, 0)).snd))
            (findMin le hs 1 (h, 0)).fst.children)) =
    none
⊢ isEmpty (Heap.heap (head✝ :: ts)) = true
Tactic:
cases ts <;> contradiction
Proof state after:
no goals
Theorem: project.IsHeapForest'_of_IsRankedTree
Proof state before:
α : Sort ?u.894
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 s : ℕ
α✝ : Type u_1
nodes : List (BinTree α✝)
h₁ : r ≠ 0
⊢ IsHeapForest' (r - 1) []
Tactic:
constructor
Proof state after:
no goals