## 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.

#### Patrick Massot (Nov 05 2020 at 15:14):

Can anyone recommend a good C++ book to Johan?

#### Johan Commelin (Nov 05 2020 at 15:16):

/me is using >50% of his work week on teaching, another 20% on seminars, another 20% on reviewing PRs.... so there is 5-10% left for research...

#### Simon Hudon (Nov 05 2020 at 15:26):

And this book looks good to me but I haven't used it: link

lean#497

#### Johan Commelin (Nov 09 2020 at 21:59):

/me has to go back to teaching Lie algebras now

#### Random Issue Bot (Dec 19 2020 at 14:26):

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?

Last updated: May 09 2021 at 15:11 UTC