The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.