0

我已经定义了列表的归纳定义（称为listkind），以便我可以通过归纳listkind而不是列表来轻松证明特定定理。

Inductive listkind {X}: list X -> Prop :=
| l_nil : listkind []
| l_one : forall a:X, listkind [a]
| l_app : forall l, listkind l -> forall a b, listkind ([a]++l++[b]).

（有了这个性质，为了证明关于列表的事情，我必须证明列表是 []、[a] 或 [a]++l++[b] 的情况，而不是列表是 [] 或a::l。在我的特定定理中，这些情况更适合，并使证明更简单。）

但是，为了能够在我的证明中使用 listkind，我必须证明

Lemma all_lists_are_listkind: (forall {X} (l:list X), listkind l).

尝试了各种方法后，我发现自己卡在了这一点上。我非常感谢看到如何执行这样的证明，最好使用最少的 coq 魔法。

4

1 回答 1

2

这是一个解决方案：

Require Import List Omega.

Lemma all_lists_are_listkind_size: forall {X}  (n:nat) (l:list X), length l <= n -> listkind l.
Proof.
intros X.
induction n as [ | n hi]; simpl in *; intros l hl.
- destruct l as [ | hd tl]; simpl in *.
  + now constructor.
  + now inversion hl.
- destruct l as [ | hd tl]; simpl in *.
  + now constructor.
  + induction tl using rev_ind.
    * now constructor.
    * constructor.
      apply hi.
      rewrite app_length in hl; simpl in hl.
      omega. (* a bit overkill but it does the arithmetic job *)
Qed.

Lemma all_lists_are_listkind: forall {X} (l:list X), listkind l.
Proof.
intros.
apply all_lists_are_listkind_size with (length l).
apply le_refl.
Qed.

主要思想是您的列表与常规列表具有相同的大小，并且自然的归纳比非平凡列表形状的归纳更顺利。

希望对你有帮助，V。

于 2013-09-12T09:35:17.200 回答