no goals
α : Type u
β : Type v
γ : Type w
p : α → Bool
as bs : List α
⊢ filterTR.loop p as bs = reverse bs ++ filter p as
induction as generalizing bs with
| nil => simp [filterTR.loop, filter]
| cons a as ih =>
  simp [filterTR.loop, filter]
  split
  next => rw [ih, reverse_cons, append_assoc]; simp
  next => rw [ih]
no goals
case nil
α : Type u
β : Type v
γ : Type w
p : α → Bool
bs : List α
⊢ filterTR.loop p nil bs = reverse bs ++ filter p nil
simp [filterTR.loop, filter]
case cons
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
⊢ (match p a with
    | true => filterTR.loop p as (a :: bs)
    | false => filterTR.loop p as bs) =
    reverse bs ++
      match p a with
      | true => a :: filter p as
      | false => filter p as
case cons
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
⊢ filterTR.loop p (a :: as) bs = reverse bs ++ filter p (a :: as)
simp [filterTR.loop, filter]
case cons.h_1
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = true
⊢ filterTR.loop p as (a :: bs) = reverse bs ++ a :: filter p as

case cons.h_2
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = false
⊢ filterTR.loop p as bs = reverse bs ++ filter p as
case cons
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
⊢ (match p a with
    | true => filterTR.loop p as (a :: bs)
    | false => filterTR.loop p as bs) =
    reverse bs ++
      match p a with
      | true => a :: filter p as
      | false => filter p as
split
case cons.h_2
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = false
⊢ filterTR.loop p as bs = reverse bs ++ filter p as
case cons.h_1
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = true
⊢ filterTR.loop p as (a :: bs) = reverse bs ++ a :: filter p as

case cons.h_2
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = false
⊢ filterTR.loop p as bs = reverse bs ++ filter p as
next => rw [ih, reverse_cons, append_assoc]; simp
no goals
case cons.h_2
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = false
⊢ filterTR.loop p as bs = reverse bs ++ filter p as
next => rw [ih]
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = true
⊢ reverse bs ++ (a :: nil ++ filter p as) = reverse bs ++ a :: filter p as
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = true
⊢ filterTR.loop p as (a :: bs) = reverse bs ++ a :: filter p as
rw [ih, reverse_cons, append_assoc]
no goals
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = true
⊢ reverse bs ++ (a :: nil ++ filter p as) = reverse bs ++ a :: filter p as
simp
no goals
α : Type u
β : Type v
γ : Type w
p : α → Bool
a : α
as : List α
ih : ∀ (bs : List α), filterTR.loop p as bs = reverse bs ++ filter p as
bs : List α
x✝ : Bool
heq✝ : p a = false
⊢ filterTR.loop p as bs = reverse bs ++ filter p as
rw [ih]