squeeze_dsimp is a lie

Stream: general

[Kevin Buzzard]

Does squeeze_dsimp actually ever report anything other than dsimp only? Amelia showed me a situation where dsimp worked, squeeze_dsimp reported dsimp only, which didn't work, and squeeze_simp reported simp only [a bunch of lemmas which are true by refl] and then dsimp only [those lemmas] worked. And indeed it's pretty easy to reproduce:

import algebra.associated
-- import random file which contains a simp lemma whose proof is `rfl`, in this case
-- `@[simp] lemma associates.mk_one [monoid α] : associates.mk (1 : α) = 1 := rfl`

example (α : Type) [monoid α] : associates.mk (1 : α) = 1 :=
begin
  squeeze_simp, -- `simp only [associates.mk_one]`
  -- goals accomplished
end

example (α : Type) [monoid α] : associates.mk (1 : α) = 1 :=
begin
  dsimp,
  -- ⊢ 1 = 1
  refl
end

example (α : Type) [monoid α] : associates.mk (1 : α) = 1 :=
begin
  squeeze_dsimp, -- `dsimp only`
  -- ⊢ 1 = 1
  refl
end

example (α : Type) [monoid α] : associates.mk (1 : α) = 1 :=
begin
  dsimp only, -- error: tactic failed to simplify
end

example (α : Type) [monoid α] : associates.mk (1 : α) = 1 :=
begin
  dsimp only [associates.mk_one],
  -- ⊢ 1 = 1
  refl
end

[Kevin Buzzard]

I was quite surprised to find that simp tracing and dsimp tracing seemed to be two totally different systems, when trying to understand what was going on.

[Martin Dvořák]

Yes. I have places where squeeze_dsimp correctly outputs dsimp only [list.map] for example.

[Martin Dvořák]

That said, we all know squeeze_dsimp is unreliable.

[Martin Dvořák]

To be honest, I don't know whether squeeze_dsimp ever outputs a rfl lemma. In my cases, they were definitions that were expanded.

[Kevin Buzzard]

Aah, very good! So if it manages to use an equation lemma, it might print something?

-- Lean 3
import tactic

#print prefix list.map

/-
list.map : Π {α : Type u} {β : Type v}, (α → β) → list α → list β
list.map._main : Π {α : Type u} {β : Type v}, (α → β) → list α → list β
list.map._main._meta_aux : Π {α : Type u} {β : Type v}, (α → β) → list α → list β
list.map._main.equations._eqn_1 : ∀ {α : Type u} {β : Type v} (f : α → β), list.map._main f list.nil = list.nil
list.map._main.equations._eqn_2 : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (l : list α),
  list.map._main f (a :: l) = f a :: list.map._main f l
list.map._sunfold : Π {α : Type u} {β : Type v}, (α → β) → list α → list β
list.map.equations._eqn_1 : ∀ {α : Type u} {β : Type v} (f : α → β), list.map f list.nil = list.nil
list.map.equations._eqn_2 : ∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (l : list α), list.map f (a :: l) = f a :: list.map f l
-/

example (α β : Type) (f : α → β) : list.map f list.nil = list.nil :=
begin
  squeeze_dsimp, -- Try this: dsimp only [list.map]
  -- ⊢ list.nil = list.nil
  refl,
end

example (α β : Type) (f : α → β) : list.map f list.nil = list.nil :=
begin
  dsimp only [list.map],
  -- ⊢ list.nil = list.nil
  refl,
end

[Martin Dvořák]

Yes but it isn't enough for squeeze_dsimp to be really useful.

[Martin Dvořák]

It might be the case that squeeze_dsimp is better at suggesting unfold [...] than suggesting dsimp only [...] maybe.