coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ilya Sergey <ilya.sergey AT imdea.org>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Universe polymorphism in 8.5b2 and rewriting
- Date: Fri, 21 Aug 2015 13:28:53 +0000
Hello all.
I'm currently using Coq 8.5 beta 2 with Ssreflect 1.5, and it seems that universe-polymorphic definitions affect the way rewriting is implemented in Ssreflect.
In particular, the system doesn't seem to be able to figure out some arguments for the subterms, subject to rewritings. This breaks some of the existing proofs of statements about definitions that are now made universe-polymorphic.
Here is a small example, which is accepted by Coq/Ssr.
Definition foo {A : Type} (f : nat -> A) x := f x.
Variables (T : Type) (f g : nat -> T) (x : nat).
Hypothesis G : foo g x = foo f x.
Goal g x = f x.
Proof.
rewrite -/(foo g _).
by rewrite G.
Qed.
However, adding "Polymorphic" to the first definition makes the last rewrite of the proof break with the following error:
Error: The RHS of G
(foo f x)
does not match any subterm of the goal
Even making all the declared variables and hypotheses universe-polymorphic doesn't seem to solve the problem. Curiously, the very same goal is solved immediately by "apply G."
Any help here is appreciated. Thanks!
Cheers,
Ilya
- [Coq-Club] Universe polymorphism in 8.5b2 and rewriting, Ilya Sergey, 08/21/2015
- Re: [Coq-Club] Universe polymorphism in 8.5b2 and rewriting, Enrico Tassi, 08/24/2015
Archive powered by MHonArc 2.6.18.