The Coq mailing list

[Gilles Kahn <Gilles.Kahn AT inria.fr>]

Chet, (29 Nov 1993) says:

>So, I guess I'd say that it doesn't seem to be a good idea (from a
>mechanized reasoning point of view) to use inductive types for such
>"logical" purposes.

I understand the argument as saying: don't introduce a wealth of
inductive definitions just because our proof engine has certain 
characteristics now, because we will improve it.


Well, I am not yet convinced. As an example, the Prelude.v file
says beautifully:

Inductive Definition False : Prop = .

then goes on with the definition:

Definition not [A:Prop]A->False.

Why is this definition preferred to:

Inductive Definition Not [A: Prop]: Prop =
      Not_intro: (A -> False) -> (Not A).
Hint Not_intro.

which is much more conventional (there is an intro and an elim).

As an aside, the fact that "not" has a definition by rewrite has introduced a 
very unpleasant irregularity in the implementation of the Proof-by-pointing 
algorithm for Coq.


Gilles (with Yves' help, as usual)