In Coq, what does it mean to have an inductive type where the right-hand side of ":" is Prop?

I'm new to Coq, and my (rather limited) understanding is that inductive types are like algebraic datatypes in Haskell, so there is a constructor data T = A a with some arguments, and the result A a is a T: specifically a T, so I understand stuff like this:

Inductive List := Nil : List | Cons : nat -> List -> List.

where you apply a constructor and get a List, which defines what Lists (as opposed to something else) are.

So how exactly does it work that I can define an inductive type like this:

Inductive Person := Name : nat -> Person.
Inductive Knight : Person -> Prop := Knight_ : ∀(A:Person), Knight A.
Inductive Knave : Person -> Prop := Knave_ : ∀A, Knave A.

where the inductive type has Prop (or Person -> Prop?) on the right-hand side of it? This is supposed to represent "A is a knight" and "A is a knave" in knights-and-knaves puzzles. I think this is a way to encode the idea, but this is a little confusing, and I couldn't find an explanation of this. Some places in fact introduce inductive types as being similar to Haskell's data, but that's clearly not all of it.

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 A and 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 A and B in Prop, and construct a type in Prop.

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 A and 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 A and 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 and, or, not and 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 B is 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 Knight and 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.

StackExchange Computer Science Q#81657, answer score: 9