Coq how to pretty-print a term constructed using tactics?

I'm new to Coq and am doing some exercises to get more familiar with it.

My understanding is that proving a proposition in Coq "really" is writing down a type in Gallina and then showing that it's inhabited using tactics to combine terms together in deterministic ways.

I'm wondering if there's a way to get a pretty-printed representation of the actual term, with all the tactics removed.

In the example below, an anonymous term of type plus_comm (x y : N) : plus x y = plus y x is ultimately produced... I think. What should I do if I want to look at it? In a certain sense, I'm curious what the tactics "desugar" to.

Here's the code in question, lifted essentially verbatim from a tutorial on YouTube https://www.youtube.com/watch?v=OaIn7g8BAIc.

Inductive N : Type :=
| O : N
| S : N -> N
.

Fixpoint plus (x y : N) : N :=
match x with
| O => y
| S x' => S (plus x' y)
end.

Lemma plus_0 (x : N) : plus x O = x.

Proof.
  induction x.
  - simpl. reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.

Lemma plus_S (x y : N) : plus x (S y) = S(plus x y).

Proof.
  induction x.
  - simpl. reflexivity.
  - simpl. rewrite IHx. reflexivity.
Qed.


Lemma plus_comm (x y : N) : plus x y = plus y x.

Proof.
  induction x.
  - simpl. rewrite plus_0. reflexivity.
  - simpl. rewrite IHx. rewrite plus_S. reflexivity.
Qed.

Solution

First of all, plus_comm is not a part of the type. You get a term named plus_comm of type forall x y : N, plus x y = plus y x. You can check it using the following command

Check plus_comm.

So, an alternative way of defining the plus_comm lemma is

Lemma plus_comm : forall x y : N, plus x y = plus y x.

As a side note: in this case you'll need to add intros x y. (or just intros.) after the Proof. part.

Tactics (and the means to glue them together) are a metalanguage called Ltac, because they are used to produce terms of another language, called Gallina, which is the specification language of Coq.

For example, forall x y : N, plus x y = plus y x is an instance of Gallina sentence as well as the body of the plus function. To obtain the term attached to plus_comm use the Print command:

Print plus_comm.

plus_comm = 
fun x y : N =>
N_ind (fun x0 : N => plus x0 y = plus y x0)
  (eq_ind_r (fun n : N => y = n) eq_refl (plus_0 y))
  (fun (x0 : N) (IHx : plus x0 y = plus y x0) =>
   eq_ind_r (fun n : N => S n = plus y (S x0))
     (eq_ind_r (fun n : N => S (plus y x0) = n) eq_refl (plus_S y x0))
     IHx) x
     : forall x y : N, plus x y = plus y x

It is not an easy read, but with some experience you'll be able to understand it.

Incidentally, here is how we could have proved the lemma not using tactics:

Definition plus_comm : forall x y : N, plus x y = plus y x :=
  fix IH (x y : N) :=
    match x return plus x y = plus y x with
    | O => eq_sym (plus_0 y)
    | S x => eq_ind _ (fun p => S p = plus y (S x)) (eq_sym (plus_S y x)) _ (eq_sym (IH x y))
    end.

To explain a few things: fix is the means of defining recursive functions, eq_sym is used to change x = y into y = x, and eq_ind corresponds to the rewrite tactic.