The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 05/09/2016 12:09 PM, Jason Gross wrote:
> The rewrite tactic fails with this error message when it finds a subterm
> and instantiates the lemma, but refining with the lemma does not change the
> goal; I suspect it plays a role in determining which places to rewrite in.

Sorry - I should have realized that it was rewrite doing the 
complaining.  I guess I'm getting edgy about this universe thing.

-- Jonathan

> On Mon, May 9, 2016, 12:00 PM Jonathan Leivent 
> <jonikelee AT gmail.com>
>  wrote:
>
> > I attempted to write a tactic that would lower the universe level of an
> > equality conclusion, so as to avoid these problems - but it has a
> > problem of its own:
> >
> > Variable S1 S2 : Set.
> >
> > Ltac lowereq :=
> > lazymatch goal with
> > (*replace any equality by a min-universe-leveled one*)
> > |- @eq _ ?X ?Y => assert (X = Y) as H; [|rewrite H; reflexivity]
> > end.
> >
> > Goal @eq Type S1 S1.
> > Fail lowereq. (*Error: Tactic generated a subgoal identical to the
> > original goal*)
> > Admitted.
> >
> > Goal @eq Type S1 S2.
> > lowereq. (*works properly*)
> > lowereq. (*no complaints about identical subgoals here*)
> > Admitted.
> >
> > Why does Coq complain about a subgoal being identical to the original in
> > the first Goal case?  It doesn't do that elsewhere (as the second Goal
> > shows).  What is it trying to prevent?  Isn't that a job for the
> > progress tactical?
> >
> > -- Jonathan