wrong proof terms

Stream: general

[Mingzhe Wang]

I found that the proof terms are sometimes wrong as shown in the following example. Is there a way to get the correct proof term or fix the wrong proof term automatically?

-- this one could work
lemma test : 0 ≤ 1:=
begin
/-
Try this: exact 1.zero_le
-/
show_term{exact nat.zero_le 1},
end

-- we print the proof term which is the same as show_term
/-
theorem hoare_logic.test : 0 ≤ 1 :=
1.zero_le
-/
#print test

-- but the proof term doesn't work
lemma test1: 0 ≤ 1 := 1.zero_le
/-
invalid field notation, type is not of the form (C ...) where C is a constant
1
has type
?m_1
-/

[Kevin Buzzard]

Lean doesn't know the type of 1 in your proof term. In fact from your test lemma it's not entirely clear that you know the type of 1 either. Did you know that lean has many different 1s? Say which one you mean with eg (1 : Nat) and the problem should go away.

[Kyle Miller]

@Kevin Buzzard I think the question is about the fact that show_term pretty prints terms that can't be pasted back in. They already have nat.zero_le 1 for example

[Kevin Buzzard]

Ok, yes, that is true. Round tripping is hard!

[Kyle Miller]

In this case, I think it's set_option pp.structure_projections false that will turn off this "dot notation" and help show_term print something usable.

[Kyle Miller]

You could also do set_option pp.all true to get it to print something closer to the full form of the proof term.

[Kyle Miller]

Anyway, it's not the proof term that's wrong (thankfully), it's how the proof term is being pretty printed that's wrong.

[Mingzhe Wang]

Thanks Kevin and Kyle! WIth set_option pp.all true, I got the correct proof term!

[Kevin Buzzard]

Yeah that's definitely a way to increase the chances of round tripping working :-)