The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 06/04/2013 11:11 PM, AUGER Cédric wrote:
> I think lot of us will discourage you to use this feature. But I find
> it often convenient.
I would discourage this!

What happens here is that we just eliminate the equality, hence:

* it performs the substitution rhs->lhs, instead of the "expected" 
lhs->rhs. For example:

  Goal forall x, x = 1 -> x * x = 1.
  intros x [].

yields the unprovable goal "x * x = x". The ordinary "intros x ?; 
subst." gives "1 * 1 = 1" which is at least provable.

* it does not perform the substitution in earlier introduced hypotheses. 
For example:

  Goal forall x, 2 = x -> 1 = x -> x * x = 1.
  intros x H1 [].

gives "H1 : 2 = x" instead of "H1 : 2 = 1".

So, for people that do not fully understanding how elimination of 
equality works, this trick would be pretty confusing...

> Same for "False → P"
I have no problems using an intro pattern here.