property applies to all elements of list

Stream: maths

[Sean Leather]

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]

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

[Sean Leather]

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]

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]

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