Should I expect show_term output to type-check?

Stream: new members

[Jason Orendorff]

If I add by show_term to the beginning of this proof, the output looks fairly sensible, but it fails to type-check in a couple places. Is that expected? https://gist.github.com/jorendorff/8229ce03eb29e6031602f4003bfbf153

[Jason Orendorff]

Both errors are around eq.rec, which I guess has special elaborator support. I wasn't able to fix either one just by adding type-annotations; one I was able to fix by adding a call to iff_of_eq and a type annotation

[Jason Orendorff]

the other one, I gave up

[Reid Barton]

Did it try to use dot notation for eq.rec?

[Scott Morrison]

The general answer is unfortunately "No, you should not expect output from the pretty printer to always round-trip. There's no perfect balance between readable output and correct output." But special cases may be fixable!

[Jason Orendorff]

Did it try to use dot notation for eq.rec?

No, that wasn't the problem. Here's the output, with comments telling what the errors were https://gist.github.com/jorendorff/8229ce03eb29e6031602f4003bfbf153#file-uniqueness_show_term_output-lean

[Kevin Buzzard]

I find those sorts of puzzles quite messy to solve. You can probably get everything compiling if you tell Lean the types of a few terms (i.e. replace x with (x : X)) but if you don't understand the proof properly it's difficult to fathom out what the terms are (for me, at least)

[Jason Orendorff]

I was really surprised that I wasn't able to fix these errors using type annotations.

[Kevin Buzzard]

If you set_option pp.all true you are much more likely to get something which survives the round trip -- and also much more likely to get something which is unwieldy and incomprehensible

[Jason Orendorff]

oh! but i can be selective... thanks

[Kevin Buzzard]

if you can see the wood from the trees

[Jason Orendorff]

it actually translates pretty cleanly, because almost all of my proof uses extremely simple tactics

[Jason Orendorff]

I think I'll try again with the type annotations; I was tired when I tried it last night

[Jason Orendorff]

(probably 97% of the problem honestly)

[Reid Barton]

This is basically the stupidity of the stupid triangle in action

[Reid Barton]

rw is just better than the Lean elaborator

[Kevin Buzzard]

@Jason Orendorff do you know about the widgety VS Code extension? This makes your job a lot easier.

[Kevin Buzzard]

The widget version of the VS Code extension shows you the expected type of everything in that pp.all mess.

[Kevin Buzzard]

I pasted in the @eq.rec stuff in the two places where you had an error, and now I get another error in a new place :-(

[Jason Orendorff]

heh!!

[Jason Orendorff]

The first one is big

[Kevin Buzzard]

stupid computer

[Jason Orendorff]

pasting it worked for me just now

[Kevin Buzzard]

Nice! I might well have slipped up then.

[Jason Orendorff]

hmm, even the fully expanded version times out on codewars.com, but that's a separate issue...

[Kevin Buzzard]

Give an upvote to the codewars version upgrade which will make everything twice as fast :-)

[Jason Orendorff]

is that ... an issue somewhere that i can vote on, or...?

[Kevin Buzzard]

I think it was mentioned in #Codewars

[Jalex Stark]

making things faster is a good exercise :slight_smile:

[Reid Barton]

I'm very surprised that the original proof times out

[Jason Orendorff]

Submitting an empty program times out! Apparently it is timing out trying to check mathlib's basic topology definitions and lemmas

[Reid Barton]

Well then

[Jason Orendorff]

Details in https://github.com/codewars/codewars-runner-cli/issues/824#issuecomment-646731296