internlm/Lean-Github huggingface dataset:
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have ht₂ : IsHeapForest' h₁.rank (t :: ts) := by
  rw[← heq] at *
  apply IsHeapForest'_of_IsHeapForest' <;> assumption
Proof state after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
have : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts)) := by
  apply hRank_mergeNodes_cons ht₁ ht₂
  simp_all
Proof state after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rename_i heq₂ _
Proof state after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
rw[heq₂]
Proof state after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ t₂.rank < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝³ : h₂.rank ≤ h₁.rank
h✝² : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝¹ : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
heq₂ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
this : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ t₂.rank < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
apply Nat.lt_of_succ_le this
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
⊢ IsHeapForest' h₁.rank (t₂ :: ts₂)
Tactic:
apply IsHeapForest'_of_IsHeapForest' <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)
Tactic:
rw[← heq] at *
Proof state after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₁.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₁.rank
hf₂ : IsHeapForest' h₁.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₁.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₁.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₁.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₁.rank
hf₂ : IsHeapForest' h₁.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₁.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₁.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
⊢ IsHeapForest' h₁.rank (t :: ts)
Tactic:
apply IsHeapForest'_of_IsHeapForest' <;> assumption
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
apply hRank_mergeNodes_cons ht₁ ht₂
Proof state after:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank = t.rank
Theorem: project.IsHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂✝ : List (BinTree α)
not_le_le : ∀ (x y : α), le x y = false → le y x = true
h✝⁴ : h₂.rank ≤ h₁.rank
h✝³ : h₁.rank ≤ h₂.rank
heq : h₁.rank = h₂.rank
a✝⁹ : IsBinTree h₁
a✝⁸ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
a✝⁷ : IsBinTree h₂
a✝⁶ : ry < h₂.rank
hf₂ : IsHeapForest' h₂.rank t₂✝
t : BinTree α
ts : List (BinTree α)
a✝⁵ : h₂.rank < t.rank
a✝⁴ : IsBinTree t
a✝³ : IsHeapForest' t.rank ts
h✝² : h₁.rank + 1 = t.rank
h : True
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : h₁.rank + 1 = t₂.rank
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
hle : t.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
h✝ : t.rank < t₂.rank
ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂)
ht₂ : IsHeapForest' h₁.rank (t :: ts)
⊢ t₂.rank = t.rank
Tactic:
simp_all
Proof state after:
no goals
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
⊢ IsMinHeap le (Heap.heap []) → IsMinHeap le (Heap.heap h) → IsMinHeap le (Heap.heap (mergeNodes le [] h))
Tactic:
intros _ hys
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
hys : IsMinHeap le (Heap.heap h)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] h))
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
hys : IsMinHeap le (Heap.heap h)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] h))
Tactic:
cases hys
Proof state after:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))
Theorem: project.IsMinHeap_merge
Proof state before:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))
Tactic:
. simp[mergeNodes]
  constructor
Proof state after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))
Theorem: project.IsMinHeap_merge
Proof state before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] (t✝ :: ts✝)))
Tactic:
. constructor <;> assumption
Proof state after:
no goals
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
⊢ IsMinHeap le (Heap.heap h) → IsMinHeap le (Heap.heap []) → IsMinHeap le (Heap.heap (mergeNodes le h []))
Tactic:
intros hxs _
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap h)
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le h []))
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy h : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap h)
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le h []))
Tactic:
cases hxs
Proof state after:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))
Theorem: project.IsMinHeap_merge
Proof state before:
case nil
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝ : IsMinHeap le (Heap.heap [])
⊢ IsMinHeap le (Heap.heap (mergeNodes le [] []))

case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))
Tactic:
. simp[mergeNodes]
  constructor
Proof state after:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))
Theorem: project.IsMinHeap_merge
Proof state before:
case cons
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
a✝² : IsMinHeap le (Heap.heap [])
t✝ : BinTree α
ts✝ : List (HeapNodeAux α (Heap α))
a✝¹ : IsSearchTree le t✝
a✝ : IsMinHeap le (Heap.heap ts✝)
⊢ IsMinHeap le (Heap.heap (mergeNodes le (t✝ :: ts✝) []))
Tactic:
. constructor <;> assumption
Proof state after:
no goals
Theorem: project.IsMinHeap_merge
Proof state before:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
⊢ IsMinHeap le (Heap.heap (h₁ :: t₁)) →
    IsMinHeap le (Heap.heap (h₂ :: t₂)) → IsMinHeap le (Heap.heap (mergeNodes le (h₁ :: t₁) (h₂ :: t₂)))
Tactic:
intros hxs hys
Proof state after:
α : Type u_1
le : α → α → Bool
not_le_le : ∀ (x y : α), ¬le x y = true → le y x = true
hx hy : List (HeapNodeAux α (Heap α))
h₁ : HeapNodeAux α (Heap α)
t₁ : List (HeapNodeAux α (Heap α))
h₂ : HeapNodeAux α (Heap α)
t₂ : List (HeapNodeAux α (Heap α))
hxs : IsMinHeap le (Heap.heap (h₁ :: t₁))
hys : IsMinHeap le (Heap.heap (h₂ :: t₂))
⊢ IsMinHeap le (Heap.heap (mergeNodes le (h₁ :: t₁) (h₂ :: t₂)))