如何在当前目标的子表达式上使用重写

Question

在coq中,是否有可能将引理或假设应用于当前目标的子表达式？例如,我想应用plus是可交换的事实,以便在此示例中交换3和4.

Require Import Coq.Arith.Plus.

Inductive foobar : nat -> Prop :=
 | foob : forall n:nat, foobar n.

Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)

得到:

Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".

我怎样才能告诉coq在这个目标中究竟应用plus_comm？

Answer 1

使用策略simpl有效，但不要问我为什么rewrite plus_comm或rewrite (plus_comm 3 4)无效。apply是为了含义，而不是方程。