The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.

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