Zulip Chat Archive
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: Dec 20 2023 at 11:08 UTC