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₂
h✝² h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) []
h : ¬([] = [] ∧ [] = [])
h✝ hle : hRank [] ≤ hRank []
⊢ h₁.rank + 1 < hRank []
Tactic:
contradiction
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₂
h✝² : (h₁.rank + 1 != hRank []) = false
t : BinTree α
ts : List (BinTree α)
a✝² : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (h₁.rank + 1 != hRank (t :: ts)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : hRank (t :: ts) ≤ hRank []
hle : hRank (t :: ts) ≤ hRank (t :: ts)
⊢ h₁.rank + 1 < hRank (t :: ts)
Tactic:
rw[hrank_of_cons] 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₂
h✝² : (h₁.rank + 1 != hRank []) = false
t : BinTree α
ts : List (BinTree α)
a✝² : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (h₁.rank + 1 != t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : t.rank ≤ hRank []
hle : t.rank ≤ t.rank
⊢ h₁.rank + 1 < 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₂
h✝² : (h₁.rank + 1 != hRank []) = false
t : BinTree α
ts : List (BinTree α)
a✝² : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (h₁.rank + 1 != t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : t.rank ≤ hRank []
hle : t.rank ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
unfold bne 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₂
h✝² : (!h₁.rank + 1 == hRank []) = false
t : BinTree α
ts : List (BinTree α)
a✝² : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (!h₁.rank + 1 == t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : t.rank ≤ hRank []
hle : t.rank ≤ t.rank
⊢ h₁.rank + 1 < 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₂
h✝² : (!h₁.rank + 1 == hRank []) = false
t : BinTree α
ts : List (BinTree α)
a✝² : h₁.rank < t.rank
a✝¹ : IsBinTree t
a✝ : IsHeapForest' t.rank ts
h✝¹ : (!h₁.rank + 1 == t.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : t.rank ≤ hRank []
hle : t.rank ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
rw[Bool.not_eq_false', beq_iff_eq] 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₂
h✝² : h₁.rank + 1 = hRank []
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) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : t.rank ≤ hRank []
hle : t.rank ≤ t.rank
⊢ h₁.rank + 1 < 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₂
h✝² : h₁.rank + 1 = hRank []
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) (t :: ts)
h : ¬(t :: ts = [] ∧ [] = [])
h✝ : t.rank ≤ hRank []
hle : t.rank ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
simp 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₂
h✝² : h₁.rank + 1 = hRank []
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) (t :: ts)
h✝ : t.rank ≤ hRank []
h hle : True
⊢ h₁.rank + 1 < 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₂
h✝² : h₁.rank + 1 = hRank []
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) (t :: ts)
h✝ : t.rank ≤ hRank []
h hle : True
⊢ h₁.rank + 1 < t.rank
Tactic:
contradiction
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
h✝² : (h₁.rank + 1 != hRank t₁) = false
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 != hRank (t :: ts)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ (t :: ts))
h : ¬(t₁ = [] ∧ t :: ts = [])
h✝ : hRank t₁ ≤ hRank (t :: ts)
hle : hRank t₁ ≤ hRank (mergeNodes le t₁ (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le t₁ (t :: ts))
Tactic:
match hf with
| .nil => 
  rw[empty_heap_merge_left] at *
  rw[hrank_of_cons] at *
  unfold bne at *
  rw[Bool.not_eq_false', beq_iff_eq] at *
  simp at *
  contradiction
| .cons (t := t₂) (ts := ts₂) _ _ _ =>
  repeat rw[hrank_of_cons] at *
  unfold bne at *
  rw[Bool.not_eq_false', beq_iff_eq] at *
  simp at *
  have ht₁ : IsHeapForest' h₁.rank (t₂ :: ts₂) := by
    apply IsHeapForest'_of_IsHeapForest' <;> assumption
  have ht₂ : IsHeapForest' h₁.rank (t :: ts) := by
    rw[← heq] at *
    apply IsHeapForest'_of_IsHeapForest' <;> assumption
  have : t₂.rank + 1 ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts)) := by
    apply hRank_mergeNodes_cons ht₁ ht₂
    simp_all
  rename_i heq₂ _
  rw[heq₂]
  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 != hRank (t :: ts)) = false
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le [] (t :: ts))
h : ¬([] = [] ∧ t :: ts = [])
h✝ : hRank [] ≤ hRank (t :: ts)
hle : hRank [] ≤ hRank (mergeNodes le [] (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le [] (t :: ts))
Tactic:
rw[empty_heap_merge_left] 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 != hRank (t :: ts)) = false
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ hRank (t :: ts)
⊢ h₁.rank + 1 < hRank (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 != hRank (t :: ts)) = false
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ hRank (t :: ts)
⊢ h₁.rank + 1 < hRank (t :: ts)
Tactic:
rw[hrank_of_cons] 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) = false
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < 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) = false
h✝¹ : (h₁.rank + 1 != hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
unfold bne 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) = false
h✝¹ : (!h₁.rank + 1 == hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < 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) = false
h✝¹ : (!h₁.rank + 1 == hRank []) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
rw[Bool.not_eq_false', beq_iff_eq] 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✝¹ : h₁.rank + 1 = hRank []
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < 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✝¹ : h₁.rank + 1 = hRank []
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h : ¬([] = [] ∧ t :: ts = [])
h✝ hle : hRank [] ≤ t.rank
⊢ h₁.rank + 1 < t.rank
Tactic:
simp 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✝¹ : h₁.rank + 1 = hRank []
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h✝ hle : hRank [] ≤ t.rank
h : True
⊢ h₁.rank + 1 < 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✝¹ : h₁.rank + 1 = hRank []
ih : IsHeapForest' (min h₁.rank h₂.rank) (t :: ts)
h✝ hle : hRank [] ≤ t.rank
h : True
⊢ h₁.rank + 1 < t.rank
Tactic:
contradiction
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 != hRank (t :: ts)) = false
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : (h₁.rank + 1 != hRank (t₂ :: ts₂)) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : ¬(t₂ :: ts₂ = [] ∧ t :: ts = [])
h✝ : hRank (t₂ :: ts₂) ≤ hRank (t :: ts)
hle : hRank (t₂ :: ts₂) ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
repeat rw[hrank_of_cons] 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) = false
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : (h₁.rank + 1 != t₂.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : ¬(t₂ :: ts₂ = [] ∧ t :: ts = [])
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ 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) = false
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : (h₁.rank + 1 != t₂.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : ¬(t₂ :: ts₂ = [] ∧ t :: ts = [])
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
Tactic:
unfold bne 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) = false
t₂ : BinTree α
ts₂ : List (BinTree α)
a✝² : h₁.rank < t₂.rank
a✝¹ : IsBinTree t₂
a✝ : IsHeapForest' t₂.rank ts₂
h✝¹ : (!h₁.rank + 1 == t₂.rank) = false
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le (t₂ :: ts₂) (t :: ts))
h : ¬(t₂ :: ts₂ = [] ∧ t :: ts = [])
h✝ : t₂.rank ≤ t.rank
hle : t₂.rank ≤ hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))
⊢ h₁.rank + 1 < hRank (mergeNodes le (t₂ :: ts₂) (t :: ts))