The Coq mailing list

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

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

> thank you all for the replies!
> 
> what is the human explanation of the "anything" class (i naiively
> would expect it to be close to your lemma False_ind, may be wrong).
> 
> is any of these types empty or not (the wizard can't prove it any
> way):
> 
> Inductive AA : Prop := A0: BB->AA with BB : Prop := B0: AA->BB .

Without going so far, you can stop to:

Inductive AA' : Prop := A': AA' -> AA'.

This type is already empty.

Here is a closed proof term:

Fixpoint AA_is_empty' (aa: AA'): False (* term has type AA' -> False *)
:= match aa with
   | A' aa => AA_is_empty' aa
   end.

(You can prove this with tactics:

 Lemma AA_is_empty': AA' -> False.
 Proof.
  intros aa.
  induction aa.
  assumption.
 Qed.
)

For same reasons, AA and BB are empty:

Fixpoint AA_is_empty (aa: AA): False (* term has type AA -> False *)
:= match aa with
   | A0 bb => BB_is_empty bb
   end
with BB_is_empty (bb: BB): False (* term has type BB -> False *)
:= match bb with
   | B0 aa => AA_is_empty aa
   end.

(You can prove this with tactics:

 Lemma AA_is_empty: AA -> False
 with BB_is_empty: BB -> False
 Proof.
  intros [].
  apply BB_is_empty.
  assumption.
 Proof.
  intros [].
  apply AA_is_empty.
  assumption.
 Qed.
)

Remember that an inductive type is the smallest type stable by its
constructors.

Empty types are stable by these constructions
(for any empty object you can build an empty object using the
constructor).
But if you add a constructor with no parameters, then your type cannot
be empty as it requires to contain this constructor.
So in the case of AA', if you add the "AO: AA'" constructor, then your
type won't be empty (in fact your type will be isomorphic to "nat":
AO~O and A'~S)

Note also that Coq admits an other construction: coinductive types,
this time, the types are the largest one stable by constructors.
So that if you change

Inductive AA' : Prop := A': AA' -> AA'.

into

CoInductive AA' : Prop := A': AA' -> AA'.

Then AA' will become non-empty, and will contain only one element:

cofix aa_elt: AA' := AA' aa_elt

that is:

AA'
 (AA'
   (AA'
     (AA'
       ([I am too lazy to complete this part of the term]
       )
     )
   )
 )

But that is an other story (and you cannot do proof by induction with
coinductive types; you will have to do proof by coinduction which are
often trickier).

> 
> (suppose expressing disequation won't be possible).
> 
> 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