Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jan 04 2021 at 23:18):

You can simplify 1 to refl.

view this post on Zulip Eric Wieser (Jan 04 2021 at 23:30):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 04 2021 at 23:35):

And then there's only ever one spelling for each

view this post on Zulip Eric Wieser (Jan 04 2021 at 23:36):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Jan 04 2021 at 23:53):

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

view this post on Zulip Eric Wieser (Jan 04 2021 at 23:55):

monoid_hom?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Gabriel Ebner (Jan 05 2021 at 09:01):

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

view this post on Zulip 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`

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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: May 13 2021 at 06:15 UTC