## Stream: Is there code for X?

### Topic: involutive f ↔ f ∘ f = id

#### 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?

#### 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.)

#### 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.

#### Johan Commelin (Sep 23 2020 at 09:25):

You would then be able to use reverse_involutive.comp_self

#### 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?

#### Johan Commelin (Sep 23 2020 at 09:26):

No, I think we want both names

#### 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?

#### 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.

#### Johan Commelin (Sep 23 2020 at 09:28):

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

#### Eric Wieser (Sep 23 2020 at 09:28):

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

#### 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.

#### 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.)

#### Eric Wieser (Sep 23 2020 at 13:29):

Presumably we still want a third lemma, involutive reverse?

#### Gabriel Ebner (Sep 23 2020 at 13:37):

Sure, seems reasonable enough.

#### 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.

#### 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?

#### Eric Wieser (Sep 23 2020 at 13:40):

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

#### Johan Commelin (Sep 23 2020 at 13:44):

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

#### Johan Commelin (Sep 23 2020 at 13:44):

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

#### 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.

#### 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

#### 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

#### 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

#### Gabriel Ebner (Sep 23 2020 at 15:00):

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

#### Eric Wieser (Sep 23 2020 at 15:40):

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

#### Gabriel Ebner (Sep 23 2020 at 15:50):

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

#### Eric Wieser (Sep 23 2020 at 15:53):

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

#### Eric Wieser (Sep 23 2020 at 15:54):

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

#### 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.

#### 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?

#### Gabriel Ebner (Sep 24 2020 at 14:10):

#4237

Last updated: May 17 2021 at 16:26 UTC