How does one produce types (or theorems) from proof terms (programs or objects) in Coq?

Question

I was curious to learn about type inference in Coq. I wanted a concrete way in Coq to generate types (theorems) given a proof term/object/program. So given a proof term (perhaps with a hole, perhaps with not holes or perhaps a proof sub term) can I deterministically generate it's type? I was wondering if Coq provided this functionality for us for this e.g. in pseudo-Coq:

program := (fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n)
.

type := Coq.Proofterm_2_Type(program).

Print type.

What is the right function in Coq to do that: Given a proof term get me its type (type inference basically in Coq/Gallina).

---

I was playing around with this proof and it's proof objects:

Theorem add_easy_induct_1:
    forall n:nat,
      n + 0 = n.
  Proof.
    Show Proof.
    intros.
    Show Proof.
    induction n as [| n' IH].
    Show Proof.
    - simpl. reflexivity.
    Show Proof.
    - simpl. rewrite -> IH. reflexivity.
    Show Proof.
  Qed.

Print add_easy_induct_1.

some output examples:

?Goal
(fun n : nat => ?Goal)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) ?Goal
  (fun (n' : nat) (IH : n' + 0 = n') => ?Goal0) n)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') => ?Goal) n)
(fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n)
add_easy_induct_1 = 
fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n
     : forall n : nat, n + 0 = n

Arguments add_easy_induct_1 _%nat_scope

I used the really nice jsCoq while I wait Coq, Opam etc. to install in my new computer.

Answer 1

You can use Check to see the type of a term:

Let example := (fun n : nat =>
nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl
  (fun (n' : nat) (IH : n' + 0 = n') =>
eq_ind_r (fun n0 : nat => S n0 = S n') eq_refl IH)
  n).

Check example.
(*
example
     : forall n : nat, n + 0 = n
*)

Answer 2

Definition type_of {A} (_ : A) : Type := A.