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

Question

在 coq 中，是否有可能将引理或假设应用于当前目标的子表达式？例如，我想应用加号是可交换的这一事实，以便在此示例中交换 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是为了含义，而不是方程。