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