battling with large pp.all terms

Stream: general

[Kevin Buzzard]

Is it possible to have some sort of tool where large pp.all terms can be folded up in manageable ways -- I am looking at a term that starts @eq alpha (XXXXXXXXXXXXXXXX...) (YYYYYYYYYYYYYYYYYYY.....) and I would like to see the head term of YYYYY... but it's hard to find in the pp.all output.

[Simon Hudon]

Have you tried other pp options?

[Mario Carneiro]

I would get the expr out with tactics

[Mario Carneiro]

set_option pp.all true
open tactic
example (fooooooo barrrrrrrrr : ℕ) : fooooooo = barrrrrrrrr :=
by do `(%%_ = %%e) ← target,
  pp e >>= trace

[Kevin Buzzard]

convert rfl is not safe to use! You don't want to try proving mul_comm with it.

example (X : Type) [comm_group X] (a b  : X) : a * b = b * a :=
begin intros,
convert rfl, -- ⊢ b = a
  repeat {sorry},
end

I would like to be able to do some more delicate analysis

[Mario Carneiro]

there is a :1 argument for convert I think

[Mario Carneiro]

convert rfl using 0

[Mario Carneiro]

hm, congr' 0 fails because it makes no progress. I think convert needs to be fixed to reflect that

[Mario Carneiro]

oh but in your case it's fine because you want congr' 1 anyway

[Mario Carneiro]

example (X : Type) [comm_group X] (a b  : X) : a * b = b * a :=
begin intros,
  convert rfl using 1, -- ⊢ b * a = a * b
  repeat {sorry},
end

[Mario Carneiro]

that said, convert rfl looks pretty useless

[Kevin Buzzard]

convert rfl` is really good when you have two terms which are defeq up to subsingleton typeclass inference equality issues

[Mario Carneiro]

isn't that just congr'?

[Kevin Buzzard]

This happened to me a fair bit when I was doing sheaves.

[Kevin Buzzard]

Maybe; I don't know the difference between congr and congr', I don't really understand them properly.

[Mario Carneiro]

congr' is congr with bugfixes

[Mario Carneiro]

and a depth limiter

[Kevin Buzzard]

I've never used it without 1

[Jesse Michael Han]

i also thought convert rfl using k is equivalent to congr' k