Zulip Chat Archive

Stream: triage

Topic: issue #3097: `squeeze_simp` produces invalid result

Random Issue Bot (Nov 05 2020 at 14:16):

Today I chose issue 3097 for discussion!

squeeze_simp produces invalid result
Created by @Gabriel Ebner (@gebner) on 2020-06-17
Labels: bug, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

Gabriel Ebner (Nov 05 2020 at 14:19):

I'd be happy to close this as wontfix, blocked-on-:lucky: since nobody runs into this accidentally from what it seems.

Johan Commelin (Nov 05 2020 at 14:24):

How hard would it be to make squeeze_simp use the lemmas that set_option trace.simplify.rewrites lists?

Johan Commelin (Nov 05 2020 at 14:24):

I guess that needs changes to the C++. But is it hard?

Gabriel Ebner (Nov 05 2020 at 14:29):

Main issue is that there's no way to get trace messages from the Lean side at the moment.

Gabriel Ebner (Nov 05 2020 at 14:30):

But if you're doing that, you might as well have the C++ record the list of lemmas used and return that.

Johan Commelin (Nov 05 2020 at 14:36):

Just to be clear: I don't think this is something that I can do. I'm just wondering how hard it is to get those trace messages from within the tactic state. Does it mean changing 5 lines of C++ or 500? Or even 5000?

Gabriel Ebner (Nov 05 2020 at 14:53):

Between 5-50, I'd guess.

Johan Commelin (Nov 05 2020 at 14:58):

Ok, I think that could (i) make squeeze_simp more reliable, and (ii) give it a significant speed-up.

(ii), because as I understand it, currently squeeze_simp is quadratic in the number of lemmas that are used, and this change would just drop that part completely.