证明列表翻转函数的单射

新年第一更，本文讲述一个非常直观的性质：对于列表的翻转函数，它是单射的。我们将使用 Coq 来协助我们证明。这道问题的证明颇具启发意义，在这里撰文描述下证明的过程。我们也可以从证明本身探讨下一个成功的证明所应有的切入点。

定义

翻转列表函数rev的定义如下所示：

Fixpoint rev (l:natlist) : natlist := 
  match l with
   | nil    => nil
   | h :: t => rev t ++ [h]
  end.

定理rev_injective：

Theorem  rev_injective : forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.

一个切入点或许是数学归纳，不过证明过程中相对繁琐，而且会遇到证明不下去的情况。我尝试过一些手段，都没有什么效果。也就是说，局部的分析或许不太适合本问题；尝试重新审视定理的内容，我们发现，事实上应该用全局的视角去看待它。

假设rev l1 = rev l2是正确的，那么接下来证明是不是就简单多了呢？(Hint : rev (rev l) = l)

引理rev_involutive：

Theorem rev_involutive : forall l : natlist,
  rev (rev l) = l.

证明略。

证明

首先我们要假设前件成立：

Theorem  rev_injective : forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
Proof.
  intros l1 l2.
  intros H.

得到一个subgoal:

1 subgoal
l1 : natlist
l2 : natlist
H : rev l1 = rev l2
______________________________________(1/1)
l1 = l2

根据定理rev_involutive我们可以推倒出：l1 = rev (rev l2)。在根据假设 rev l1 = rev l2，可以得到 l1 = rev (rev l1)。再次应用定理 rev_involutive， l1 = l1， rev l1 = rev l2 -> l1 = l2 得证。

Theorem  rev_injective : forall (l1 l2 : natlist), rev l1 = rev l2 -> l1 = l2.
Proof.
  intros l1 l2.
  intros H.
  rewrite <- rev_involutive.
  rewrite <- H.
  rewrite -> rev_involutive.
  reflexivity.
Qed.

剩余过程：

______________________________________(1/1)
l1 = rev (rev l2)

______________________________________(1/1)
l1 = rev (rev l1)

______________________________________(1/1)
l1 = l1

no more subgoals

总结

形式化证明可以很灵活。