List of elements all satisfying predicate

Stream: new members

[Eric Wieser]

How do I declare a type where each element satisfies a predicate? list.all seems to almost be what I want, but it works in terms of bool instead of Prop.

[Jalex Stark]

i don't understand your question

[Jalex Stark]

does Pred mean Prop?

[Jalex Stark]

are you asking how to coerce a bool to a Prop?

[Alistair Tucker]

Subtype?

[Jalex Stark]

def x : Prop := ↑ff
#print x
#check x

[Eric Wieser]

No, I'm asking how to convert an a -> Prop to an a -> bool

[Reid Barton]

See the statement of all_iff_forall_prop for example.

[Jalex Stark]

why do you want to work with bool?

[Reid Barton]

Jalex, see the original question.

[Jalex Stark]

(oh, probably by original question you mean this thread, where maybe eric is computing with stuff)

[Jalex Stark]

my objection is that the main reason to work with bool is computing things, but coming from Prop loses computational interpretation?

[Eric Wieser]

I don't want to work with bool, but the closest thing I found to what I want is list.all, which does

[Eric Wieser]

It's looking like the answer is I should subtype the _elements_ of the list

[Eric Wieser]

Which I somehow missed

[Eric Wieser]

So as the simplest version of my question, how would I state the proposition all elements of a list of Nat are > 2

[Jalex Stark]

example (l : list ℕ) : Prop := list.all l (λ x, 2 < x)

[Jalex Stark]

you were in fact asking how to coerce a bool into a Prop

[Jalex Stark]

typeclass inference knows about a coercion from bool to Prop, so if you just ask Lean to interpret a bool as a Prop, it will apply that coercion

[Alistair Tucker]

Wouldn't you want to construct a term of type ∀ n : ℕ, n ∈ l → 2 < n?

[Reid Barton]

Eric Wieser said:

How do I declare a type where each element satisfies a predicate? list.all seems to almost be what I want, but it works in terms of bool instead of Prop.

(Jalex, I'm talking about this one!)

[Jalex Stark]

Reid Barton said:

Eric Wieser said:

How do I declare a type where each element satisfies a predicate? list.all seems to almost be what I want, but it works in terms of bool instead of Prop.

(Jalex, I'm talking about this one!)

okay, I think I understand now. Eric said they wanted to be able to turn their a \to Prop into a \to bool, but actually they're just as happy going the other way, and the other way is the right way

[Kenny Lau]

def they_all_satisfy_predicate (α : Sort*) (P : α → Prop) (L : list α) : Prop :=
∀ x ∈ L, P x

[Kenny Lau]

@Eric Wieser is this what you want?

[Alistair Tucker]

Ignoring the excursion into bool land, you are looking at one of two options. You could construct a list from a subtype with a proof attached to each element i.e. list {n : ℕ // 2 < n}. Or make a list l and then prove this fact about it ∀ n : ℕ, n ∈ l → 2 < n. Which is better might depend on your particular use case, but I think I see more of the latter style in mathlib.

[Mario Carneiro]

I recommend Kenny's idiom

[Mario Carneiro]

there are simp lemmas for it and decidability

[Johan Commelin]

Shouldn't list.all be renamed to list.ball?

[Mario Carneiro]

perhaps, but it's not really competing with anything

[Johan Commelin]

Well, it would free up the name for a Prop-valued version

[Mario Carneiro]

I don't want a prop valued version to exist

[Mario Carneiro]

because that would mean two idioms

[Mario Carneiro]

∀ x ∈ L, P x already exists

[Eric Wieser]

It turns out we do have the definition I was looking for, it's docs#list_all which satisfies list_all p l ↔ ∀ x ∈ l, p x. Should we rename that to list.all or list.forall? It's a bit silly having list.all be about bool and list_all being about Prop.

[Eric Wieser]

Mario Carneiro said:

I don't want a prop valued version to exist

This is a strange claim to make given you are responsible for it existing!