The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Saturday 29 September 2007 05:36:10 Stefan O'Rear wrote:
> On Sat, Sep 29, 2007 at 12:26:06AM -0400, Ethan Aubin wrote:
> > Hi,  This might be an obvious question, but is 'forall (A:Set)(x y:A),
> > (x=y)=(y=x)' provable in Coq? - EA
>
> Equality is a very slippery subject in Coq and other systems based on
> intuitionistic type theories.  Your statement is certainly true if you
> replace the outer = with <-> (split; auto).  In general, it's a bad idea
> to use = on anything other than values of inductive types.
>
> Stefan

Hi,

I ran across a similar situation recently. A tactic I was reading about tries 
to change the goal so that a subterm is equal to a Prop assumption called p. 
It then replaces p with True. In other words, it tries to use the following 
theorem:

forall (p:Prop), p->p=True.

In Coq, none of the automated tactics do anything if you try to prove this 
theorem and I really can't see any useful steps forward. I assume it isn't 
true but I can't explain why. If it isn't true, does anyone have a good 
explanation as to why it isn't true in Coq but it is in other logics?

Regards,

Sean