Theorem: Set.merge_length (ReckonLean/Common.lean)

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
⊢ ∀ (l1 l2 : List α), List.length (merge l1 l2) = List.length l1 + List.length l2
Tactic:
intro l1 l2
State after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length (merge l1 l2) = List.length l1 + List.length l2

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length (merge l1 l2) = List.length l1 + List.length l2
Tactic:
match l1 with
| .nil => unfold merge; rw [List.length_nil, Nat.zero_add]
| .cons h1 t1 =>
  unfold merge
  match l2 with
  | .nil => simp only [List.length_cons, List.length_nil, Nat.add_zero]
  | .cons h2 t2 =>
    simp only [List.length_cons]
    split
    . rw [List.length_cons, merge_length t1 (h2 :: t2)]
      simp only [List.length_cons]
      omega
    . rw [List.length_cons, merge_length (h1 :: t1) t2]
      simp only [List.length_cons]
      omega
State after:
no goals

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length (merge [] l2) = List.length [] + List.length l2
Tactic:
unfold merge
State after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length l2 = List.length [] + List.length l2

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
⊢ List.length l2 = List.length [] + List.length l2
Tactic:
rw [List.length_nil, Nat.zero_add]
State after:
no goals

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length (merge (h1 :: t1) l2) = List.length (h1 :: t1) + List.length l2
Tactic:
unfold merge
State after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length
      (match l2 with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length l2

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length
      (match l2 with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length l2
Tactic:
match l2 with
| .nil => simp only [List.length_cons, List.length_nil, Nat.add_zero]
| .cons h2 t2 =>
  simp only [List.length_cons]
  split
  . rw [List.length_cons, merge_length t1 (h2 :: t2)]
    simp only [List.length_cons]
    omega
  . rw [List.length_cons, merge_length (h1 :: t1) t2]
    simp only [List.length_cons]
    omega
State after:
no goals

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
⊢ List.length
      (match [] with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length []
Tactic:
simp only [List.length_cons, List.length_nil, Nat.add_zero]
State after:
no goals

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
⊢ List.length
      (match h2 :: t2 with
      | [] => h1 :: t1
      | l2@h:(h2 :: t2) =>
        let_fun x := (_ : List.length t1 + List.length l2 < List.length (h1 :: t1) + List.length l2);
        let_fun x := (_ : List.length (h1 :: t1) + List.length t2 < List.length (h1 :: t1) + List.length l2);
        if isLE (compare h1 h2) = true then h1 :: merge t1 l2 else h2 :: merge (h1 :: t1) t2) =
    List.length (h1 :: t1) + List.length (h2 :: t2)
Tactic:
simp only [List.length_cons]
State after:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
⊢ List.length (if isLE (compare h1 h2) = true then h1 :: merge t1 (h2 :: t2) else h2 :: merge (h1 :: t1) t2) =
    Nat.succ (List.length t1) + Nat.succ (List.length t2)

State before:
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
⊢ List.length (if isLE (compare h1 h2) = true then h1 :: merge t1 (h2 :: t2) else h2 :: merge (h1 :: t1) t2) =
    Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
split
State after:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ List.length (h1 :: merge t1 (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

State before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ List.length (h1 :: merge t1 (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
. rw [List.length_cons, merge_length t1 (h2 :: t2)]
  simp only [List.length_cons]
  omega
State after:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

State before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
. rw [List.length_cons, merge_length (h1 :: t1) t2]
  simp only [List.length_cons]
  omega
State after:
no goals

State before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ List.length (h1 :: merge t1 (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
rw [List.length_cons, merge_length t1 (h2 :: t2)]
State after:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + List.length (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

State before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + List.length (h2 :: t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
simp only [List.length_cons]
State after:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + Nat.succ (List.length t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

State before:
case inl
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : isLE (compare h1 h2) = true
⊢ Nat.succ (List.length t1 + Nat.succ (List.length t2)) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
omega
State after:
no goals

State before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ List.length (h2 :: merge (h1 :: t1) t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
rw [List.length_cons, merge_length (h1 :: t1) t2]
State after:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (List.length (h1 :: t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

State before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (List.length (h1 :: t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
simp only [List.length_cons]
State after:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (Nat.succ (List.length t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)

State before:
case inr
α : Type
inst✝¹ : Ord α
inst✝ : BEq α
l1 l2 : List α
h1 : α
t1 : List α
h2 : α
t2 : List α
h✝ : ¬isLE (compare h1 h2) = true
⊢ Nat.succ (Nat.succ (List.length t1) + List.length t2) = Nat.succ (List.length t1) + Nat.succ (List.length t2)
Tactic:
omega
State after:
no goals