Inductive types are similar to Haskell's
data, but they are more general.
An inductive definition in
Set describes a way to build a piece of data from smaller pieces. For example, the following definition defines a type called
prod which allows taking two pieces of data and bundling them together.
Inductive prod (A B : Set) : Set := pair : A -> B -> prod A B.
(This definition exists in the standard library — with
Type rather than
Set, but I won't get into that distinction in my answer.) In English, given two data types
B, and given a value
a of type
A and a value
b of type
B, I can build the value
pair a b which has the type
prod A B. (In the standard library, there's syntactic sugar for this:
(a, b) : A * B.) And this is the only way to build a value of the type
prod A B: given a value of this type, I can extract the two values that make it up (the primitive syntax for that is pattern matching, both in Haskell and in Coq).
You could take the same definition, but with
Prop, and construct a type in
Inductive pprod (A B : Prop) : Prop := ppair : A -> B -> pprod A B.
What does this mean? Let's go through the English explanation above, applying the Curry-Howard correspondence: types become propositions, and values become proofs. So, given two propositions
B, and given a proof
a of the proposition
A and a proof
b of the proposition
B, I can build a proof
ppair a b which has the type
pprod A B. And this is the only way to build a proof of
pprod A B.
To build a proof of
pprod A B, I need a proof of
A and a proof of
B. In other words,
pprod A B is true if
B are both true. There's a name for that: it's the conjunction of the two propositions —
pprod A B is “A and B”.
Well, in the standard library, there's syntactic sugar for this:
pprod is called
and — the definition is
Inductive and (A B : Prop) : Prop := conj : A -> B -> and A B.
and there's syntactic sugar for
and A B which is
A /\ B.
This is pretty typical of how Coq works. In Coq, to say that something is true is to hold a proof of it. Coq implements a constructive logic, and makes that logic apparent. Every time you prove something, Coq builds the proof object and verifies that it's well-formed. It's rare to write down constructions in
Prop, you'd usually let a tactic do it for you, but the objects always exist under the hood. (End a proof with
Defined. instead of
Qed. and run
Print mytheorem to see the proof object for
mytheorem. It can get big, but it's sometimes instructive to look at that for small proofs.)
I think it's instructive to look at how basic logical operators such as
exists are defined (
forall is a primitive concept). They're in the
Logic library. It might not all make sense at first read, so revisit it again after you've practiced a bit.
To say that “P is true” in Coq, you build a proof of X. To show that “(A and B) is true”, you build a proof of (A and B), and you do this by building a proof of A and a proof of B. Likewise, to show that “(A or B) is true”, you build a proof of (A or B) by either building a proof of A or a proof of B (your choice, and if the proof depends on some variable, then you can pick a different side to prove depending on the value of that variable). This illustrates the relationship between constructivity and intuitionistic logic: the only way to prove
A \/ B (syntactic sugar for
or A B) is to either prove
A or prove
B, and this goes even when
not A. If you can't manage to prove
A and you can't manage to prove
not A either, then you can't prove
A \/ not A. The law of excluded middle does not hold. (It can be added as an axiom, but at a cost — you lose some of the advantage of constructivity.)
I don't think your definitions of
Knave are particularly useful. You can prove
Knight p and
Knave p for any person
p. The point of defining things in
Prop is that they're not always true. Parametrized types in
Set are often non-empty for every value of the parameters, but parametrized types in
Prop are usually empty for some parameters — the parameters that make the proposition false.