The definition for the booleans true
/false
and their link with the propositional types True
/False
is described in Coq.Bool.Bool :
Inductive bool : Set := true : bool | false : bool
Definition Is_true (b:bool) :=
match b with
| true => True
| false => False
end.
When it comes to the bool
type, I more or less understand their purpose and function, but that is not the case for the Prop
types. This question gives a good example of my confusion. As presented there, the following is not a valid definition:
Definition inv (a: Prop): Prop := match a with | False => True | True => False end.
Resulting in "Pattern "True" is redundant in this clause.
". The same definition with bool
types on the other hand, compiles fine:
Definition inv (a: bool): bool :=
match a with
| false => true
| true => false
end.
Ptival's answer explains well why this happens in the pattern-matching sense: "False
is not a data constructor [...]". Indeed, that is clear by examining True
and False
:
Print True.
Print False.
Inductive True : Prop := I : True
Inductive False : Prop :=
In that case however, my question becomes: why? If they are not the same as true
/false
, then what are they? Specifically:
true
and false
from the propositional True
and False
, instead of merging them into one primitive construct?Prop
versions True
/False
don't mean the same as the bool
versions true
/false
, then what do they actually mean and what are the they supposed to represent in contrast with their boolean variants?Let me answer the different questions that you have. To begin with, in the pattern-matching
Definition inv (a: Prop): Prop :=
match a with
| False => True
| True => False
end.
Coq tells you it's redundant because it interprets False
and True
as variables that will be bound. Indeed True
and False
can't be matched against so it assumes you mean to name your variable True
or False
.
This code is equivalent to
Definition inv (a: Prop): Prop :=
match a with
| x => True
| y => False
end.
Then you can see why y
would be redundant: you are saying match any value to True
and any value to False
.
The greatest confusion you have I think is thinking that True
and False
should somehow mean the same as true
and false
. The short answer is: there is no relation at all, except in the name.
Actually True
and False
are closer to bool
than they are to true
and false
: they are (data) types.
True
is the type containing only one element, and False
is the empty type, with no inhabitant.
Inductive True : Prop :=
| I : True.
Inductive False : Prop :=.
(Admittedly, the definition of False
can be a bit weird, but it really says that it's a type which has no constructor.)
By contrast, bool
is a type with two elements: true
and false
.
So you can have h : True
which is a proof of True
but not x : true
because true
is not a type, its rather a piece of data.
Data can be observed (pattern-matching) but not data types.
I really want to insist that true
and false
are not variants of True
and False
. true
and false
are just bits and don't really have any meaning besides how you use them. True
and False
on the other hand have very precise meaning. True
is the trivial proposition that is always provable, and False
is the proposition that is never provable, having h : False
expresses a contradiction.
The elimination principle of False
shows how you can use it:
False_rect : ∀ P : Type, False → P
It says that you can derive anything from a proof of False
.