coq - 先写假设？

Question

我想要一个变体，erewrite它首先要求假设，然后继续重写目标，而不是反过来。这是一个小例子：

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.

我认为 SSR 有这样的策略，但我找不到正确的策略。

Answer 1

这是在错误跟踪器上，因为重写的前提以不同的顺序出现。

• 该顺序在 SSR 重写中已修复，并按我要求的顺序显示。
• 默认重写（不使用 setoid 相等时？）以“错误”顺序显示前提。