Zulip Chat Archive

Stream: general

Topic: Simp and `equiv.refl α` vs `(1 : perm α)`


Eric Wieser (Jan 04 2021 at 18:44):

Is there any way to tell simp that it is allowed to reduce (1 : perm α) to equiv.refl α when looking for lemmas (and vice versa)? Or do we have to copy every simp lemma about refl for 1 too?

Yury G. Kudryashov (Jan 04 2021 at 23:18):

You can simplify 1 to refl.

Eric Wieser (Jan 04 2021 at 23:30):

I'm aware of docs#equiv.perm.one_def

Eric Wieser (Jan 04 2021 at 23:30):

But it's not a simp lemma, and if I made it one then it would prevent lemmas like mul_one firing

Eric Wieser (Jan 04 2021 at 23:32):

Conversely, if I made its reverse a simp lemma, then docs#equiv.trans_refl would not fire on (e : equiv A B).trans (refl B)

Yury G. Kudryashov (Jan 04 2021 at 23:33):

As far as I know, you have two choices:

  • duplicate lemmas;
  • simplify * to trans and 1 to refl.

Eric Wieser (Jan 04 2021 at 23:35):

I suppose there's a third choice, which is make equiv and perm no longer defeq, so that a cast has to be inserted

Eric Wieser (Jan 04 2021 at 23:35):

And then there's only ever one spelling for each

Eric Wieser (Jan 04 2021 at 23:36):

I think I'll probably just go with the duplication for now...

Yakov Pechersky (Jan 04 2021 at 23:46):

Simplifying to trans and refl loses the ability to use lemmas about monoids, unfortunately. Is it better to simplify in the context of the monoid, and then simplify, or first simplify all to equivs?

Reid Barton (Jan 04 2021 at 23:53):

Are there any useful lemmas about monoids that don't also exist for equiv?

Eric Wieser (Jan 04 2021 at 23:55):

monoid_hom?

Eric Wieser (Jan 04 2021 at 23:57):

Showing f (a.trans b) = (f a).trans (f b) would feel like an uphill battle if simp rewrote * into trans

Eric Wieser (Jan 05 2021 at 00:00):

(also to be clear, docs#equiv.perm.perm_group is not just a monoid but a group)

Gabriel Ebner (Jan 05 2021 at 09:01):

There's also a fourth choice, simplifying trans to *.

Eric Wieser (Jan 05 2021 at 09:04):

That's not always possible, for instance in the (e : equiv A B).trans 1 case I mention above`

Eric Wieser (Jan 05 2021 at 09:16):

I was hoping there was some way to make equiv.perm.perm_group.one reducible, but perhaps that doesn't make sense

Gabriel Ebner (Jan 05 2021 at 09:26):

I'm surprised that trans_refl doesn't fire on e.trans 1. 1 should reducibly reduce to equiv.refl, AFAICT.

Eric Wieser (Jan 05 2021 at 09:31):

Based on the fact the linter does not complain about the lemmas in #5614, I'm pretty sure it doesn't

Gabriel Ebner (Jan 05 2021 at 09:58):

That's maybe a bit misleading: you're allowed to specialize simp lemmas, and the linter won't complain.


Last updated: Dec 20 2023 at 11:08 UTC