The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Tue, 04 Jun 2013 23:26:22 +0200,
Robbert Krebbers 
<mailinglists AT robbertkrebbers.nl>
 a écrit :

> 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.

Yes, I am pretty sure I did the mistake to write "rewrite K" instead of
"rewrite <- K". I always know what I do when I use it, so I always
orient my equalities to what seems to me the best way to have the luck
to use this trick.

Also you may find "rewrite" more natural than "rewrite <-", but in a
way, "rewrite <-" is more efficient than "rewrite". "rewrite" calls
"eq_ind_r" (which in turns calls "eq_ind"), while "rewrite <-" directly
calls "eq_ind". I know that it is not relevant, as there is no intended
computation behind.

Also, I find that "intros []" gives more readable proof terms (I said
proof terms, not proof scripts) than what "rewrite …" does. Of course,
almost no one cares about it (and they are not wrong in doing so,
unless they want to understand the language behind the tactics).

> 
> * 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 problems with people using "inversion_clear" (and the reason why
almost nobody does, and redefine it as "inversion H; clear H; subst.").
I do not use "inversion" nor "inversion_clear" as it gives way too big
proof terms (and not easy to read). I hope someone will rewrite it
someday to make a better version.

Once again, I know what I do when I do this and take care that.

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