关闭 nats 列表上的引理

Question

我坚持要证明以下公认的引理。请帮助我如何进行。

函数 sumoneseq 添加到 returns 'true' 的重复列表，顺序相反。给定 [true;false;true;true;false;true;true;true]，它returns [3;2;1]。函数 sumones 在 nat 列表中添加值。给定 [3;2;1]，它 returns 6.

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).


Fixpoint sumoneseq (lb: list bool) (ln: list nat) : list nat :=
 match lb, ln with
 | nil, 0::tl'' => tl''
 | nil, _ => ln
 | true::tl', nil => sumoneseq tl' (1::nil)
 | true::tl', h::tl'' => sumoneseq tl' (S h::tl'')
 | false::tl', 0::tl'' => sumoneseq tl' ln
 | false::tl', _ => sumoneseq tl' (0::ln)
 end.

Fixpoint sumones (ln: list nat) : nat :=
 match ln with
 | nil => 0
 | r::tl => r + (sumones tl)
 end. 

Lemma sumones_l: forall lb ln,  
 sumones (sumoneseq lb ln) = sumones ln + sumones (sumoneseq lb []).
Proof.
 induction ln.
 + simpl. auto.
 + simpl.  
 Admitted.

Answer 1

两件事：

当使用直接归纳证明某个函数 f 的属性时，选择 f 在其上结构递归的参数。因此，在涉及 sumoneseq 的示例中，归纳 lb 而不是 ln，因为 sumoneseq 在 lb.
证明某个函数 f 的属性其中一个或多个参数固定为特定值（例如 sumoneseq 其第二个参数为 []）通过直接归纳几乎肯定会失败，因为该参数的值在 f 的递归调用之间变化，这意味着您将无法在您的归纳案例中应用归纳假设。在这种情况下，您需要通过找到 f 成立的更一般的属性来手动概括归纳假设，其中每个参数都足够一般。例如，不是通过归纳法直接证明 forall lb ln, sumones (sumoneseq lb ln) = sumones ln + sumones (sumoneseq lb [])，而是尝试将其概括为类似 forall lb ln ln', sumones (sumoneseq lb (ln ++ ln')) = sumones ln + sumones (sumoneseq lb ln') 的东西，并通过直接归纳法证明 that。然后，您想要的结果将作为该更一般结果的必然结果。

您可以在 James Wilcox's blog post 中了解更多关于概括归纳假设的信息，其中慷慨地包含了 8 个难度递增的练习。

现在试着用这两点来证明你的引理。 提示：当通过直接归纳法证明关于 sumoneseq 的更一般性陈述时，您可能还会发现在 sumones 的某个属性上提取出合适的引理会有所帮助。

如果您再次尝试无果，则在水平线下方提供了完整的解决方案（剧透警告！）。

这里是完整的解决方案。正如您可能看到的那样，在主要归纳之上需要大量案例分析（可能是由于您在 sumoneseq 中从 ln 中丢弃 0 的优化）和推理其中许多案例实际上非常相似和重复。我可能可以通过一些 Ltac 编程来进一步缩短证明脚本，在各种情况下寻找类似的模式，但我没有费心这样做，因为我直接把它搞砸了。

From Coq Require Import List Lia.
Import ListNotations.

Fixpoint sumoneseq (lb: list bool) (ln: list nat)
  : list nat :=
  match lb, ln with
  | nil, 0::tl'' => tl''
  | nil, _ => ln
  | true::tl', nil => sumoneseq tl' (1::nil)
  | true::tl', h::tl'' => sumoneseq tl' (S h::tl'')
  | false::tl', 0::tl'' => sumoneseq tl' ln
  | false::tl', _ => sumoneseq tl' (0::ln)
  end.

Fixpoint sumones (ln: list nat) : nat :=
  match ln with
  | nil => 0
  | r::tl => r + (sumones tl)
  end.

Lemma sumones_app_plus_distr : forall l l',
  sumones (l ++ l') = sumones l + sumones l'.
Proof.
  induction l; simpl; intros; auto.
  rewrite IHl; lia.
Qed.

Lemma sumones_l' : forall lb ln ln',
  sumones (sumoneseq lb (ln ++ ln')) =
  sumones ln + sumones (sumoneseq lb ln').
Proof.
  induction lb; simpl; intros.
  - destruct ln, ln'; simpl; auto.
    + destruct n; rewrite app_nil_r; simpl; auto.
    + destruct n, n0; simpl; rewrite sumones_app_plus_distr;
        simpl; lia.
  - destruct a, ln, ln'; simpl; auto.
    + replace (S n :: ln ++ []) with ((S n :: ln) ++ [])
        by reflexivity.
      replace [1] with ([1] ++ []) by now rewrite app_nil_r.
      repeat rewrite IHlb; simpl; lia.
    + replace (S n :: ln ++ n0 :: ln')
        with ((S n :: ln ++ [n0]) ++ ln')
        by (simpl; now rewrite <- app_assoc).
      replace (S n0 :: ln') with ([S n0] ++ ln')
        by reflexivity.
      repeat rewrite IHlb.
      replace (S n :: ln ++ [n0])
        with ((S n :: ln) ++ [n0])
        by reflexivity.
      repeat rewrite sumones_app_plus_distr; simpl; lia.
    + destruct n.
      * replace (0 :: ln ++ []) with ((0 :: ln) ++ [])
          by reflexivity.
        replace [0] with ([0] ++ [])
          by now rewrite app_nil_r.
        repeat rewrite IHlb; simpl; lia.
      * replace (0 :: S n :: ln ++ [])
          with ((0 :: S n :: ln) ++ []) by reflexivity.
        replace [0] with ([0] ++ [])
          by now rewrite app_nil_r.
        repeat rewrite IHlb; simpl; lia.
    + destruct n, n0.
      * replace (0 :: ln ++ 0 :: ln')
          with ((0 :: ln ++ [0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: ln') with ([0] ++ ln') by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
      * replace (0 :: ln ++ S n0 :: ln')
          with ((0 :: ln ++ [S n0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: S n0 :: ln') with ([0; S n0] ++ ln')
          by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
      * replace (0 :: S n :: ln ++ 0 :: ln')
          with ((0 :: S n :: ln ++ [0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: ln') with ([0] ++ ln')
          by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
      * replace (0 :: S n :: ln ++ S n0 :: ln')
          with ((0 :: S n :: ln ++ [S n0]) ++ ln')
          by (simpl; now rewrite <- app_assoc).
        replace (0 :: S n0 :: ln') with ([0; S n0] ++ ln')
          by reflexivity.
        repeat rewrite IHlb.
        repeat (repeat rewrite sumones_app_plus_distr;
          simpl); lia.
Qed.

Lemma sumones_l: forall lb ln,
  sumones (sumoneseq lb ln) =
  sumones ln + sumones (sumoneseq lb []).
Proof.
  intros; replace (sumoneseq lb ln)
    with (sumoneseq lb (ln ++ []))
    by (now rewrite app_nil_r); apply sumones_l'.
Qed.

关闭 nats 列表上的引理

Closing a lemma on list of nats

list

proof

nat

coq

induction