## Stream: new members

### Topic: squeeze_dsimp incorrect suggestion

#### Horatiu Cheval (Apr 15 2021 at 05:26):

I have encountered several situations in which the dsimp only ... suggestion does not behave like the original squeeze_dsimp.
Should they always match, or is this expected behaviour? For example

import data.vector
import tactic

@[simp]
def f : ℕ → Type × Type
| 0 := (unit, unit)
| (n + 1) := (vector ℕ n, vector ℕ n.succ)

@[reducible, simp]
def g (x) := (f x).fst

example : unique $g 0 := begin squeeze_dsimp, -- simplifies to 'unique unit' -- and suggest 'dsimp obly [g]' apply_instance, end example : unique$ g 0 :=
begin
dsimp only [g],
-- simplifies to unique (f 0).fst
-- dsimp only [g, f] is actually needed
apply_instance,
end


#### Kevin Buzzard (Apr 15 2021 at 06:25):

Basically squeeze_simp is hard to write perfectly. Check out mathlib issues in GitHub, I think this is already there.

#### Johan Commelin (Apr 15 2021 at 06:26):

In other words, this is unfortunately expected behaviour, but we wouldn't mind if a C++ hacker made it unexpected behaviour :grinning:

Last updated: May 12 2021 at 23:13 UTC