The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

On Mon, Apr 23, 2012 at 01:41:40PM +0200, Alan Schmitt wrote:
> On 21 avr. 2012, at 21:11, 
> wesongathedeveloper AT yahoo.com
>  wrote:
> 
> > Hello,
> > 
> > I have a question about the following proof state:
> > 
> > 
> > v_neq : v = v0 -> False
> > ______________________________________(1/51)
> > v = v0
> 
> There is something very wrong with this: you are trying to show that v is 
> equal to v0 assuming they are not.
> 
> Alan
I think Saint is trying to obtain a contradiction from the fact that he can 
prove v = v0 from v = v0 -> False. If the Logic were Classical this would 
indeed be possible. However a logic that deals with constructed proofs is 
Intuitinistic and so this can't, in general, be done.

Bernard.