squeeze_dsimp bug

Stream: general

[Tony Scholl]

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]

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

[Rob Lewis]

@Simon Hudon

[Rob Lewis]

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

[Simon Hudon]

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]

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]

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

[Simon Hudon]

#3431

[Sebastien Gouezel]

Could we have squeeze_dsimp and squeeze_dsimp!?

[Sebastien Gouezel]

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]

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

[Simon Hudon]

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]

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]

That should probably be a separate refactor, no?

[Bryan Gin-ge Chen]

Yeah, you're right.