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 α)
hxs : IsHeapForest' rx (h₁ :: t₁)
hys : IsHeapForest' ry (h₂ :: t₂)
hneq : ((combine le h₁ h₂).rank != hRank t₁) = true
hneq₂ : ((combine le h₁ h₂).rank != hRank t₂) = true
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
⊢ (combine le h₁ h₂).rank = h₁.rank + 1
Tactic:
apply rank_combine heq
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inl.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₂)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
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
Proof state after:
no goals
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inl.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
have ih := IsHeap_merge ht₁ ht₂
Proof state after:
case inr.inr.inl.inl.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inl.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
have min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂) := by 
  rw[← heq] at ht₂
  apply min_hRank_mergeNodes ht₁ ht₂
Proof state after:
case inr.inr.inl.inl.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case inr.inr.inl.inl.a.cons.cons
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
by_cases (t₁ = [] ∧ t₂ = [])
Proof state after:
case pos
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : t₁ = [] ∧ t₂ = []
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)

case neg
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case pos
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : t₁ = [] ∧ t₂ = []
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)

case neg
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
. have (And.intro he₁ he₂) := h
  simp[he₁, he₂]
  constructor
Proof state after:
case neg
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Theorem: project.IsHeap_merge
Proof state before:
case neg
α : Type u_1
le : α → α → Bool
rx : ℕ
xs : List (BinTree α)
ry : ℕ
ys : List (BinTree α)
h₁ : BinTree α
t₁ : List (BinTree α)
h₂ : BinTree α
t₂ : List (BinTree α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
min_le : min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
h : ¬(t₁ = [] ∧ t₂ = [])
⊢ IsHeapForest' (h₁.rank + 1) (mergeNodes le t₁ t₂)
Tactic:
. 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
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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
Tactic:
rw[← heq] at 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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₁.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
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 α)
hneq : (h₁.rank + 1 != hRank t₁) = true
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₁.rank t₂
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le t₁ t₂)
⊢ min (hRank t₁) (hRank t₂) ≤ hRank (mergeNodes le t₁ t₂)
Tactic:
apply min_hRank_mergeNodes ht₁ ht₂
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 α)
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (mergeNodes le [] t₂)
h : ¬([] = [] ∧ t₂ = [])
h✝ : hRank [] ≤ hRank t₂
min_le : hRank [] ≤ hRank (mergeNodes le [] t₂)
⊢ h₁.rank + 1 < hRank (mergeNodes le [] t₂)
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 α)
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) t₂
h : ¬([] = [] ∧ t₂ = [])
h✝ min_le : hRank [] ≤ hRank t₂
⊢ h₁.rank + 1 < hRank t₂
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 α)
hneq₂ : (h₁.rank + 1 != hRank t₂) = true
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) t₂
h : ¬([] = [] ∧ t₂ = [])
h✝ min_le : hRank [] ≤ hRank t₂
⊢ h₁.rank + 1 < hRank t₂
Tactic:
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
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝¹ : IsBinTree h₂
a✝ : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq hneq₂ : (h₁.rank + 1 != hRank []) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) []
h : ¬([] = [] ∧ [] = [])
h✝ min_le : hRank [] ≤ hRank []
⊢ h₁.rank + 1 < hRank []
Tactic:
simp at h
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₂.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : (h₁.rank + 1 != hRank (bt :: ts✝)) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ hRank (bt :: ts✝)
⊢ h₁.rank + 1 < hRank (bt :: 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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₂.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : (h₁.rank + 1 != bt.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ bt.rank
⊢ h₁.rank + 1 < bt.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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₂.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : (h₁.rank + 1 != bt.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ bt.rank
⊢ h₁.rank + 1 < bt.rank
Tactic:
rw[← heq] at hlt
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₁.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : (h₁.rank + 1 != bt.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ bt.rank
⊢ h₁.rank + 1 < bt.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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₁.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : (h₁.rank + 1 != bt.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ bt.rank
⊢ h₁.rank + 1 < bt.rank
Tactic:
unfold bne at hneq₂
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
ht₁ : IsHeapForest' h₁.rank t₁
a✝³ : IsBinTree h₂
a✝² : ry < h₂.rank
ht₂ : IsHeapForest' h₂.rank t₂
hneq : (h₁.rank + 1 != hRank []) = true
bt : BinTree α
ts✝ : List (BinTree α)
hlt : h₁.rank < bt.rank
a✝¹ : IsBinTree bt
a✝ : IsHeapForest' bt.rank ts✝
hneq₂ : (!h₁.rank + 1 == bt.rank) = true
ih : IsHeapForest' (min h₁.rank h₂.rank) (bt :: ts✝)
h : ¬([] = [] ∧ bt :: ts✝ = [])
h✝ min_le : hRank [] ≤ bt.rank
⊢ h₁.rank + 1 < bt.rank