Is there List.Forall₂, but for one list? (In library Std)

Stream: Is there code for X?

[Lessness]

I'm searching in https://leanprover-community.github.io/mathlib4_docs/Std/Data and can't find such definition.

For now I have found only List.Forall₂ (for two lists and binary relation) and List.all (for one list and function that returns Bool), and List.All₂...

[Lessness]

Of course, I can do forall x, List.Mem x L -> P x. I just want to find out if I'm bad at search or there's no such definition actually.

[Ruben Van de Velde]

There's docs#List.all in core

[Lessness]

Yes, that's the second definition I found and mentioned. It's almost what I wanted but not exactly (Bool instead of Prop).

[Eric Wieser]

I think the ∀ version is idiomatic here, though it's possible the one you want also exists

[Lessness]

Ok, thank you both

[Eric Wieser]

docs#List.All₂

[Eric Wieser]

What a confusing pair of names

[Eric Wieser]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Defs.html#List.All%E2%82%82

[Lessness]

Oh, right, somehow I found List.All₂ but got some brain fog and didn't understand that it is what I was searching for.

Thank you.

[Joachim Breitner]

That's indeed a very unhelpful name, I expect most associate the subscript 2 with ”Two lists”. Worth renaming to All or Forall?

[Eric Wieser]

Yes, I think the previous name was dealing with a name clash that was only a problem with the lean3 naming

[Joachim Breitner]

I also wonder how useful it is to avoid the final And True, I expect this makes some proofs harder, because it needs more case analyses in the inductive case. Maybe I'll see what breaks if one uses the normal recursive definition.

[Eric Wieser]

It's pretty handy to have nice defeqs for things like this

[Eric Wieser]

If we didn't have the defeq we could just use ∀

[Joachim Breitner]

Yes! But I'd expect the simpler function that doesn't special case the singleton list to have even nicer defeqs (in particular All p (x :: xs) = p x /\ All p xs). But I'll first have to try to see what Chesterson has to say about that.

[Joachim Breitner]

I just notice that List.Forall₂ isn't recursive with nice defeq either, but rather an inductive predicate. I understand that that’s useful for proofs by induction, but I wouldn’t you get the best of all if List.Forall₂ is defined recursively (using /\, for nice defeqs), and an inductive principle is then proved for it?
Is it possible to register such a recursor for List.Forall₂ after the fact, so that induction h still works as before?
(But probably not; that would be the “custom recusor” feature we talked about here a few days ago.)

[Eric Wieser]

Custom recursors via induction are already a feature

[Joachim Breitner]

But they won’t be picked up by match, will they?

[Joachim Breitner]

Too bad, then it’s not a refactoring that’s “for free” (unless nobody uses pattern matching on Forall_2).
@David Thrane Christiansen , is there already a tracking issue for “custom pattern matching” where we could collect usecases?

[Eric Wieser]

In my view the use-case of All₂ is to use change to go from p ∧ q ∧ r to All₂ [p, q, r], and then use a lemma to get to ∀ pi ∈ [p, q, r], pi

[Eric Wieser]

In the same spirit as docs#FinVec.Forall

[Joachim Breitner]

Somehow this special-casing of the singleton list feels wrong to me, but if you are dealing mostly dealing with concrete finite lists, rather than arbitrary lists with induction, I see the benefit of avoiding the ∧ True that corresponds to :: [].
I have https://github.com/leanprover-community/mathlib4/pull/7797 so far. I could back out the change to the definition and only keep the renaming.

[David Thrane Christiansen]

Joachim Breitner said:

Too bad, then it’s not a refactoring that’s “for free” (unless nobody uses pattern matching on Forall_2).
David Thrane Christiansen , is there already a tracking issue for “custom pattern matching” where we could collect usecases?

We don't yet have one - do you want to make it or should I?

[Joachim Breitner]

Started one at https://github.com/leanprover/lean4/issues/2716, feel free to expand, I sense you might have some concrete surface syntax suggestions.