Zulip Chat Archive

Stream: Is there code for X?

Topic: involutive f ↔ f ∘ f = id


view this post on Zulip Eric Wieser (Sep 23 2020 at 09:19):

I have a goal of the form map (reverse ∘ reverse) l = l for some nested list l, and would like it to simplify. Unfortunately, docs#list.reverse_reverse doesn't apply here, as there is no direct application.

I can write

lemma involutive_comp_self {f : α  α} (h : function.involutive f) : f  f = id :=
by {funext, simp [h x]}

and then use involutive_comp_self reverse_reverse but this isn't suitable as a simp lemma due to the h. Can I make h be inferred by simp too?

Should involutive_comp_self be in mathlib?

view this post on Zulip Kyle Miller (Sep 23 2020 at 09:23):

(I have no comment about mathlib, but you can simplify the proof to the term funext h.)

view this post on Zulip Johan Commelin (Sep 23 2020 at 09:25):

@Eric Wieser I would call the lemma involutive.comp_self (with a .).
Does reverse_involutive exist? If not, it should.

view this post on Zulip Johan Commelin (Sep 23 2020 at 09:25):

You would then be able to use reverse_involutive.comp_self

view this post on Zulip Eric Wieser (Sep 23 2020 at 09:26):

Does it make sense to change the definition of reverse_reverse to be involutive reverse instead of reverse reverse l = l?

view this post on Zulip Johan Commelin (Sep 23 2020 at 09:26):

No, I think we want both names

view this post on Zulip Eric Wieser (Sep 23 2020 at 09:27):

Can we make involutive.comp_self be simp somehow, where the proof of involutiveness is found automatically?

view this post on Zulip Johan Commelin (Sep 23 2020 at 09:28):

Yes, you can make it simp, but you will need to feed reverse_involutive into the simp set, for it to work.

view this post on Zulip Johan Commelin (Sep 23 2020 at 09:28):

I'm not sure if reverse_involutive should be @[simp] by default.

view this post on Zulip Eric Wieser (Sep 23 2020 at 09:28):

If we did that, presumably reverse_reverse could be removed from the simp set?

view this post on Zulip Eric Wieser (Sep 23 2020 at 10:38):

Added as part of #4222

view this post on Zulip Reid Barton (Sep 23 2020 at 12:50):

Eric Wieser said:

If we did that, presumably reverse_reverse could be removed from the simp set?

I'm skeptical--I don't think there is any way simp could then look at reverse (reverse l) and think, "gee, I wish I knew reverse was involutive, so I could apply the definition of involutive"--the reason being that a lemma (h : involutive f) : f (f x) = x isn't a valid form for a simp lemma.
Similarly, I think changing the statement of reverse_reverse to be involutive reverse will prevent it from being used conveniently with both simp and rw.

view this post on Zulip Gabriel Ebner (Sep 23 2020 at 13:24):

I think the canonical solution is to have two lemmas here:

@[simp] lemma reverse_reverse {x : list α} : x.reverse.reverse = x := ...
@[simp] lemma reverse_comp_reverse : (reverse  reverse) = @id (list α) := by ext; simp

Similar to docs#deriv_pow and docs#deriv_pow', etc. ( is a bit of a pain in simp lemmas sometimes, but it should be fine here. We should really make it semireducible one day.)

view this post on Zulip Eric Wieser (Sep 23 2020 at 13:29):

Presumably we still want a third lemma, involutive reverse?

view this post on Zulip Gabriel Ebner (Sep 23 2020 at 13:37):

Sure, seems reasonable enough.

view this post on Zulip Gabriel Ebner (Sep 23 2020 at 13:38):

Johan Commelin said:

I'm not sure if reverse_involutive should be @[simp] by default.

IMHO it should definitely be simp, there's no real downside.

view this post on Zulip Eric Wieser (Sep 23 2020 at 13:39):

So now every single involutive def needs two obvious lemmas on top of the original lemma (+ the standard func_inj one). Is there any way to avoid all this repetition?

view this post on Zulip Eric Wieser (Sep 23 2020 at 13:40):

Making involutive a class might solve that problem. Would that be sane?

view this post on Zulip Johan Commelin (Sep 23 2020 at 13:44):

Well, we tried that with semi-bundled homs, but simp didn't fire in many cases.

view this post on Zulip Johan Commelin (Sep 23 2020 at 13:44):

Hence we started the bundled hom story. But I don't think we want bundled involutions.

view this post on Zulip Gabriel Ebner (Sep 23 2020 at 13:59):

Eric Wieser said:

So now every single involutive def needs two obvious lemmas on top of the original lemma (+ the standard func_inj one). Is there any way to avoid all this repetition?

If you make both involutive.comp_self and involutive_reverse simp, then you don't need reverse_comp_reverse. But yeah, it's still two lemmas.

view this post on Zulip Eric Wieser (Sep 23 2020 at 14:02):

You're right, I overcounter. For reverse, in my PR #4222 and master we have

  • reverse_reverse
  • reverse_involutive := reverse_reverse (new in my PR)
  • reverse_injective := reverse_involutive.injective
  • reverse_inj : = reverse_injective.eq_iff

Perhaps we can remove some of these

view this post on Zulip Reid Barton (Sep 23 2020 at 14:05):

In your original goal, I think you should also just be able to add function.comp to the list of simp lemmas, and that should enable reverse_reverse to fire

view this post on Zulip Eric Wieser (Sep 23 2020 at 14:17):

Reid Barton said:

In your original goal, I think you should also just be able to add function.comp to the list of simp lemmas, and that should enable reverse_reverse to fire

That doesn't work, the goal reduces to l = map (λ (x : list α), x) l, which doesn't match the map_id simp lemma

view this post on Zulip Gabriel Ebner (Sep 23 2020 at 15:00):

So we need map_id' : xs.map (λ x, x) = xs!

view this post on Zulip Eric Wieser (Sep 23 2020 at 15:40):

And the same for every other lemma that currently involves id?

view this post on Zulip Gabriel Ebner (Sep 23 2020 at 15:50):

We already do, see docs#deriv_id, docs#deriv_id', docs#deriv_id'', etc.

view this post on Zulip Eric Wieser (Sep 23 2020 at 15:53):

Is a simp lemma from id to (λ x, x) sensible to eliminate the duplication?

view this post on Zulip Eric Wieser (Sep 23 2020 at 15:54):

(Also, does your suggestion go against or complement the new lemma in my PR?)

view this post on Zulip Johan Commelin (Sep 23 2020 at 16:59):

Gabriel Ebner said:

We already do, see docs#deriv_id, docs#deriv_id', docs#deriv_id'', etc.

I feel like this is a bit of a symptom. It would be good if we could find a way to avoid these repetitive statements.

view this post on Zulip Eric Wieser (Sep 24 2020 at 13:21):

Gabriel Ebner said:

If you make ...involutive_reverse simp, then ...

It seems that while marking involutive reverse with simp is fine, marking injective reverse fails with:

/- The `simp_var_head` linter reports: -/
/- LEFT-HAND SIDE HAS VARIABLE AS HEAD SYMBOL.
Some simp lemmas have a variable as head symbol of the left-hand side: -/
-- data/list/basic.lean
#print list.reverse_injective /- Left-hand side has variable as head symbol: a₁ -/

I don't understand this error @Gabriel Ebner, but I assume I should just ignore your request in https://github.com/leanprover-community/mathlib/pull/4222#discussion_r494285415 to make injective reverse simp?

view this post on Zulip Gabriel Ebner (Sep 24 2020 at 14:10):

#4237


Last updated: May 17 2021 at 16:26 UTC