InvImage instances

Stream: mathlib4

[Hannah Fechtner]

Hi, I'm working on PR#20310 which defines the shortlex relation on lists. I'm following the given advice to prove more general theorems first, and then apply them.

The shortlex order is defined as the InvImage of something; where ought I put these instances/theorems?

theorem InvImage.trichotomous {β : Type*} [IsTrichotomous α r] {f : β → α}
    (h : Function.Injective f) : ∀ a b, (InvImage r f) a b ∨ a = b ∨ (InvImage r f) b a := by
  intro a b
  rw [← Function.Injective.eq_iff h]
  exact IsTrichotomous.trichotomous (f a) (f b)

instance InvImage.isAsymm {β : Type*} [IsAsymm α r] (f : β → α) : IsAsymm β (InvImage r f) where
  asymm := fun a b h h2 => IsAsymm.asymm (f a) (f b) h h2

The most similar place looks to be https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Defs/Unbundled.html#InvImage.trans but those lemmas (InvImage.trans and InvImage.irreflexive) are listed as deprecated

[Eric Wieser]

Can the first one be stated with IsTrichotomous?

[Hannah Fechtner]

It could be, but typeclass inference won't find the hypothesis that f is injective, so it's easier to use as a theorem. Then I can use it with apply, and Lean will leave me with a goal to prove f's infectivity

[Eric Wieser]

Usually I think we'd handle this by writing it through the typeclass but not making it an instance; but probably @Yaël Dillies and @Violeta Hernández have opinions here, and I think it's not a big deal either way.

[Eric Wieser]

You _could_ make it an instance for embeddings

[Violeta Hernández]

We really ought to have one single canonical way of stating that a relation is trichotomous/asymmetric/reflexive/whatever. For better or worse (I'd argue for better) the way most of Mathlib currently writes this down is via the Is* typeclasses, so my recommendation is to just use those even if your theorem is not an instance.

[Yaël Dillies]

I also have to say that InvImage is a weird name for a perfectly common operation on relations, and I am not sure how I feel about stating theorems using it

[Violeta Hernández]

There's some very useful instances on InvImage, such as "the inverse image of a well-founded relation is well-founded".

[Yaël Dillies]

Precisely. That's not very useful because no one finds themselves using InvImage. Instead in applications you rather have a subrelation s of InvImage r f for some r and f (where r and f are not necessarily obvious!). A lemma would be much better suited here. Back when I was doing arguments of this form, no such lemma existed so I had to resort to some obscure combination of three unfindable lemmas to do the job

[Violeta Hernández]

Maybe the solution is to just use InvImage more? This seems very analogous to the preimage, which is also a very simple definition we all agree to use notation for anyways because of how many nice properties it satisfies.

[Yaël Dillies]

I don't see the situations as analogous. f ⁻¹ s is genuinely a useful object people prove things about. InvImage r f not so much. As I said, we rather prove things about a relation s for which there exist some r and f such that s ≤ InvImage r f

[Eric Wieser]

Is InvImage r f the same as r on f? (edit: docs#InvImage suggests it is)

[Violeta Hernández]

Ok so now we know for sure one of them must go

[Eric Wieser]

I think in practice on is only every used for Prop

[Eric Wieser]

You could check that by restricting the universe of onFun and seeing if anything breaks

[Eric Wieser]

Personally I prefer the on naming, but the notation has been controversial in the past

[Eric Wieser]

If nothing uses it for Sort I propose we drop that support

[Eric Wieser]

Nat.choose on Nat.factorial isn't exactly obvious notation

[Yaël Dillies]

Eric Wieser said:

Is InvImage r f the same as r on f? (edit: docs#InvImage suggests it is)

Yes, that's part of my quibble with it

[Edward van de Meent]

Eric Wieser said:

I think in practice on is only every used for Prop

I'm pretty sure it gets used in API around docs#Set.PairwiseDisjoint ?

[Edward van de Meent]

Ah, I was wrong. I was thinking of its definition: s.PairwiseDisjoint f := s.Pairwise (Disjoint on f) which indeed uses it for prop

[Violeta Hernández]

Wait, is docs#InvImage also equal to docs#Order.Preimage ?

[Violeta Hernández]

audible sigh

import Mathlib

open Function

variable {α β : Type*} (r : β → β → Prop) (f : α → β)

example : (r on f) = InvImage r f := rfl
example : (r on f) = f ⁻¹'o r := rfl

[Violeta Hernández]

So what now?

[Violeta Hernández]

I think Order.Preimage is the one of the three which makes the most sense from a didactic point of view. But unfortunately InvImage is the one that's in Core.

[Violeta Hernández]

I'm testing whether onFun is only used on Prop here: #21982

[Violeta Hernández]

Yep, save for a single rfl theorem onFun is only ever used on relations.

[Violeta Hernández]

So to me it's clear two of these need to go.

[Eric Wieser]

InvImage works on Sort, Order.Preimage does not

[Eric Wieser]

So for the full comparison:

import Mathlib
universe u v

recall InvImage       -- no notation
  {α : Sort u}   {β : Sort v}                            (r : β → β → Prop) (f : α → β) : α → α → Prop
recall Order.Preimage -- notation `f ⁻¹'o r`
  {α : Type u_2} {β : Type u_3}              (f : α → β) (r : β → β → Prop)             : α → α → Prop
recall Function.onFun -- notation `r on f`
  {α : Sort u₁}  {β : Sort u₂} {φ : Sort u₃}             (r : β → β → φ)    (f : α → β) : α → α → φ

[Violeta Hernández]

I like the f ⁻¹o r notation the most: it makes very clear that this is essentially a preimage construction, whereas neither InvImage nor on are very obvious.

[Violeta Hernández]

That said, if the objective is to be left with a single one of these three definitions, InvImage probably gives us the least amount of hassle, being defined in Core Lean.

[Violeta Hernández]

Could we perhaps make ⁻¹o notation for InvImage?

[Ruben Van de Velde]

That sounds at least theoretically possible, not having looked at the code

[Hannah Fechtner]

Okay, so if I follow correctly, I'll keep using InvImage for my PR#20310 and I'll use the IsTrichotomous notation for the theorem