Другой способ сделать индукцию по спискам, которые нуждаются в доказательстве

Question

Я определил индуктивное определение списков (так называемый 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]). 

(С этим свойством, чтобы доказать, что о списках, я должен доказать случаи, когда список является [], [а] или [а] ++ л ++ [б], а не дела где список [] или :: л. в моей конкретной теореме, эти случаи лучше подходят и делают доказательство проще.)

Однако, чтобы иметь возможность использовать listkind в моем доказательстве, я должен доказать

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

Пробуя различные подходы, я обнаружил, что застрял в этой точке. Я был бы очень признателен за то, что я мог бы сделать это, желательно с минимальной магией заклинания.

Answer 1

Вот решение:

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. 

Основная идея состоит в том, что ваши списки имеют один и тот же размер, как и обычный список, и индукция на естественнее идет более гладко, чем индукция по нетривиальной форме списка.

Надеется, что это помогает, В.