Leans version of "Show Proof"?

Stream: general

[Aaron Bies]

In Coq, you can display the proof term whenever you're in proof mode using the Show Proof tactic.

Goal forall (A B : Prop), A -> B -> A.
Proof.
  intros A B.
  Show Proof. (*  (fun A B : Prop => ?Goal)  *)
  intros a b.
  Show Proof. (*  (fun (A B : Prop) (a : A) (b : B) => ?Goal)  *)
  exact a.
  Show Proof. (*  (fun (A B : Prop) (a : A) (_ : B) => a)  *)
Qed.

Is there a way to do the same in Lean?

I have noticed you can #print a theorem to inspect the proof term, but is there something I can do in examples or halfway into a proof?

[Wrenna Robson]

show_term will do what you want I think.

[Wrenna Robson]

You can use it around a particular tactic, but you could also use it around the whole proof thus far.

[Wrenna Robson]

It's often, to be fair, not very useful.

[Aaron Bies]

Took me a moment to figure out how to use it

example (A B : Prop) : A → B → A :=
by show_term {
  intros a b,
  exact a,
}

[Aaron Bies]

I really like that this gives me a clickable Try this: exact λ (a : A) (b : B), a rather than just printing it in the console

[Aaron Bies]

and it also cancels out the by and exact while it's at it :D

[Aaron Bies]

Thank you!

[Wrenna Robson]

No worries :)

[Wrenna Robson]

Are you familiar with refine?

[Aaron Bies]

yes

[Wrenna Robson]

I ask only because that's often very useful for finding a nice term for part or the whole or a proof

[Aaron Bies]

ooooh
image.png

[Aaron Bies]

That's so cool!

[Wrenna Robson]

Yeah I'm not entirely sure that will work as written, sometimes the show_term output doesn't.

[Wrenna Robson]

But indeed refine \l a b, _ will then give you a state with a as a goal.

[Wrenna Robson]

(on phone so can't do lambda)

[Wrenna Robson]

You could also simply omit the by, and write \l ab, _ after the :=, and then if you click on the red underline you'll see what is missing

[Wrenna Robson]

So really often you can just do things term-wise that way.

[Wrenna Robson]

I'm sure you're also aware of rcases and rintros but they are also useful tools when you're hunting for a neat term

[Damiano Testa]

As has been pointed out, sometimes the Try this: needs some cleaning up. show_term is normally useful with the most "transparent" tactics: refine, apply, intros, split, left, right,.... It tends to be less useful with rw, simp,....

I personally found it useful to learn about how Lean works with coe/cast. show_term{(something)_cast}, is normally a huge term, which, however, contains the names of the lemmas that are used. Sometimes, this can help with replacing a norm_cast with a sequence of rw. Besides masochism, a motivation for doing this is to speed up some proofs.

[Jason Rute]

@Aaron Bies FYI: tactic.trace_result is a more literal translation of Show Proof. (You must import tactic which is available in base Lean.)