Difference between propositionals True/False and booleans true/false in Coq

Question

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:

What is the purpose of creating the booleans true and false from the propositional True and False, instead of merging them into one primitive construct?
If the 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?

This question might be useful: https://stackoverflow.com/q/31554453/1633770. It motivates the differences between bool and Prop. — Arthur Azevedo De Amorim, Feb 04 '21 at 13:50

score 1 · Accepted Answer · answered Feb 04 '21 at 09:37

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.

Difference between propositionals True/False and booleans true/false in Coq

1 Answers1