In Coq, what does it mean to have an inductive type where the right-hand side of “:” is Prop?
-
04-11-2019 - |
Question
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.
No correct solution