internlm/Lean-Github huggingface dataset:
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ u.rank + 1 < t.rank

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. rw[← heq] at hle
  apply lt_of_le_of_ne <;> assumption
Proof state after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsBinTree t

case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. assumption
Proof state after:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
hle : c.rank + 1 ≤ t.rank
⊢ IsHeapForest' t.rank ts
Tactic:
. assumption
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
heq : u.rank = c.rank
h✝² : ¬u.rank < c.rank
h✝¹ : ¬c.rank < u.rank
h✝ : ¬(u.rank + 1 != hRank y) = true
a✝⁶ : IsBinTree u
a✝⁵ : r < u.rank
a✝⁴ : IsHeapForest' u.rank y
a✝³ : IsBinTree c
a✝² : r < c.rank
hf : IsHeapForest' c.rank z
t : BinTree α
ts : List (BinTree α)
lt : c.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
neq : ¬u.rank + 1 = t.rank
⊢ c.rank + 1 ≤ t.rank
Tactic:
apply Nat.succ_le_of_lt lt
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
⊢ IsHeapForest' r y
Tactic:
cases ht₁
Proof state after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' r y
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' r y
Tactic:
apply IsHeapForest'_weaken
Proof state after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' ?cons.n y

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ ℕ
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ IsHeapForest' ?cons.n y

case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ r ≤ ?cons.n

case cons.n
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ ℕ
Tactic:
. assumption
Proof state after:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ r ≤ u.rank
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case cons.a
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
a✝² : IsBinTree u
a✝¹ : r < u.rank
a✝ : IsHeapForest' u.rank y
⊢ r ≤ u.rank
Tactic:
. apply Nat.le_of_lt 
  assumption
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
hf₂ : IsHeapForest' r y
⊢ min (hRank y) (hRank (combine le u c :: z)) ≤ hRank (mergeNodes le y (combine le u c :: z))
Tactic:
apply min_hRank_mergeNodes hf₂ hf
Proof state after:
no goals
Theorem: project.hRank_mergeNodes_cons
Proof state before:
case inr.inr.inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
hf₂ : IsHeapForest' r y
min_le : min (hRank y) (hRank (combine le u c :: z)) ≤ hRank (mergeNodes le y (combine le u c :: z))
⊢ u.rank + 1 ≤ hRank (mergeNodes le y (combine le u c :: z))
Tactic:
rw[hrank_of_cons] at *
Proof state after:
case inr.inr.inr.inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
r : ℕ
u : BinTree α
y : List (BinTree α)
c : BinTree α
z : List (BinTree α)
ht₁ : IsHeapForest' r (u :: y)
ht₂ : IsHeapForest' r (c :: z)
heq : u.rank = c.rank
h✝³ : ¬u.rank < c.rank
h✝² : ¬c.rank < u.rank
h✝¹ : ¬((combine le u c).rank != hRank y) = true
h✝ : ((combine le u c).rank != hRank z) = true
hf : IsHeapForest' r (combine le u c :: z)
hf₂ : IsHeapForest' r y
min_le : min (hRank y) (combine le u c).rank ≤ hRank (mergeNodes le y (combine le u c :: z))
⊢ u.rank + 1 ≤ hRank (mergeNodes le y (combine le u c :: z))
Theorem: project.IsHeapForest'_of_IsHeapForest'
Proof state before:
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
⊢ IsBinTree r → y < r.rank → IsHeapForest' r.rank x → IsHeapForest' y (r :: x)
Tactic:
intros
Proof state after:
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
a✝² : IsBinTree r
a✝¹ : y < r.rank
a✝ : IsHeapForest' r.rank x
⊢ IsHeapForest' y (r :: x)
Theorem: project.IsHeapForest'_of_IsHeapForest'
Proof state before:
α : Sort ?u.70497
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
α✝ : Type u_1
r : BinTree α✝
y : ℕ
x : List (BinTree α✝)
a✝² : IsBinTree r
a✝¹ : y < r.rank
a✝ : IsHeapForest' r.rank x
⊢ IsHeapForest' y (r :: x)
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx []
hys : IsHeapForest' ry h
⊢ IsHeapForest' (min rx ry) (mergeNodes le [] h)
Tactic:
rw [empty_heap_merge_left]
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx []
hys : IsHeapForest' ry h
⊢ IsHeapForest' (min rx ry) h
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx []
hys : IsHeapForest' ry h
⊢ IsHeapForest' (min rx ry) h
Tactic:
apply IsHeapForest'_weaken hys
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx []
hys : IsHeapForest' ry h
⊢ min rx ry ≤ ry
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx []
hys : IsHeapForest' ry h
⊢ min rx ry ≤ ry
Tactic:
apply min_le_right
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx h
hys : IsHeapForest' ry []
⊢ IsHeapForest' (min rx ry) (mergeNodes le h [])
Tactic:
rw[empty_heap_merge_right]
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx h
hys : IsHeapForest' ry []
⊢ IsHeapForest' (min rx ry) h
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx h
hys : IsHeapForest' ry []
⊢ IsHeapForest' (min rx ry) h
Tactic:
apply IsHeapForest'_weaken hxs
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx h
hys : IsHeapForest' ry []
⊢ min rx ry ≤ rx
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys h : List (BinTree α)
hxs : IsHeapForest' rx h
hys : IsHeapForest' ry []
⊢ min rx ry ≤ rx
Tactic:
apply min_le_left
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
⊢ IsHeapForest' (min rx ry) (mergeNodes le (h₁ :: t₁) (h₂ :: t₂))
Tactic:
unfold mergeNodes
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
⊢ IsHeapForest' (min rx ry)
    (if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ (h₂ :: t₂)
    else
      if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
⊢ IsHeapForest' (min rx ry)
    (if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ (h₂ :: t₂)
    else
      if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
      else
        let merged := combine le h₁ h₂;
        let r := merged.rank;
        if (r != hRank t₁) = true then
          if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
        else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)
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
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry) (h₁ :: mergeNodes le t₁ (h₂ :: t₂))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry)
    (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
    else
      let merged := combine le h₁ h₂;
      let r := merged.rank;
      if (r != hRank t₁) = true then
        if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
      else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case inl
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry) (h₁ :: mergeNodes le t₁ (h₂ :: t₂))

case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry)
    (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
    else
      let merged := combine le h₁ h₂;
      let r := merged.rank;
      if (r != hRank t₁) = true then
        if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
      else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)
Tactic:
. constructor
  . cases hxs
    rw[Nat.min_eq]
    split
    . assumption
    . rename_i nle
      simp at nle
      apply Nat.lt_trans nle
      assumption
  . cases hxs
    assumption
  . cases hxs with | cons hlt bt hf =>
      rename_i hlt₂
      have : h₁.rank = min h₁.rank (h₂.rank - 1) := by
        have hle : h₁.rank ≤ (h₂.rank - 1) := by
          apply Nat.le_pred_of_lt hlt₂
        have : min h₁.rank (h₂.rank - 1) = h₁.rank := by
          apply min_eq_left hle
        rw[this]
      rw [this]; clear this
      apply IsHeap_merge
      . assumption
      . apply IsHeapForest'_strengthen_pred
        . assumption
        . cases bt with | mk =>
            have hge : h₁.rank ≥ 0 := by
              cases h₁.rank
              . simp 
              . simp
            have hle : 0 ≤ h₁.rank := by
              apply hge
            have : 0 < h₂.rank := by
              apply lt_of_le_of_lt hle hlt₂
            assumption
Proof state after:
case inr
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
h✝ : ¬h₁.rank < h₂.rank
⊢ IsHeapForest' (min rx ry)
    (if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ (h₁ :: t₁)
    else
      let merged := combine le h₁ h₂;
      let r := merged.rank;
      if (r != hRank t₁) = true then
        if (r != hRank t₂) = true then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
      else if (r != hRank t₂) = true then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂)