The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Adam Chlipala wrote:
> Damien Andrew Tamburri wrote:
> >     I am having difficulty in including the context for rules in 
> > Natural Deduction, within a structure representing Natural Deduction 
> > Trees themselves (see attached file).. I keep getting the "The term 
> > "In a X" has type "Prop" which is not a (co-)inductive type." error 
> > for the last three constructors of type NDTree.. can anyone explain 
> > me if and how I can use the construct "if..then..else" in this way? 
> > what other context alternatives are there?
>
> Like the error message suggests, [if..then..else] is for analyzing
> values of inductive types that have two constructors (e.g., [bool]).  It
> doesn't make sense that you'd be able to use the same construct to
> analyze a [Prop], since [if..then..else] is very computational, and
> truth of [Prop]s is undecidable in general.
>
> Try to find a way to express what you want using implication instead.
> You don't have many other options available within an inductive type
> definition, because of the positivity criterion.

This confusion between Prop and bool is a common pitfall of the "Type 
theory approach".  In Coq, types are used to represent logical 
formulas.  Conversely, logical formulas usually are represented as types 
(of type Prop), not data inside types.  In other words, Prop is a type 
whose elements are themselves types.  It would not come to your mind to 
write

if nat then ... else ...

of

if bool then ... else ...

would it? 

A boolean value, true or false, is data, inside the type bool.  if ... 
then ... else ... is used to observe data.

Types can practically never be used as data.  On the other hand, boolean 
values can often be viewed as logical formulas,  the boolean value b is 
easily understood as meaning the logical formula "b = true".

Now, if A and B are logical formula  (A -> B) means something: A implies B
 if A and B are types (A -> B) means "the type of function from A to 
B",  the representation of formulas as types works in the following way: 
if you can show there is an element in the type C, then we say that C 
holds (or is provable, or is true, ...).  If you have an element in A -> 
B, it is a function, let's call it f, now if you have an element in A, 
let's call it a, then f a is an element in B.  Thus, if both A -> B and 
A hold, B also holds.  So it looks like the type A -> B (functions from 
A to B) has some good properties expected for the formula A -> B (A 
implies B).

This example gives a hint as to why types can be used to represent 
logical formulas and type verification can be used to check that proofs 
are well-formed.  It is the foundation of the Coq system, but in this 
application, you loose the direct correspondence between boolean values 
and logical formulas.

I hope this helps,

Yves