The Coq mailing list

[gallais <guillaume.allais AT strath.ac.uk>]

Hi all,

I thought I'd throw in a couple of references:

Jean-François Monin talked at the 2nd Coq Workshop about these proofs
by diagonalization in "Proof Trick: small Inversions":
http://coq.inria.fr/coq-workshop/2010

Pierre Boutillier and Thomas Braibant have been working on an automation
of this process. Here's a blog post about it and the github repository
with the implementation:
http://gallium.inria.fr/blog/a-new-Coq-tactic-for-inversion/
https://github.com/braibant/invert
As far as I know, this is destined to be integrated as part of Coq's
official codebase in a future release.

Cheers,


On 10/10/13 22:17, t x wrote:
> Vincent, Robbert, Geoff: your examples are much more insightful.
>
> I particularly like Robbert's example. It has just the right amount of
> "generalizable to other cases" + "simple to understand."
>
> Thanks!
>
>
> On Thu, Oct 10, 2013 at 1:43 PM, Geoff Reedy 
> <geoff AT programmer-monk.net>wrote:
>
> > On Thu, Oct 10, 2013 at 01:16:53PM -0700, t x said
> > > Inductive Nat : Type :=
> > > | O: Nat
> > > | S: forall (n: Nat), Nat.
> > >
> > > Lemma lem:
> > >    O <> S O.
> > > [...]
> > > Is there a simpler proof of this?
> >
> > I think this is as short as it gets:
> >
> > eq_ind O (fun n => match n with O => True | S _ => False end) I (S O)