Subject: Ssreflect Users Discussion List
List archive
- 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
- rewrite and instantiation of existentials: Qed fails, Ralf Jung, 04/19/2014
- Re: rewrite and instantiation of existentials: Qed fails, Enrico Tassi, 04/19/2014
- Re: rewrite and instantiation of existentials: Qed fails, Ralf Jung, 04/19/2014
- Re: rewrite and instantiation of existentials: Qed fails, Enrico Tassi, 04/19/2014
Archive powered by MHonArc 2.6.18.