对需要证明的列表进行归纳的另一种方法
对需要证明的列表进行归纳的另一种方法
提问于 2013-09-12 08:43:08
我定义了一个列表的归纳定义(称为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的情况。在我的特殊定理中，这些情况更适合并使证明更简单。)
然而，为了能够在我的证明中使用列表，我必须证明
Lemma all_lists_are_listkind: (forall {X} (l:list X), listkind l).在尝试了各种方法之后，我发现自己被困在了这一点上。我非常希望看到如何执行这样的证明，最好是最小的coq魔术应用。
回答 1
Stack Overflow用户
回答已采纳
发布于 2013-09-12 09:35:17
以下是一个解决方案：
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。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/18759490
复制相关文章
相似问题
腾讯云开发者
