是否可以使用 'rewrite' 而不是 'apply' 重写 SF 书的战术章节中的 silly2 示例？

Question

Theorem silly2 : forall(n m o p : nat),
     n = m ->
     (forall (q r : nat), q = r -> [q;o] = [r;p]) ->
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  apply eq2.
  apply eq1.
Qed.

SF book 暗示可以使用重写来执行上述操作，但我只是不知道如何操作。知道如何做到这一点吗？

Answer 1

如果你正确填写 ?，你应该可以用 rewrite (eq2 ? ? ?) 来证明它。一定要搞清楚是怎么回事，才能提高对 Coq 的理解。

[提示：尝试 pose proof (eq2 o) 看看效果如何]

Answer 2

这里有 3 个不同的版本。在我意识到 rewrite 错误消息的含义后，在不同的上下文中看到 ejgallego 的回复之前，我自己想出了第一个。

Theorem silly2 : forall(n m o p : nat),
     n = m ->
     (forall (q r : nat), q = r -> [q;o] = [r;p]) ->
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  rewrite eq2 with (r := m).
  - reflexivity.
  - rewrite eq1. reflexivity.
Qed.

第二个似乎是根据 ejgallego 的建议用函数应用程序重写的。

Theorem silly2' : forall(n m o p : nat),
     n = m ->
     (forall (q r : nat), q = r -> [q;o] = [r;p]) ->
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  rewrite (eq2 n m).
  - reflexivity.
  - rewrite eq1. reflexivity.
Qed.

第三个使用pose proof，似乎是在假设上做函数应用，而没有像上面那样重写目标。

Theorem silly2'' : forall(n m o p : nat),
     n = m ->
     (forall (q r : nat), q = r -> [q;o] = [r;p]) ->
     [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  pose proof (eq2 n m).
  apply H.
  apply eq1.
Qed.

是否可以使用 'rewrite' 而不是 'apply' 重写 SF 书的战术章节中的 silly2 示例？

Is it possible to rewrite the silly2 example from the Tactics chapter of the SF book using 'rewrite' instead of 'apply'?

coq