Ssreflect Users Discussion List

[Enrico Tassi <>]

From the ssreflect user manual:

  The rewrite tactic will not instantiate existing existential
  metavariables when matching a redex pattern.

Issue #30 on github:

  https://github.com/math-comp/math-comp/issues/30

made me realize that this invariant is today broken.  Eg.

  Axiom H : forall x, 3 + x = x.

  Goal exists y, y + 4 = y.
  eexists.
  rewrite H.

works, and instantiates ?y with 3.  I've a patch that makes this rewrite
step being rejected (or better, makes the flexible subterm "?y + 4" not
match the "3 + _" pattern).

Unfortunately such change may break your scripts, hence this message.

The behavior of rewrite w.r.t. the instantiation of evars in the goal
has been discussed at length both in the context of Coq and Ssreflect,
so I guess there is no argument against restoring the documented
behavior.

The check is O(n*log k) where n is the number of evars in the goal
and k is the number of open goals.  So I guess its cost is OK.

Best, 
-- 
Enrico Tassi