Theorem: project.IsHeap_merge
Proof state before:
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:
. split
  . constructor
    . rw[Nat.min_eq]
      split
      . cases hys
        apply Nat.lt_of_le_of_lt <;> assumption
      . cases hys
        assumption
    . cases hys
      assumption
    . have heq : min h₂.rank (h₁.rank -1) = h₂.rank := by
        have : h₂.rank ≤ (h₁.rank - 1) := by
          apply Nat.le_pred_of_lt
          assumption
        apply min_eq_left
        assumption
      rw[← heq]
      apply IsHeap_merge 
      . cases hys
        assumption
      . constructor
        . cases hxs
          apply Nat.pred_lt
          simp
          cases rx <;> apply Nat.not_eq_zero_of_lt; repeat assumption
        . cases hxs
          assumption
        . cases hxs
          assumption
  . dsimp
    split
    . split
      . rename_i hneq hneq₂ 
        simp at * 
        have heq : h₁.rank = h₂.rank := by
          apply Nat.le_antisymm <;> assumption
        constructor
        . have : (combine le h₁ h₂).rank = h₁.rank + 1 := by
            apply rank_combine heq
          rw[this]; clear this
          rw[Nat.min_eq]
          split
          . cases hxs
            apply Nat.lt_succ_of_lt 
            assumption
          . cases hys
            rw[heq]
            apply Nat.lt_succ_of_lt
            assumption
        . cases hxs
          cases hys
          apply combine_IsBinTree <;> assumption
        . rw[rank_combine heq] at *
          cases hxs with | cons _ _ ht₁ => 
          cases hys with | cons _ _ ht₂ =>
          have ih := IsHeap_merge ht₁ ht₂
          have min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂) := by 
            rw[← heq] at ht₂
            apply min_hRank_mergeNodes ht₁ ht₂
          by_cases (t₁ = [] ∧ t₂ = [])
          . have (And.intro he₁ he₂) := h
            simp[he₁, he₂]
            constructor
          . apply IsHeapForest'_strengthen
            . apply ih
            . rw[Nat.min_eq] at min_le
              split at min_le
              . match ht₁ with
                | .nil =>
                  rw[empty_heap_merge_left] at *
                  match ht₂ with
                  | .nil => simp at h
                  | .cons (t := bt) hlt _ _ =>
                    rw[hrank_of_cons] at *
                    rw[← heq] at hlt
                    unfold bne at hneq₂
                    rw[Nat.not_beq_eq_true_eq] at hneq₂
                    have n : h₁.rank + 1 ≤ bt.rank := by
                      apply Nat.succ_le_of_lt hlt 
                    apply lt_of_le_of_ne <;> assumption
                | .cons (t := t) (ts := ts) hlt _ _ =>
                  rw[hrank_of_cons] at *
                  have : h₁.rank < hRank (mergeNodes le (t :: ts) t₂) := by
                    apply lt_of_lt_of_le <;> assumption
                  unfold bne at hneq
                  rw[Nat.not_beq_eq_true_eq] at hneq
                  have : h₁.rank + 1 ≤ t.rank := by
                    apply Nat.succ_le_of_lt hlt
                  have : h₁.rank + 1 < t.rank := by
                    apply lt_of_le_of_ne <;> assumption
                  apply lt_of_lt_of_le <;> assumption
              . match ht₂ with
                | .nil => 
                  rw[empty_heap_merge_right] at *
                  match ht₁ with
                  | .nil =>
                    simp at h
                  | .cons (t := t) (ts := ts) lt _ _ => 
                    rw[hrank_of_cons] at *
                    unfold bne at hneq
                    rw[Nat.not_beq_eq_true_eq] at hneq
                    have : h₁.rank + 1 ≤ t.rank := by
                      apply Nat.succ_le_of_lt lt
                    apply lt_of_le_of_ne <;> assumption
                | .cons (t := t) (ts := ts) lt _ _ =>
                  rw[hrank_of_cons] at *
                  rw[← heq] at lt
                  have : h₁.rank + 1 ≤ t.rank := by
                    apply Nat.succ_le_of_lt lt
                  unfold bne at hneq₂
                  rw[Nat.not_beq_eq_true_eq] at hneq₂
                  have : h₁.rank + 1 < t.rank := by
                    apply lt_of_le_of_ne <;> assumption
                  apply lt_of_lt_of_le <;> assumption
      . apply IsHeap_merge
        simp at *
        have heq : h₁.rank = h₂.rank := by
          apply Nat.le_antisymm <;> assumption
        . constructor
          . cases hxs with | cons lt _ _ =>
              rw[rank_combine heq]
              have : h₁.rank < h₁.rank + 1 := by
                apply Nat.lt_succ_self
              apply lt_trans lt this
          . cases hxs 
            cases hys
            apply combine_IsBinTree <;> assumption
          . match hxs with
            | .cons _ _ hf =>
              have : (combine le h₁ h₂).rank = h₁.rank + 1 := by
                apply rank_combine heq
              simp only [this] at *; clear this
              match hf with
              | .nil =>
                constructor
              | .cons (t := t) (ts := ts) lt _ _ =>
                constructor
                . have : h₁.rank + 1 ≤ t.rank := by
                    apply Nat.succ_le_of_lt lt
                  apply lt_of_le_of_ne this
                  rw[hrank_of_cons] at *
                  unfold bne at *
                  rw[Nat.not_beq_eq_true_eq] at *
                  assumption
                . assumption
                . assumption
        . cases hys with | cons lt _ hf =>
            have : ry ≤ h₂.rank := by
                apply le_of_lt lt
            apply IsHeapForest'_weaken hf this
    . split
      . apply IsHeap_merge
        . cases hxs with | cons lt _ hf =>
            have : rx ≤ h₁.rank := by
                apply le_of_lt lt
            apply IsHeapForest'_weaken hf this
        . constructor
          . simp at *
            have heq : h₁.rank = h₂.rank := by
              apply Nat.le_antisymm <;> assumption
            rw[rank_combine heq] at *
            cases hys
            rw[heq]
            apply Nat.lt_succ_of_lt
            assumption
          . cases hxs with | cons =>
              cases hys with | cons =>
                simp at *
                have : h₁.rank = h₂.rank := by
                  apply Nat.le_antisymm <;> assumption
                apply combine_IsBinTree <;> assumption
          . simp at *
            have heq : h₁.rank = h₂.rank := by
              apply Nat.le_antisymm <;> assumption
            rw[rank_combine heq] at *
            cases hys with | cons _ _ hf =>
              match hf with 
              | .nil =>
                constructor
              | .cons (t := t) (ts := ts) lt _ _ =>
                rw[← heq] at lt
                have b : h₁.rank + 1 ≤ t.rank := by
                  apply Nat.succ_le_of_lt lt
                rw[hrank_of_cons] at *
                constructor
                . unfold bne at *
                  rw[Nat.not_beq_eq_true_eq] at *
                  apply lt_of_le_of_ne <;> assumption
                repeat assumption      
      . simp at * 
        have heq : h₁.rank = h₂.rank := by
          apply Nat.le_antisymm <;> assumption
        constructor
        . rw[Nat.min_eq]
          split
          . rw[rank_combine heq] at *
            cases hxs
            apply Nat.lt_succ_of_lt
            assumption
          . rw[rank_combine heq] at *
            cases hys
            rw[heq]
            apply Nat.lt_succ_of_lt
            assumption                
        . cases hxs
          cases hys
          apply combine_IsBinTree <;> assumption
        . rw[rank_combine heq] at *
          cases hxs with | cons _ _ hf =>
          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