Ssreflect Users Discussion List

[Enrico Tassi <>]

On Sat, Apr 19, 2014 at 12:17:43PM +0200, Ralf Jung wrote:
> Hi all,
> 
> when I use rewrite to instantiate an existential, I often see failures
> of the proof after completing all subgoals, when running "Qed.".
> 
> For example, when I have a situation like this
> 
>   a: nat
>   H: S a = 42
>   ============
>   S ?56 = 42
> 
> I use "rewrite H" to then solve the goal with reflexivity (or "by
> rewrite H"). This seems to instantiate the existential, but something
> goes wrong:

This time I don't have time for a long reply.

The "bug" in ssr is that rewriting with H left to right should fail.
For ssr, ?56 is a fresh constant, different from a.  Since ssr builds
on the coq proof engine, that is quite a moving target, some check must
have become ineffective.

If you need to instantiate ?56, you should call standard Coq rewrite
tactic with

  rewrite -> H.

but you lose all the bells and whistles that ssr rewrite has.

I will check which assertion is not working anymore in ssr, but ssr 1.4
and ssr 1.5 tactics are not supposed to instantiate evars.  I should add
some tests in that direction...

When ssr was originally written coq was really bad at handling evars,
hence the safe choice of considering them as constants.

Cheers
-- 
Enrico Tassi