Zulip Chat Archive

Stream: maths

Topic: property applies to all elements of list


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 30 2018 at 08:11):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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