0

这是我正在使用的 coq 版本：

sibi { ~ }-> coqc --version
The Coq Proof Assistant, version 8.4pl4 (November 2015)
compiled on Nov 04 2015 12:56:53 with OCaml 4.02.3

这是我要证明的定理：

Require Import Coq.Lists.List.
Import ListNotations.

Theorem rev_app_distr: forall l1 l2 : list nat,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.

请注意，我将在证明中使用这个定理（我已经证明了）：

Theorem app_nil_r : forall l : list nat,
  l ++ [] = l.

好的，现在这是我尝试通过通常的归纳方式证明定理：

Theorem rev_app_distr: forall l1 l2 : list nat,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros l1 l2.
  induction l1 as [| n l1'].
  - simpl.
    rewrite -> app_nil_r with (l := rev l2) at 2.

但是在执行该rewrite策略时，它给了我以下错误：

Error: Tactic failure:Nothing to rewrite.

但是如果我使用symmetry策略，我实际上可以通过相同的代码来证明它：

Theorem rev_app_distr: forall l1 l2 : list nat,
  rev (l1 ++ l2) = rev l2 ++ rev l1.
Proof.
  intros l1 l2.
  induction l1 as [| n l1'].
  - simpl.
    symmetry.
    rewrite -> app_nil_r with (l := rev l2) at 1.

那么，为什么在没有对称的情况下重写它是行不通的呢？

4

1 回答 1

1

问题不在于您错过了symmetry呼叫，而在于您at 2在调用该策略时添加了修饰符。app_nil_r由于此时的目标在(即)的左侧仅出现一次rev l2 ++ []，因此该rewrite策略会变得混乱并且不会执行任何操作。如果您替换at 2为at 1，或者只是删除它，问题就会消失。您可以在Coq 手册中了解有关at修饰符的更多信息。

于 2017-03-17T18:16:00.657 回答