Zulip Chat Archive

Stream: general

Topic: fooling `squeeze_simp`

Kevin Buzzard (May 20 2022 at 15:06):

import tactic

example (a b : ) : (a+b)^3=a^3+3*a^2*b+3*a*b^2+b^3 :=
  squeeze_simp [show (a+b)^3=a^3+3*a^2*b+3*a*b^2+b^3, by ring]

succeeds, and suggests

Try this: simp only [show ((fun (this : (frozen_name eq) ((frozen_name has_pow.pow) ((frozen_name has_add.add) a b) 3) ((frozen_name has_add.add) ((frozen_name has_add.add) ((frozen_name has_add.add) ((frozen_name has_pow.pow) a 3) ((frozen_name has_mul.mul) ((frozen_name has_mul.mul) 3 ((frozen_name has_pow.pow) a 2)) b)) ((frozen_name has_mul.mul) ((frozen_name has_mul.mul) 3 a) ((frozen_name has_pow.pow) b 2))) ((frozen_name has_pow.pow) b 3))), this) (by (typed_expr (tactic unit) (interactive.executor.execute_explicit tactic (has_bind.seq (tactic.save_info (anonymous_constructor (4._.9 5 57))) (tactic.istep 5 57 5 57 80 (tactic.interactive.ring (as_is (option.none.{0} unit)))))))))]

which unsurprisingly doesn't work. Probably a wontfix but thought it was good for a laugh on a Friday afternoon.

Eric Rodriguez (May 20 2022 at 15:32):

cc @Arthur Paulino - can we make a whacky amalgamation of pp and to_string to fix this?

Eric Rodriguez (May 20 2022 at 15:32):

do people know if this was an issue in the past? I'm wondering how to control this

Arthur Paulino (May 20 2022 at 15:33):

Given the priority I would mark it to be solved in Lean 4 since we have more metaprogramming power there

Arthur Paulino (May 20 2022 at 15:34):

(not that this would be too complicated, it's just that the solution here wouldn't necessarily be translated to Lean 4)

Eric Rodriguez (May 20 2022 at 15:35):

there's a similar issue that @Julian Berman reported:

changed line 526 of measure_theory/decomposition/jordan.lean to squeeze_simp

I'll try some quick fixes and see what it can do

Kevin Buzzard (May 20 2022 at 19:37):

I'm not really suggesting this needs fixing, I just thought it was funny :-)

Mario Carneiro (May 20 2022 at 19:37):

Yep, this is ~hopeless in lean 3, it needs actual AST data. We have that now, but not AST printing

Mario Carneiro (May 20 2022 at 19:38):

it is something that occasionally annoys me about squeeze_simp, it might be better if it just tells me what to add and delete from my list instead of trying and failing to print what I wrote

Last updated: Aug 03 2023 at 10:10 UTC