## Stream: general

### Topic: squeeze_dsimp bug

#### Tony Scholl (Jul 17 2020 at 09:15):

With Kevin's help I came up with a bug in squeeze_dsimp:

import topology.metric_space.basic

open_locale classical filter topological_space

namespace lftcm
open filter set

/-!
# Filters

## Definition of filters
-/

def principal {α : Type*} (s : set α) : filter α :=
{ sets := {t | s ⊆ t},
univ_sets := begin
simp only [subset_univ, mem_set_of_eq],
end,
sets_of_superset := begin
squeeze_dsimp,
intros x y h1 h2,
transitivity x ; assumption,
end,
inter_sets := begin
sorry,
end}

end lftcm


Lean suggests dsimp only [] but this breaks the proof!

#### Kevin Buzzard (Jul 17 2020 at 09:16):

(just to add -- Tony was asking about squeeze_dsimp so I told him to do leanproject up ;-) )

@Simon Hudon

#### Rob Lewis (Jul 17 2020 at 09:30):

Really going after cutting-edge features here, squeeze_dsimp is four hours old!

#### Simon Hudon (Jul 17 2020 at 13:19):

squeeze_dsimp is probably not to be trusted completely. Because dsimp preserves definitional equality, it can use lemmas without them being obviously used.

#### Simon Hudon (Jul 17 2020 at 13:32):

I'm going to look into the issue, maybe it can be made more reliable. Do you have an example that doesn't use topology?

#### Simon Hudon (Jul 17 2020 at 14:10):

The good news is that there's a way to make it more reliable but this call takes 2 min to complete

#3431

#### Sebastien Gouezel (Jul 17 2020 at 14:32):

Could we have squeeze_dsimp and squeeze_dsimp!?

#### Sebastien Gouezel (Jul 17 2020 at 14:33):

Or try the first strategy, then the tactic would try its output, see if the new goal matches what is should be, and if it doesn't switch to the slow strategy?

#### Simon Hudon (Jul 17 2020 at 14:33):

That's an option. The same technique could apply for squeeze_simp but ! has a meaning already. We could use ? instead

#### Simon Hudon (Jul 17 2020 at 14:34):

I hadn't considered that. That's an interesting option. I think having a ? flag might have the added benefit that if you convert a whole file at once, you won't have a lot of calls holding you up.

#### Bryan Gin-ge Chen (Jul 17 2020 at 14:38):

I think it'd be most intuitive to make dsimp? do what squeeze_dsimp does, along the lines of #2706. (Would we need a dsimp?? for the slower version?)

#### Simon Hudon (Jul 17 2020 at 14:40):

That should probably be a separate refactor, no?

#### Bryan Gin-ge Chen (Jul 17 2020 at 14:42):

Yeah, you're right.

Last updated: May 06 2021 at 21:09 UTC