fooling `squeeze_simp`

Stream: general

[Kevin Buzzard]

import tactic

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

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]

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

[Eric Rodriguez]

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

[Arthur Paulino]

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

[Arthur Paulino]

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

[Eric Rodriguez]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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