证明用地图构造的列表的相等性

Question

我有两个列表，一个列表直接通过递归构造，另一个列表使用map操作构造。我试图证明它们是平等的，令人惊讶的是我被卡住了。

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint ls_zeroes n :=
  match n with
  | 0 => nil
  | S n' => 0 :: ls_zeroes n'
  end.

Fixpoint ls_ones n := map S (ls_zeroes n).
Fixpoint ls_ones' n :=
  match n with
  | 0 => nil
  | S n' => 1 :: ls_ones' n'
  end.

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl. f_equal. (* ??? *)
Abort.

这是上下文的外观：

1 subgoal
n : nat
IHn : ls_ones n = ls_ones' n
______________________________________(1/1)
map S (ls_zeroes n) = ls_ones' n

我以为fold ls_ones会将map S (ls_zeroes n)转换为ls_ones n，因为这实际上是ls_ones的定义，但它什么也没做。如果我尝试unfold ls_ones in IHn，则会得到一个讨厌的递归表达式，而不是ls_ones的逐字定义。

最完整的证明方法是什么？

Answer 1

我以为fold ls_ones会将map S (ls_zeroes n)转换为ls_ones n，因为这实际上是ls_ones的定义

是吗？您说的是Fixpoint ls_ones，而不是Definition。像任何Fixpoint一样，这意味着将给定的ls_ones定义转换为fix。给出的定义中没有递归结构，因此这毫无意义，但是您说过做到了，所以Coq做到了。发出Print ls_ones.以查看实际定义。真正的解决方案是将ls_ones设置为Definition。

如果您不解决此问题，则仅当递归参数以构造函数开头时，Coq才会减少Fixpoint。然后，为了完成该证明，您需要destruct n显示这些构造函数：

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  - reflexivity.
  - simpl. f_equal. destruct n; assumption.
Qed.

Answer 2

注意，当您定义ls_one并展开定义时，您会得到：

(fix ls_ones (n0 : nat) : list nat := map S (ls_zeroes n0)) n = ls_ones' n

问题是ls_one不是固定点。确实，它不会递归。一旦coq自动定义了点{struct n0}（在这种情况下，第n个参数），您的证明就被卡住了，因为n从未在P k-> P（k + 1）中被破坏，因为k没有被破坏。使用：

Definition ls_ones n := map S (ls_zeroes n). 

证明变得无关紧要：

Goal forall n, ls_ones n = ls_ones' n.
Proof.
  intros.
  induction n.
  trivial.
  unfold ls_ones in *.
  simpl.
  rewrite IHn.
  trivial.
Qed.