involutive f ↔ f ∘ f = id

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Johan Commelin]

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

[Johan Commelin]

You would then be able to use reverse_involutive.comp_self

[Eric Wieser]

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

[Johan Commelin]

No, I think we want both names

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

Added as part of #4222

[Reid Barton]

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]

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]

Presumably we still want a third lemma, involutive reverse?

[Gabriel Ebner]

Sure, seems reasonable enough.

[Gabriel Ebner]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Gabriel Ebner]

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]

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]

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]

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]

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

[Eric Wieser]

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

[Gabriel Ebner]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

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]

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]

#4237