Skip to Content.
Sympa Menu

ssreflect - Re: rewrite and instantiation of existentials: Qed fails

Subject: Ssreflect Users Discussion List

List archive

Re: rewrite and instantiation of existentials: Qed fails


Chronological Thread 
  • From: Ralf Jung <>
  • To:
  • Subject: Re: rewrite and instantiation of existentials: Qed fails
  • Date: Sat, 19 Apr 2014 14:24:01 +0200

Hi,

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

Unfortunately that does not work, the Coq rewrite does not instantiate
existentials either. That's why I was happy about ssreflect (seemingly)
doing that, but now I see that was just a bug. Well, fair enough :-)

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

I see, so I will just (continue to) explicitly instantiate them. Thanks.

Kind regards
Ralf



Archive powered by MHonArc 2.6.18.

Top of Page