How does the induction principle for the singleton type unit in Coq work?

Question

I was going through Adam Chlipala's book on Coq and it defined the inductive type:

Inductive unit : Set :=
  | tt.

I was trying to understand its induction principle:

Check unit_ind.
(* unit_ind
     : forall P : unit -> Prop, P tt -> forall u : unit, P u *)

I am not sure if I understand what the output of Coq means.

1) So check gives me a look at the type of "objects" right? So unit_ind has type:

forall P : unit -> Prop, P tt -> forall u : unit, P u

Right?

2) How does one read that type? I am having trouble understanding where to put the parenthesis or something...For the first thing before the comma, it doesn't make sense to me to read it as:

IF "for all P of type unit" THEN " Prop "

since the hypothesis is not really something true or false. So I assume the real way to real the first thing is this way:

forall P : (unit -> Prop), ...

so P is just a function of type unit to prop. Is this correct?

I wish this was correct but under that interpretation I don't know how to read the part after the first comma:

P tt -> forall u : unit, P u

I would have expected all the quantifications of variables in existence to be defined at the beginning of the proposition but thats not how its done, so I am not sure what is going on...

Can someone help me read this proposition both formally and intuitively? I also want to understand conceptually what it's trying to say and not only get bugged down by the details of it.

Anton Trunov Anton Trunov · Accepted Answer · 2018-12-16T21:44:21

Let me put some extra (not really necessary) parentheses:

forall P : unit -> Prop, P tt -> (forall u : unit, P u)

I would translate it as "For any predicate P over the unit type, if P holds of tt, then P holds of any term of type unit".

Intuitively, since tt is the only value of type unit, it makes sense to only prove P for this unique value.

You can check if this intuition works for you by trying to interpret the induction principle for the bool type in the same manner.

Check bool_ind.
bool_ind
     : forall P : bool -> Prop, P true -> P false -> (forall b : bool, P b)

How does the induction principle for the singleton type unit in Coq work?

1 Answers