The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/09/2016 09:13 AM, Matthieu Sozeau wrote:
> > 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.

Just submitted as #4721

> > Definition T1 : Type := S1.
> > Definition T2 : Type := S2.
> >
> > Goal T1 = T1.
> > congruence.
> > Undo.
> > tauto.
> > Undo.
> > unfold T1.
> > Fail congruence.
> > tauto.
> > Qed.
> 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.

This is #4718, submitted before I started to think that maybe I was just 
using universes incorrectly.

> Best,
>   -- Matthieu

Thanks, Matthieu.

-- Jonathan