coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] The Altenkirch birthday paradox

From: Jesper Louis Andersen <jesper.louis.andersen AT gmail.com>
To: Andreas Abel <andreas.abel AT ifi.lmu.de>
Cc: Andrej Bauer <andrej.bauer AT andrej.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] The Altenkirch birthday paradox
Date: Wed, 21 Sep 2011 19:34:04 +0200

On Wed, Sep 21, 2011 at 17:26, Andreas Abel
<andreas.abel AT ifi.lmu.de>
wrote:
> Envy:  My coq installation does not have the proof-theoretical power of
> yours...
>
> Or how did you define S?

That part is easy:

Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.

Even undergraduates know that!

What I wonder however is the extension of the "auto" tactic and CiC
that makes the proof assistant so powerful it can do this. "auto"
seems to be a new powerful variant of Adam Chlipala's "crush". In
fact, it is so powerful I will argue we should rename "auto" to
"crash".

--
J.

[Coq-Club] The Altenkirch birthday paradox, Andrej Bauer
- Re: [Coq-Club] The Altenkirch birthday paradox, Andreas Abel
  - Re: [Coq-Club] The Altenkirch birthday paradox, Jesper Louis Andersen