## Stream: maths

### Topic: property applies to all elements of list

#### Sean Leather (Apr 30 2018 at 08:10):

Is there another, convenient way one might specify this given what exists in mathlib?

inductive allp (p : α → Prop) : list α → Prop
| nil {} : allp []
| cons : Π {a : α} {l : list α}, p a → allp l → allp (a :: l)


Or, alternatively:

def allp (p : α → Prop) : list α → Prop :=
list.foldr (λ a h, p a ∧ h) true


#### Mario Carneiro (Apr 30 2018 at 08:11):

The standard way to write allp is \forall x \in l, p x

#### Sean Leather (Apr 30 2018 at 08:18):

I see. That uses the recursive of list.mem to accomplish the recursion of allp.

Are there existing equivalent theorems to these?

theorem allp_singleton (pa : p a) : allp p [a]
theorem allp_append : allp p l₁ → allp p l₂ → allp p (l₁ ++ l₂)
theorem allp_nil : allp p [] ↔ true
theorem allp_cons : allp p (a :: l) ↔ p a ∧ allp p l


#### Sean Leather (Apr 30 2018 at 08:19):

In the core library?

lemma ball_nil (p : α → Prop) : ∀ x ∈ @nil α, p x
lemma ball_cons (p : α → Prop) (a : α) (l : list α) : (∀ x ∈ (a :: l), p x) ↔ (p a ∧ ∀ x ∈ l, p x)


#### Mario Carneiro (Apr 30 2018 at 08:22):

There are forall_mem_nil and forall_mem_cons, but the append theorem is not there. You can probably get the singleton theorem by simp

Last updated: May 09 2021 at 09:11 UTC