Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inr.inr.a.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hys : IsHeapForest' ry (h₂ :: t₂)
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
h✝ : (h₁.rank + 1 != hRank t₂) = false
heq : h₁.rank = h₂.rank
a✝¹ : IsBinTree h₁
a✝ : rx < h₁.rank
hf : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
cases hys with | cons _ _ hf₂ =>
have ih := IsHeap_merge hf hf₂ 
have hle : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂) := by 
  rw[← heq] at hf₂
  apply min_hRank_mergeNodes hf hf₂
by_cases (t₁ = [] ∧ t₂ = [])
. have he₁ := h.left
  have he₂ := h.right
  simp[he₁, he₂]
  constructor
. apply IsHeapForest'_strengthen
  . apply ih
  . rw[Nat.min_eq] at hle
    split at hle
    . match hf₂ with
      | .nil =>
        rw[empty_heap_merge_right] at *
        match hf with
        | .nil =>
          contradiction
        | .cons (t := t) (ts := ts) _ _ _ =>
          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) _ _ _ => 
        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
    . match hf₂ with
      | .nil =>
        rw[empty_heap_merge_right] at *
        cases hf
        . contradiction
        . 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) _ _ _ =>
        rw[hrank_of_cons] at *
        unfold bne at *
        rw[Bool.not_eq_false', beq_iff_eq] at *
        simp at *
        match hf with
        | .nil =>
          contradiction
        | .cons (t := t₂) (ts := ts₂) _ _ _ =>
          rw[hrank_of_cons] 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