Curry Howard correspondence in Coq

Question

By Curry Howard correspondence, all theorems and lemmas are types and proof objects are values. As an example:

Theorem test:  0 <= 0.
Proof.
  omega. Qed.

When I do, Check test. Coq's output is:

test
     : 0 <= 0

But when I check the type of "<=", it is nat -> nat -> Prop. That means (0 <= 0) is of type Prop. Does this mean that the type 'test' is a subtype of Prop? In general, are theorem and lemma identifiers subtypes of Prop?

Answer 1

test : 0 <= 0 and 0 <= 0 : Prop, as you said. In the terminology of the Curry-Howard correspondence, 0 <= 0 is a type/theorem statement, and test is a value of that type/proof of that theorem.

There isn't any subtyping involved in this example. Subtyping is a relationship between two types; when Cat <: Animal (cat is a subtype of animal), it means all objects of type cat are also of type animal: x : Cat implies x : Animal.

Coq has one relatively simple form of subtyping, between type universes. The simplest example is that Prop is a subtype of Type. You can see this by using Check to confirm that 0 <= 0 : Prop and also 0 <= 0 : Type.