The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Jonathan,

On Mon, May 9, 2016 at 1:08 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 05/08/2016 05:23 PM, Jason Gross wrote:
> What error message do you get if you do [into H; pose (H : @peq@{Set}
> Type@{Set}
> T1 T2).]?  In particular, which universe variable is it refusing to
> minimize, and why?  (My approach to [Set] with universe polymorphism is
> mostly "don't use it".  Note that [@eq Type@{i} A B -> @eq Type@{j} A B]
> does not hold for [i > j], but you don't run into these other problems,
> which are generally a result of Coq refusing to minimize some universes to
> Set (allowing minimization in these cases has resulted in even more issues,
> sometimes in cases where [Set] was not explicitly mentioned, so Mathieu
> chose to forbid some minimizations).)

Note that I'm not using universes in the sense of having (prior to
trying to fix this problem) any definitions that use explicit universes
or polymorphism.  I just have some definitions that implicitly declare
args as Types (like A in definition foo{A}(a : A)...), and uses of those
definitions on Sets.

I'd rather not use universe polymorphism.  However, I thought I was
being dragged in its direction.  But, I'm not sure what's going on.
Here's an example:

Variables S1 S2 : Set.

Goal @eq Type S1 S2 -> @eq Type S1 S2.
intro H.
Fail tauto.
assumption.
Qed.

Why does tauto fail, when assumption succeeds?  Is this a bug in tauto?

That's a regression in tauto indeed, which now requires exact equality 

of the universes, through a non linear goal pattern matching:

match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible, with no additional universe constraints currently, but the two types are initially different. This can be fixed easily to allow the same flexibility as in 8.4 (or assumption) to unify the universes as well.

 

Or, is there an explanation having to do with universe levels that
absolves tauto of missing this easily proven case, but is consistent
with assumption succeeding?

Another example:

Definition T1 : Type := S1.
Definition T2 : Type := S2.

Goal T1 = T1.
congruence.
Undo.
tauto.
Undo.
unfold T1.
Fail congruence.
tauto.
Qed.

Here, tauto is well behaved, but congruence is not.  Since I am seeing
these strange behaviors through the lens of various unanticipated tactic
failures, I'm not sure whether I'm seeing some expected behavior on the
part of universes that I have to compensate for (how?), or if I'm
hitting tactic bugs.

This one is a bit more surprising: congruence does not work up to cumulativity Set <= Type(i) (already in 8.4). It builds a proof of [@eq Set S1 S1] by inferring the type of S1, but this proof can no longer apply to the [@eq Type S1 S1] goal, because Type cannot be unified with Set in general. It can also be fixed by allowing larger types in the proofs produced by congruence.

Best,

 -- Matthieu