在需要证明的列表上进行归纳的另一种方法 [英] A different way to do induction on lists that needs a proof

问题描述

为了方便起见，我已经定义了列表的归纳定义(称为listkind) 让我通过在listkind而不是列表上的归纳法证明一个特定的定理.

I have defined an inductive definition of lists (called listkind) in order make it easy for me to prove a specific theorem by induction on listkind rather than on list.

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.在我的特定定理中，这些情况更合适，并且使证明更简单.)

(With this property, to prove things about lists, I have to prove the cases where a list is [], [a], or [a]++l++[b], rather than the cases where a list is [] or a::l. In my particular theorem, those cases fit better and makes the proof simpler.)

但是，要能够在证明中使用listkind，我必须证明

However, to be able to use listkind in my proof, I have to prove

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

尝试了各种方法之后，我发现自己陷于这一点. 看到如何执行这样的证明，我将不胜感激， 最好使用最少的coq魔术.

Having tried various approaches, I find myself stuck at this point. I would very much appreciate seeing how to perform such a proof, preferably with minimal coq magic applied.

推荐答案

以下是解决方案:

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.

主要思想是列表的大小与常规列表相同，自然归纳比非平凡形状的归纳更加顺畅.

The main idea is that your lists have the same size as regular list, and induction on a natural is goes more smoothly than induction on a non trivial shape of list.

希望有帮助， V.

这篇关于在需要证明的列表上进行归纳的另一种方法的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！