## Stream: Is there code for X?

### Topic: sum.elim (f ∘ sum.inl) (f ∘ sum.inr) = f

#### Eric Wieser (Nov 25 2020 at 14:35):

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 (Nov 25 2020 at 14:36):

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

#### Eric Wieser (Nov 25 2020 at 14:37):

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

#### Reid Barton (Nov 25 2020 at 14:37):

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

#### Eric Wieser (Nov 25 2020 at 14:38):

I had no idea ext took rcases-style patterns

#### Reid Barton (Nov 25 2020 at 14:38):

I think that might be a somewhat recent feature

#### Reid Barton (Nov 25 2020 at 14:39):

tidy can prove it too

#### Eric Wieser (Nov 25 2020 at 14:39):

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 (Nov 25 2020 at 14:40):

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

#### Reid Barton (Nov 25 2020 at 14:40):

then cases x; refl instead

#### Reid Barton (Nov 25 2020 at 14:53):

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 (Nov 25 2020 at 14:59):

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 (Nov 25 2020 at 15:00):

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

#### Reid Barton (Nov 25 2020 at 15:00):

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

#### Eric Wieser (Nov 25 2020 at 15:00):

That's true of all simp lemmas though!

#### Reid Barton (Nov 25 2020 at 15:00):

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 (Nov 25 2020 at 15:01):

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

#### Reid Barton (Nov 25 2020 at 15:01):

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 (Nov 25 2020 at 15:01):

Which it is in #5112, which I just opened

#### Reid Barton (Nov 25 2020 at 15:01):

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

#### Reid Barton (Nov 25 2020 at 15:02):

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

#### Eric Wieser (Nov 25 2020 at 15:02):

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 (Nov 25 2020 at 15:04):

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 (Nov 25 2020 at 15:20):

Isn't hiding "obvious" dependencies fine though?

#### Eric Wieser (Nov 25 2020 at 15:21):

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 (Nov 25 2020 at 17:38):

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 (Nov 25 2020 at 17:46):

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 (Nov 25 2020 at 17:55):

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

#### Gabriel Ebner (Nov 25 2020 at 18:01):

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 (Nov 25 2020 at 18:25):

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 (Nov 25 2020 at 21:36):

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 (Nov 25 2020 at 21:37):

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

#### Eric Wieser (Nov 25 2020 at 21:39):

Would this problem go away if simp unfolded comp?

#### Kevin Buzzard (Nov 25 2020 at 21:39):

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

#### Kevin Buzzard (Nov 25 2020 at 21:40):

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

#### Kevin Buzzard (Nov 25 2020 at 21:43):

How about making function.comp [reducible]?

#### Kevin Buzzard (Nov 25 2020 at 21:44):

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

#### Yakov Pechersky (Nov 25 2020 at 21:45):

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 (Nov 25 2020 at 21:45):

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

#### Kevin Buzzard (Nov 25 2020 at 21:45):

What does @[inline] mean?

#### Kevin Buzzard (Nov 25 2020 at 21:47):

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

#### Yakov Pechersky (Nov 25 2020 at 21:47):

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 (Nov 25 2020 at 21:48):

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

#### Eric Wieser (Nov 25 2020 at 21:51):

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 (Nov 25 2020 at 21:53):

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 (Nov 25 2020 at 21:54):

hmm, thousands of occurrences in mathlib...

#### Eric Wieser (Nov 25 2020 at 21:55):

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

#### Kevin Buzzard (Nov 25 2020 at 23:12):

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 (Nov 26 2020 at 09:52):

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 (Nov 26 2020 at 10:24):

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 (Nov 26 2020 at 10:25):

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

#### Yakov Pechersky (Nov 26 2020 at 15:15):

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 (Nov 26 2020 at 15:33):

I'm suspicious about this map_map direction

#### Reid Barton (Nov 26 2020 at 15:33):

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

#### Reid Barton (Nov 26 2020 at 15:39):

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

#### Reid Barton (Nov 26 2020 at 15:40):

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

#### Gabriel Ebner (Nov 26 2020 at 15:57):

@Yakov Pechersky

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


IMHO, the only solution is to make ∘ semireducible.

Last updated: May 17 2021 at 16:26 UTC