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

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是用于含义，而不是方程式。

Answer 2

在这种情况下，如果使用构造函数参数而不是索引来定义归纳类型，则rewrite将起作用：

Inductive foobar : Type :=
    | foob (n : nat).

由于这种类型只有一个构造函数，所以我的理解（from this answer）使用索引不会带来任何好处，但是会使Coq很难进行模式匹配。

通常，以下任何一种技术都可以达到目标rewrite的效果：

assert

assert (H: 3 + 4 = 4 + 3). { rewrite <- plus_comm. reflexivity. }

重写

(* introduce a new sub-goal where you can prove that the replacement is OK *)
replace (3 + 4) with (4 + 3).
(* annoyingly, Coq orders the new goal last. I think it's clearer to tackle it first *)
Focus 2.
(* do the rewrite *)
rewrite <- plus_comm. reflexivity.