The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Fri, 20 May 2011 12:19:04 +0300,
Georgi Guninski 
<guninski AT guninski.com>
 a écrit :

> ...and is the "anything" type as good as False - if i rename your
> original False to FalseO and define "anything" to be False is Coq
> expected to work (possibly after modifying some proofs a bit) ?
> 

Not well defined question.
But if you can prove (and in this case you can) that "Himpl: anything
-> False", then you can replace any binder of type "False" by a binder
of type "anything" and replace every occurence of your binder by
"(Himpl [your binder])".

Typically, "forall f: False, P f" can be replaced by
 "forall a: anything, P (Himpl a)"

But "anything" and "False" are considered to be different type:
"forall a: anything, exists f: False, a = f" won't be accepted.
(but of course "forall a: anything, exists f: False, (Himpl a) = f"
 will be [and will be provable])

> On Thu, May 19, 2011 at 11:41:55AM -0400, Adam Chlipala wrote:
> > Georgi Guninski wrote:
> > >what is the formal definition of "empty"
> > 
> > A type [T] is empty if you can prove [T -> False].
> > 
> > >Lemma l1: anything.
> > >Proof.
> > >constructor 1.
> > >(* this passes without plug-ins *)
> > 
> > So would running [idtac].  The problem is that you haven't finished
> > the proof. :P