The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Wed, 11 May 2005, Roland Zumkeller wrote:

> Another question: Is there any damage apart from this? Would it be
> consistent?
>

I think so. If Term would be accepted, then we could use it in a Fixpoint
for proving False:
-----------------------------------------------------------------------
Inductive Term : Set :=
   Lambda : (Term -> Term) -> Term.

Definition anyTerm : Term := Lambda (fun t=>t).

Fixpoint toFalse (t:Term) : False := match t with
  | Lambda f => toFalse (f anyTerm)
 end.

Definition oouch : False := toFalse anyTerm.
----------------------------------------------------------------------
Of course, I cannot test my Fixpoint in Coq, but it ought to be valid. In
particular, the recursive call (f anyTerm) is indeed structurally smaller
than t, since f is structurally smaller than t.

In fact, I've tested a legal variant that works great. It's even a good
way to prove that the following inductive type is _not_ inhabited:
----------------------------------------------------------------------
Inductive Term : Set :=
   Lambda : (nat -> Term) -> Term.

Fixpoint toFalse (t:Term) : False := match t with
  | Lambda f => toFalse (f 0)
 end.
----------------------------------------------------------------------

Best,

Pierre