Zulip Chat Archive

Stream: new members

Topic: squeeze_dsimp incorrect suggestion


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

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

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