list equivalence relation

Stream: Is there code for X?

[Martin Dvořák]

I want to take an equivalence relation and apply it to a pair of lists. If the lists have different lengths, it should return false. If the lists have the same lengths, it should apply the binary relation pointwisely and return the conjunction of all outputs.

I want to have a lemma (instance) saying that the resulting relation on lists is again an equivalence relation. Is it in mathlib?

[Eric Wieser]

Is this docs#list.forall₂? (Edit: https://leanprover-community.github.io/mathlib_docs/data/list/defs.html#list.forall%E2%82%82)

[Eric Wieser]

Yeah, it's that

[Kyle Miller]

Here's where API for that goes: https://leanprover-community.github.io/mathlib_docs/data/list/forall2.html

[Kyle Miller]

Nothing about equivalence relations yet

[Eric Wieser]

We have the fact it's transitive and reflexive already

[Violeta Hernández]

Would a list.sublist_forall₂.is_equiv instance cause loops?

[Violeta Hernández]

Not too sure how typeclass inference works for these predicates made out of simpler ones

[Eric Wieser]

It ought to be fine

[Violeta Hernández]

Wait, is this really symmetric? Surely sublist_forall₂ r [] (a :: l) but not the other way around?

[Eric Wieser]

We weren't talking about sublist_forall₂, were we?

[Violeta Hernández]

oops