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

cs.stackexchange https://cs.stackexchange.com/questions/81657

  •  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

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top