Search code examples
coqcoq-tactic

erewrite that asks for hypothesis first?

I want a variant of erewrite which asks for the hypothesis first, and then proceeds to the rewritten goal, rather than the other way round. Here is a small example:

Variable P : Prop.
Variable SomeProp: Prop -> Prop.

Lemma rewriter: forall (R: Prop), SomeProp R -> P = R.
Admitted.

Lemma useRewriter: P.
Proof.
  intros.
  erewrite rewriter.
  (* Current goal state, ?R *)
  (* I want SomeProp ?R first, not ?R *)
Abort.

I think SSR has some tactic like this, but I'm not able to find the correct one.

Solution

  • This is on the bug tracker as Premises of rewrite appear in different order.

    • The order was fixed in the SSR rewrite, and appears in the order that I ask for.
    • The default rewrite (when not using setoid equality?) shows premises in the "wrong" order.