The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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

  I would guess the recommanded intro-pattern here, is the rewriting pattern: intros ? ->.

* 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 [].

Works for that too. But since we need backward rewriting this time: intros x H1 <-


Arnaud