no goals
α : Type u_1
p : α → Bool
l : List α
⊢ partition p l = (filter p l, filter (not ∘ p) l)
simp [partition, aux]
no goals
α : Type u_1
p : α → Bool
l as✝ bs✝ : List α
⊢ partition.loop p [] (as✝, bs✝) = (reverse as✝ ++ filter p [], reverse bs✝ ++ filter (not ∘ p) [])
simp [partition.loop, filter]
no goals
α : Type u_1
p : α → Bool
l✝ as✝ bs✝ : List α
a : α
l : List α
⊢ partition.loop p (a :: l) (as✝, bs✝) = (reverse as✝ ++ filter p (a :: l), reverse bs✝ ++ filter (not ∘ p) (a :: l))
cases pa : p a <;> simp [partition.loop, pa, aux, filter, append_assoc]