Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 25 2020 at 14:36):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 25 2020 at 14:37):

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

view this post on Zulip Eric Wieser (Nov 25 2020 at 14:38):

I had no idea ext took rcases-style patterns

view this post on Zulip Reid Barton (Nov 25 2020 at 14:38):

I think that might be a somewhat recent feature

view this post on Zulip Reid Barton (Nov 25 2020 at 14:39):

tidy can prove it too

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 25 2020 at 14:40):

then cases x; refl instead

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 25 2020 at 15:00):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 25 2020 at 15:00):

That's true of all simp lemmas though!

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 25 2020 at 15:01):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 25 2020 at 15:01):

Which it is in #5112, which I just opened

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 25 2020 at 15:02):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Nov 25 2020 at 15:20):

Isn't hiding "obvious" dependencies fine though?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Nov 25 2020 at 17:55):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Nov 25 2020 at 21:39):

Would this problem go away if simp unfolded comp?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:43):

How about making function.comp [reducible]?

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 21:43):

Isn't it already?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:45):

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

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:45):

What does @[inline] mean?

view this post on Zulip 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?

view this post on Zulip 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"

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 21:48):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 25 2020 at 21:54):

hmm, thousands of occurrences in mathlib...

view this post on Zulip Eric Wieser (Nov 25 2020 at 21:55):

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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip Eric Wieser (Nov 26 2020 at 10:25):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 26 2020 at 15:33):

I'm suspicious about this map_map direction

view this post on Zulip Reid Barton (Nov 26 2020 at 15:33):

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

view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 26 2020 at 15:40):

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

view this post on Zulip 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