The Coq mailing list

[Ilya Sergey <ilya.sergey AT imdea.org>]

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