sum.elim (f ∘ sum.inl) (f ∘ sum.inr) = f

Stream: Is there code for X?

[Eric Wieser]

Proof is:

@[simp] lemma what {α β γ : Sort*} (f : α ⊕ β → γ) : sum.elim (f ∘ sum.inl) (f ∘ sum.inr) = f :=
funext $ λ x, sum.cases_on x (λ _, by rw sum.elim_inl) (λ _, by rw sum.elim_inr)

This looks like an obvious candidate for a simp lemma, but I don't know what to call it

[Reid Barton]

it seems vanishingly unlikely that this left hand side would ever appear again

[Eric Wieser]

Is that an argument against inclusion into mathlib, or just an argument against being a simp lemma?

[Reid Barton]

and the proof ext (_|_); refl is easier than knowing that this lemma exists

[Eric Wieser]

I had no idea ext took rcases-style patterns

[Reid Barton]

I think that might be a somewhat recent feature

[Reid Barton]

tidy can prove it too

[Eric Wieser]

Ah, but you can't use that proof if your goal state is actually sum.elim (f ∘ sum.inl) (f ∘ sum.inr) x = f x

[Eric Wieser]

And in general ext only works on top level goals, you can't use it to simplify subexpressions

[Reid Barton]

then cases x; refl instead

[Reid Barton]

Eric Wieser said:

And in general ext only works on top level goals, you can't use it to simplify subexpressions

If this is a problem it might mean that you haven't fully decomposed your task into its parts.

[Reid Barton]

But in any case, I don't think it is a good simp lemma because that is effectively just action at a distance

[Eric Wieser]

What do you mean by it being action at a distance?

[Reid Barton]

If you rely on it to make simp work then there's an implicit long-range dependency

[Eric Wieser]

That's true of all simp lemmas though!

[Reid Barton]

imagine the import structure changes somehow to make the lemma not imported, then someone in the future will have no idea why the proof broke

[Eric Wieser]

That's moot if the lemma is in the same file as the definitions it simplifies

[Reid Barton]

right but most simp lemmas are obvious things that don't contain things like sum.elim or function composition or repeated occurrences of a variable on the left hand side

[Eric Wieser]

Which it is in #5112, which I just opened

[Reid Barton]

If it's in the same file then there's even less reason to make it a simp lemma

[Reid Barton]

oh, you mean the thing it simplifies in the sense of appearing in the lemma

[Eric Wieser]

Regarding "left hand sides don't contain composition", https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Fully.20applied.20lemmas/near/217828890 is relevant

[Reid Barton]

It's still the case that the lemma is likely to get used exactly once in which case marking it simp is just a way to hide a dependency which is better made explicit

[Eric Wieser]

Isn't hiding "obvious" dependencies fine though?

[Eric Wieser]

IMO these lemmas fall in the same category as prod.mk.eta, as proving something that you would expect to go away by itself

[Floris van Doorn]

This rule is sometimes called the co-eta rule for sums. It seems like a very basic rule that is nice to have in mathlib.
I think it's fine to make it a simp-lemma. I think that often when it applies the LHS is not exactly of this form (for example if the function composition is unfolded), which might make it tricky to use.

[Gabriel Ebner]

I'm not sure this would be a good simp-lemma. Remember that function.comp is still reducible, so this quickly becomes a higher-order matching problem.

[Floris van Doorn]

Does that argument apply to other simp lemmas involving function.comp?

[Gabriel Ebner]

I'm a bit uneasy about function.comp in simp lemmas, yes. I don't think this lemma is actively harmful, but lemmas like list.comp_map shouldn't be marked simp.

[Eric Wieser]

I added a couple more lemmas to the PR (#5112)on top of what is discussed here, would appreciate comments on which ones are good and which ones aren't

[Eric Wieser]

Is sum.elim f g ∘ inr = g any worse a simp lemma than f ∘ id = f (docs#function.comp.right_id) or [involutive f] f ∘ f = id (docs#function.involutive.comp_self)?

[Kevin Buzzard]

A Lean 3 simp expert (who probably wrote the simp linter) has expressed their unease about function.comp in simp lemmas.

[Eric Wieser]

Would this problem go away if simp unfolded comp?

[Kevin Buzzard]

comp is really weird. I used to use it a lot, and now I avoid it like the plague.

[Kevin Buzzard]

You would imagine that if it could be easily fixed, it would have been fixed a while ago.

[Kevin Buzzard]

How about making function.comp [reducible]?

[Yakov Pechersky]

Isn't it already?

[Kevin Buzzard]

Oh yes it is! I looked in the docs and it didn't mention it, but it's in the source.

[Yakov Pechersky]

It's also inlined. What about comp do you avoid? f * id = f seems like that should be "simpable" without applying, since id is the unit in that "multiplication", no?

[Kevin Buzzard]

today I learnt : docs show stuff tagged as @[simp] but not @[reducible]

[Kevin Buzzard]

What does @[inline] mean?

[Kevin Buzzard]

If function.comp is reducible, does Gabriel also get uneasy about lambdas in simp lemmas? simp can see through reducible stuff, right?

[Yakov Pechersky]

In compsci, inline usually means, "when you encounter this function, don't place it in the function call stack, which involves jumping in memory... just unwrap it and place the body of it in the current context, to avoid the jumps"

[Yakov Pechersky]

So here, it might mean, just generate the underlying VM code if you can?

[Eric Wieser]

Reducible or not, simp does not reduce docs#function.comp:

constant f : ℕ → ℕ
constant g : ℕ → ℕ

@[simp]
axiom fg : (λ x, f (g x)) = id

example : (f ∘ g) = id := by {unfold function.comp, simp} -- ok
example : (f ∘ g) = id := by simp  -- fail

[Kevin Buzzard]

def f : ℕ → ℕ := λ x, x + 3
def g : ℕ → ℕ := λ x, 2 * x

@[simp] lemma fg : (λ x, f (g x)) = id := sorry

example : (f ∘ g) = id := by simp [function.comp] -- works

(constants and axioms and sorrying data scares me). OK so maybe the issue is that we don't see function.comp in the wild so much?

[Kevin Buzzard]

hmm, thousands of occurrences in mathlib...

[Eric Wieser]

It would be good to see an example of an obviously harmful comp simp lemma.

[Kevin Buzzard]

I don't have a feeling what a harmful simp lemma could look like, but perhaps one could argue that a simp lemma which never fires is harmful because it's making simp run more slowly for no good reason

[Gabriel Ebner]

Eric Wieser said:

It would be good to see an example of an obviously harmful comp simp lemma.

We've had quite a few such problems with type class instances (such as is_monoid_hom instances for composition), that's why I'm careful. Translated to a simp lemma, this would be a problematic example:

import data.list.basic
import tactic.simp_command

open list

@[simp]
lemma comp_map' {α β γ} (h : β → γ) (g : α → β) (l : list α) :
  map (h ∘ g) l = map h (map g l) :=
(map_map _ _ _).symm

#simp only [comp_map'] [1,2,3].map (+1) -- works 🤷
#simp only [comp_map'] [1,2,3].map id   -- loops

At first glance the comp_map' lemma looks fine because it reduces the number of ∘ in the first argument of map.
But the reason it loops is that h ∘ g can match any function because ∘ is reducible and then Lean uses higher-order matching to match the resulting lambdas. (BTW, I would've expected it to match (+1) as well, but apparently it doesn't.)

[Eric Wieser]

Thanks for the example - I assume the issue is that lean matches id against id ∘ id. Is there any way to tell it to only match against non-trivial patterns?

[Eric Wieser]

Eg, have the pattern P a not match against a as id a

[Yakov Pechersky]

But if there was a lemma that simplified f ∘ id = f, comp_map' wouldn't even need to fire. The discussion on https://github.com/leanprover-community/mathlib/pull/5030 suggests that anyway, map_map should be the simp direction, and not comp_map.

[Reid Barton]

I'm suspicious about this map_map direction

[Reid Barton]

You wouldn't want a simp lemma that says x = option.map id x

[Reid Barton]

for example docs#mul_hom.map_mul goes in the direction I expect: f of a product turns into product of fs

[Reid Barton]

Maybe it's one of those cases where the grass looks greener on both sides

[Gabriel Ebner]

@Yakov Pechersky

#simp only [comp_map'] [1,2,3].map (nat.add 1)   -- loops as well

IMHO, the only solution is to make ∘ semireducible.