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是为了暗示，而不是方程式。

Answer 2

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

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

由于这种类型只有一个构造函数，我的理解（来自这个答案）是使用索引不会提供任何好处，但会使 Coq 更难进行模式匹配。

一般来说，以下两种技术都可以达到针对性的效果rewrite：

断言

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).
(* Coq orders the new goal last. I think it's clearer to tackle it first *)
Focus 2.
(* do the rewrite *)
rewrite <- plus_comm. reflexivity.