simp puzzles

Stream: general

[Floris van Doorn]

Consider the following proof:

import data.set.basic
example {α β} (f g : α → β) (h : ∀ x, f x = g x) (s : set α) : f '' s = g '' s :=
by simp*

Puzzle 1: Explain why simp succesfully proves this. (I will post the solution below.)
Puzzle 2: Is there any simp only [h, ...] invocation that solves this, using only lemmas that simp* used? simp only [h, set.image] works but doesn't count, because simp* didn't unfold set.image. (I have no idea how to do it / whether this is possible.)

This came up in #7250.

[Floris van Doorn]

Solution to puzzle 1

simp uses the congr-lemma docs#set.image_congr

@[congr] lemma image_congr {f g : α → β} {s : set α}
  (h : ∀a∈s, f a = g a) : f '' s = g '' s

Therefore, it can use the hypothesis h to rewrite inside set.image.

[Floris van Doorn]

Thoughts on puzzle 2

• squeeze_simp and simp? give (different) outputs that both fail to complete the goal.
• Interestingly, simp [*, - set.image_congr] also fails to complete the goal
• simp only [h, set.image_congr] or something similar doesn't work. Is there a bug here that we cannot add @[congr] lemmas to the simp-set, only remove them?

[Mario Carneiro]

congr lemmas aren't part of the simp set

[Floris van Doorn]

But simp [h, - set.image_congr] removes set.image_congr from something (the congr-set?). Can we make it so that simp only [h, set.image_congr] adds set.image_congr to that set?

[Mario Carneiro]

isn't that ambiguous? set.image_congr is a very bad simp lemma

[Mario Carneiro]

actually it's probably ineligible

[Floris van Doorn]

Maybe it is ambiguous, but can we allow simp to use congr-lemmas from the provided names? Currently it seems like we have a thing that simp can do but no simp only [...] invocation can do, which is bad when using squeeze_simp.

[Mario Carneiro]

I think the functionality is a good idea but I'm not sure how to make the syntax work

[Mario Carneiro]

we could do something like simp only [lemmas...] using congr [lemmas...]?