coq - 在 Coq 中证明“rev (rev l) = l”

Question

这是给我的练习之一，我在对 l 进行归纳后几乎立即卡住了。我不知道这里还有什么其他断言。

我不允许使用自动、直觉等高级策略。

Fixpoint snoc {A : Type} l a : list A :=

match l with

  | nil    => a :: nil

  | h :: t => h :: (snoc t a)

end.

Fixpoint rev {A : Type} l : list A :=

match l with

  | nil    => nil

  | h :: t => snoc (rev t) h

end.

(Prove the following)

Theorem rev_rev : forall A (l : list A),

rev (rev l) = l.

Answer 1

我们都是新手，刚开始时，在尝试掌握一门新学科时，寻求帮助以免失去勇气是很有用的。我会尽量给你一个提示，但不会泄露太多。

这比之前的练习更棘手的原因可能是因为这个证明涉及执行两个归纳推理步骤。您可能第一个做得很好，并获得了第二个目标，例如

  ...
  IHl : rev (rev l) = l
  ============================
   rev (snoc (rev l) a) = a :: l

不幸的是，你不能IHl立即使用你的归纳假设，因为论点的rev形式不正确。

所以，在这里你可以尝试证明另一个引理rev (snoc l a) = ...，这会将目标变成你可以重写的东西IHl。
如果你能弄清楚这一点，并在引理中证明这一点，那么你应该没问题。

Answer 2

我们不会为你做作业，你应该先用笔和纸证明它，就像@gallais 说的那样。

提示：您可能需要稍微概括您的属性（使用中间引理）才能证明rev_rev. 你应该看看rev_append。