How do inductive proposition work in Coq?

Question

I was going through IndProp in software foundations and Adam Chlipala's chapter 4 book and I was having difficulties understanding inductive propositions.

For the sake of a running example, lets use:

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

I think I do understand "normal" types using Set like:

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

and things like O just return the single object of type nat and S O is taking an object of type nat and returning another different one of the same type nat. By different object I guess I mean they have different values.

What I am confused is on how exactly the constructors for inductive props differ from inductive types Set. For Set it seems they just behave as function, a function that take values and return more values of that type. But for Inductive Propositions I am having a hard time figuring out what they do.

For example take ev_0 as a simple example. I assume that is the name for the propositional object (value) ev 0. Since it's by itself ev 0 must be a Prop a proposition. But what exactly makes it true? If its a proposition it could be false I assume. I guess the induction is confusing me. ev is the "function that returns objects of some type (proposition)", so ev 0 is just a proposition, but we have not said what ev 0 should mean (unlike in my definition of natural number the base case is clear what its doing). In python I would expect to see

n == 0: return True

or something for the base case. But in this case it seems circular pointing to itself and not to something like True. I know there is a foundational misconception I have but I don't know what exactly what I am not understanding.

Also whats confusing me is the naming. In the nat the name O was crucial for building/constructing objects. But in the inductive definition ev_0 seems to be more like a label/pointer to the real value ev 0. So I'd assume ev_SS == ev_0 -? ev 2 doesn't really make sense but I don't know why. How are the labels here acting differently from the labels in the inductive types using set?

For ev_SS thats even more confusing. Since I don't know what labels are doing of course thats confusing me but look how this is pointing:

forall n : nat, ev n -> ev (S (S n))

so given a natural number n I assume it returns the proposition ev n -> ev (S (S n)) (I am assuming forall n : nat is not part of the proposition object and its just there to indicate when the constructer that returns propositions works). So forall n : nat, ev n -> ev (S (S n)) isn't really a proposition but ev n -> ev (S (S n)).

Can someone help me clarify how inductive proposition type really work in Coq?

---

Note I don't truly understand the difference between Set vs Type but I believe that would be a whole other post by itself.

---

Some more comments:

I was playing around with this some more and did:

Check ev_SS

and to my surprise got:

ev_SS
     : forall n : nat, ev n -> ev (S (S n))

I think this is unexpected because I didn't expect that the type of ev_SS (unless I am misunderstanding what Check is suppose to do) would be the definition of the function itself. I thought that ev_SS was a constructor so in my mind I thought that would do a mapping in this case nat -> Prop so of course thats the type I expected.

Answer 1

So, first, it is normal for you to be confused by this, but it might be simpler than what you think!

There are two distinct concepts you are confused about, so let's take them one at a time. First, you mention that ev 0 is a proposition, and wonder what makes it true. You will learn at some point that propositions and types are the same things, and the distinction between Prop and Set and Type is not that those things are different inherently.

So, when you define the type (or proposition) nat, you are creating a new type, and describing what values exist within it. You declare that there is a value O, that is a nat. And you declare that there is a parameterized value S, that is a nat, when passed a nat.

In the same way, when you define the type (or proposition) ev, you are creating a new type (well, it's actually a family of types indexed by values of type nat), and describing what values exist within those ev types. You declare that there is a value ev_0, that is an ev 0. And you declare that there is a parameterized value ev_SS, that is an ev (S (S n)), when passed a n : nat and an ev n.

So you made the proposition be true by having ways of creating values within it. You can also define a false proposition by having no constructors, or having constructors that can never be called:

Inductive MyFalse1 := . (* no constructor! *)

Inductive MyFalse2 :=
| TryToConstructMe : False ->  MyFalse2
| ThisWontWorkEither : 0 = 1 -> MyFalse2
.

I have declared two now types (or proposition), but there's no way to witness them because they either have no constructors, or no way to ever call those constructors.

---

Now regarding the naming of things, ev_0, ev_SS, O, and S are all the same kind of entity: a constructor. I'm not sure why you think that ev_0 is a pointer to a value ev 0.

There is no meaning to assign to ev n as a proposition, other than it's a proposition that may be true if there is a way to construct a value with type ev n, and may be false if there is no way to construct a value with type ev n.

However, note that ev n has been carefully crafted to be inhabited for exactly those ns that are even, and to be uninhabited for exactly those ns that are odd. It's in this sense that ev captures a proposition. If you receive a value of type ev n, it essentially asserts that n is an even number, because the type ev n only contains inhabitants for even values:

• ev 0 contains 1 inhabitant (ev_0)
• ev 1 contains 0 inhabitant
• ev 2 contains 1 inhabitant (ev_SS 0 ev_0)
• ev 3 contains 0 inhabitant
• ev 4 contains 1 inhabitant (ev_SS 2 (ev_SS 0 ev_0))
• etc.

---

Finally, for the difference between Set, Prop, and Type, these are all universes within which you can create inductive types, but they come with certain restrictions.

Prop enables an optimization for code generation. It's essentially a way for you, the programmer, to mark some type as being only used for verification purposes, never used for computation purposes. As a result, the type-checker will force you to never compute on proofs within the Prop universe, and the code generation will know that it can throw away those proofs as they don't participate in computational behavior.

Set is just a restriction of Prop to avoid dealing with universe levels. You don't really need to understand this until later in your learning process.

You should really try to not think of Prop as being a magical thing different than Set.

---

The following might help you: we could rewrite the definitions of nat and ev, in a completely equivalent way, as:

Inductive nat1 : Set :=
| O : nat1
| S : nat1 -> nat1
.
(* is the same as *)
Inductive nat1 : Set :=
| O : nat1
| S : forall (n : nat1), nat1
.

(* and *)
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall (n : nat), ev n -> ev (S (S n))
.
(* is the same as *)
Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall (n : nat) (e : ev n), ev (S (S n))
.

Any time you see a type looking like a -> b, it's really a short-hand for forall (_ : a), b, that is, we expect an input of type a, and return an output of type b.

The reason why we write forall (n : nat) in ev_SS is that we have to give a name to the first argument, because the type of the second argument will depend on it (the second argument has type ev n).

Answer 2

If you replace Prop with Set then you say you understand the definition:

Inductive ev' : nat -> Set :=
| ev_0' : ev' 0
| ev_SS' : forall n : nat, ev' n -> ev' (S (S n)).

For every n : nat we think of ev' n as a type which has some elements, or perhaps none. Because this is an inductive definition, we can tell what the elements of ev' 0 are: the only element is ev_0' (or to be more precise, every closed term of type ev' 0 computes to ev_0;). There are no elements of ev_0 1, but there is an element of ev 2', namely ev_SS' 0 ev_0'. In fact, a little bit of thinking shows that ev n is either empty or a singleton, depending on whether n is even or odd.

It's exactly the same when we switch from Set to Prop, except that the reading is different: Set is a (large) type of types, Prop is also a type of types (they are universes). Each element of Prop is a type (but we prefer to call it a "proposition") which has some elements (but we prefer to call them "proofs"). So consider this:

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

For every n : nat, we think of ev n as the statement that n has the property ev, whatever that property might be. For any give n, there may be a proof of ev n, in which case n has the property ev, or there may be no such proof, in which case n does not have the property ev. Because this is an inductive definition, we can tell what the proofs of ev_0 are: they all compute to ev_0'. There are no proofs of ev_0 1, but there is a proof of ev 2, namely ev_SS 0 ev_0. In fact, a little bit of thinking shows that ev n has a proof if, and only if, n is even. We now understand that ev is the property of being "even".

This is knows as "propositions as types".

We observed that ev' 0 contains just one element ev_0'. The type unit also contains just one element tt. Does this mean that ev' 0 and unit are equal? No, but they are equivalent because we can provide functions ev' 0 -> unit and unit -> ev' 0 which are inverses of each other.

We can ask the same question about ev 0: is it equal to True? No, but they are equivalent because we can prove the implications ev 0 -> True and True -> ev' 0.

One starts to wonder what the difference between Prop and Set is. For a type P : Prop all of its elements are considered equal, i.e., Coq does not allow us to distinguish between them. (This is a bit of a pedagocical lie, because in reality Coq is agnostic about whether all the element of P are considered equal, but perhaps it's better not to get into this right now.)