Better defeqs for `Equiv.Perm.subtypeCongr`

Stream: mathlib4

[Wrenna Robson]

I would like to change Equiv.Perm.subtypeCongr so that it has better defeqs - in particular I would like to avoid going via sumCongr. I keep running into the fact that it means that both this and Equiv.perm.extendDomain just are more annoying to use and give things based on them worse simps lemmas than one would otherwise want.

(I think there's a bit of other work we could do in this related area - i.e. we could consider a non-MulHom version of Equiv.Perm.ofSubtype and the like - but that would be outside the scope of what I am proposing here.)

I wanted to test the water first and ask people what they thought. Does this irritate anyone else or is it just me?

[Eric Wieser]

What defeq do you care about and why?

[Wrenna Robson]

I would quite like it to be a dite-via-defeq. i.e. I would like Equiv.Perm.subtypeCongr.apply (why isn't this subtypeCongr_apply, btw?) to be rfl.

[Wrenna Robson]

As I say the main issue for me here is that using simps (or I suppose in particular simps!) on stuff based on it gives fairly useless lemmas - which means when you construct things using this they are just, well, a pain to use and you end up manually building API.

[Eric Wieser]

Does simps +simpRhs help?

[Wrenna Robson]

No

[Wrenna Robson]

Equiv.Perm.extendDomain_apply:
      ∀ {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
        (a : β'), (e.extendDomain f) a = (sumCompl p) (Sum.map (⇑(f.permCongr e)) id ((sumCompl p).symm a))

[Wrenna Robson]

For an example of the kind of stuff generated (here by simps! +simpRHS - without the ! gives a warning)

[Eric Wieser]

Wait, what are you putting simps on here?

[Wrenna Robson]

Perm.extendDomain

[Wrenna Robson]

first example I thought of

[Wrenna Robson]

I think for me it's just not good that it exposes all this sum-related stuff, which really it doesn't particularly have anything to do with sum types except that it's a convenient construction to conjugate through them for this. But it's very straightforward to do things the more obvious way and it means you don't constantly get these horrible sum expressions

[Wrenna Robson]

It also then impacts Perm.ofSubtype because that's built on top of extendDomain (some of the order in which we define these things doesn't entirely make sense to me but that is again a different issues).

[Wrenna Robson]

This came about because I was effectively replicating this in a special case (permutations on Nat, predicate < n for fixed n) and I realised that was silly, I should try and use the existing functions - but they are frustrating and cumbersome to use and they expose ugly internals to my eye.

[Wrenna Robson]

but I think me just trying to bodge together a fix would be very bad - so I am not going to do a PR until, well, I've chatted about it a bit

[Wrenna Robson]

I've been doing this long enough now to know that keeping my "just do a PR" ego in check and talking about it is 95% of the time the better option.

[Eric Wieser]

I think in this case the answer is "just write the simp lemmas you want by hand", simps isn't expected to be perfect everywhere

[Wrenna Robson]

Fair. I think partially I'm also a little unsure what the best simps lemmas are for this kind of thing.

[Wrenna Robson]

I find the naming using for subtypeCongr/extendDomain and related somewhat ideosyncratic.

[Wrenna Robson]

Do you think it is better to use library functions like this when you can, or is it acceptable for a particular application to make a different, perhaps cleaner definition and just provide a lemma showing it can be implemented in some other way?