关于 Coq 列表的推理

Question

我正在尝试根据 Pierce 的 "Software Foundations" 来解决一些定理。

首先我创建了几个有用的函数：

Inductive natlist: Type :=
  | nil: natlist
  | cons : nat -> natlist -> natlist.

Notation "x :: l" := (cons x l) (at level 60, right associativity).

Fixpoint repeat (n count: nat): natlist :=
    match count with
      | O => nil
      | S count' => n :: (repeat n count')
    end.

  Fixpoint length (l: natlist): nat :=
    match l with
      | nil => O
      | h :: t => S (length t)
    end.

 Theorem count_repeat: forall n: nat, length (repeat n n) = n.
  Proof.
    intros n. induction n as [| n'].
    simpl. reflexivity.
    simpl. (* and here I can't continue... *)

我想听从皮尔斯的建议：

Note that, since this problem is somewhat open-ended, it's possible that you may come up with a theorem which is true, but whose proof requires techniques you haven't learned yet. Feel free to ask for help if you get stuck!

那么，你能给我一些证明技巧吗？

Answer 1

正如@eponier 所说，你应该尝试证明一个更一般的引理，比如

Theorem count_repeat_gen: forall m n: nat, length (repeat n m) = m.

使用 repeat n n 在元素的值和列表的大小之间创建一个隐含的 link，这使得您的陈述无法直接证明。一旦你证明了 count_repeat_gen，你就能证明你的定理。

关于 Coq 列表的推理

Reasoning about lists in Coq

coq