The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

This message is partially a reply to Aaron's post about axiomatizing 
nat, and partially a reply to Benjamin's post quoted below.

Benjamin Werner wrote:

> It is not so much the question of "which types" but rather what you  
> can do with them. Without inductive types, i.e. in raw CC, you :
>
> * cannot prove 0 \neq 1
>
> * cannot prove the induction scheme (or dependent matching for the  
> matter)
>
> * do not have constant-time reduction for the matching, and matching  
> only works for closed terms.
>
> You can get back some of the results in CC through mere axioms. But  
> not the reduction behavior.

I think I've below defined True, False, eq, and nat without using 
inductive definitions or axioms.  I'm able to prove 0 \neq 1, and the 
induction scheme follows trivially from my definition of nat.

Have I used inductive types without realizing it, or have I 
misunderstood what you meant by being able to prove 0 \neq 1?

-------

Definition True := forall (T : Type), T -> T.
Definition truei : True := fun (T : Type) (x : T) => x.

Definition False := forall (T : Type), T.

Definition eq (T : Type) (x y : T) :=
 forall (P : T -> Type), P x -> P y.
Definition refl_equal (T : Type) (x : T) : eq T x x :=
 fun (P : T -> Type) (pf : P x) => pf.

Definition nat :=
 forall (P : Type),
   P
   -> (P -> P)
   -> P.
Definition O : nat := fun (P : Type) (init : P) _ => init.
Definition S n : nat := fun (P : Type) (init : P) (step : P -> P) =>
 step (n P init step).

Theorem zero_neq_one : eq nat O (S O) -> False.
 intro.
 unfold eq in X.
 assert ((fun (n : nat) => n Type True (fun _ => False)) (S O)).
 apply X.
 unfold O.
 apply truei.
 trivial.
Qed.