Let’s consider this definition for a type for natural numbers:
Inductive t : Type :=
| O
| S (n : t).
I used to read this definition as
t
is an inductive type with two constructors -O
andS
, the latter taking a term of typet
as a parameter.
and from that, I used to conclude something like
All the terms of type
t
are of the formS (S ... (S O) ... )
, namely a bunch of (optional)S
’s, followed by a terminatingO
.
In fact, I based my intuition for induction on the statement above, but the statement is clearly incorrect, cus other terms can also have the type t
, for example (fun x : t => x) O
. But nonetheless, the “base” terms of t
, those on which no more reductions can be performed, are indeed a bunch of optional S
’s, terminated by an O
, right?
So, is there a notion of “values” of a type in Rocq? Maybe something like a term that isn’t reducible any further? I’ve seen the term inhabitant used at some places in the reference manual but I’m not sure what that means.
And, when you guys read a statement of the form forall n : t, n = n
, do you think of these n
’s as only the sequence of S
’s followed by an O
, or do you also think about terms like function applications, let-in expressions, etc? I suppose it doesn’t make much of a difference, though, because all of those terms are reducible to these “base” terms, so proving a proposition for the base terms is “enough” - but I still want to know how you guys “read” these inductive definitions and these propositions involving the universal quantifier.
Thanks a lot.