The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Thanks everyone. I solved the proof.  The one tip below was useful.  If anyone is interested in seeing the solution, I can mail it out.  Unfortunately, it is difficult to extract from the rest of my framework and I don't feel like posting the entire framework at this time.

                                    - Ken

> Date: Tue, 16 Aug 2011 21:23:54 -0400
> From: adamc AT csail.mit.edu
> To: kendroe AT hotmail.com
> CC: coq-club AT inria.fr
> Subject: Re: [Coq-Club] A proof I'm having difficulty with
>
> Kenneth Roe wrote:
> > I have abstracted out the appropriate definitions from my model. I'm
> > trying to figure out a good approach for this proof. I'm pretty sure
> > that it requires classical logic. The key to the proof is to show
> > that "v < vars" in the theorem at the end. To do this, I'd like to
> > assume that v >= vars and then construct an m and m' that are counter
> > examples to the first hypothesis. How can I set this up? I've
> > included all the relevant definitions. Hopefully, some Coq guru can
> > solve this quickly.
>
> I haven't yet read any of the code you included below, but I thought it
> worth pointing out that proof by contradiction is valid for all
> decidable propositions (or at least those decidable within CIC), even in
> constructive logic. If your [v < vars] fact uses the usual natural
> number comparison, then you can prove a lemma for the contradiction
> rule. The decidable tests like [le_lt_dec] in the Coq standard library
> should let you prove this lemma without any induction.