Zulip Chat Archive

Stream: general

Topic: squeeze_dsimp bug


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

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

view this post on Zulip Rob Lewis (Jul 17 2020 at 09:30):

@Simon Hudon

view this post on Zulip Rob Lewis (Jul 17 2020 at 09:30):

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

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

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

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

view this post on Zulip Simon Hudon (Jul 17 2020 at 14:23):

#3431

view this post on Zulip Sebastien Gouezel (Jul 17 2020 at 14:32):

Could we have squeeze_dsimp and squeeze_dsimp!?

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

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

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

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

view this post on Zulip Simon Hudon (Jul 17 2020 at 14:40):

That should probably be a separate refactor, no?

view this post on Zulip Bryan Gin-ge Chen (Jul 17 2020 at 14:42):

Yeah, you're right.


Last updated: May 06 2021 at 21:09 UTC