Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Universe polymorphism in 8.5b2 and rewriting

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Universe polymorphism in 8.5b2 and rewriting


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page