COQ中的电感类型的证明

Question

我试图证明以下定理：

Theorem implistImpliesOdd :
  forall (n:nat) (l:list nat),  implist n l -> Nat.Odd(length l).

含义如下：

Inductive implist : nat -> list nat -> Prop :=
 | GSSingle    : forall (n:nat), implist n [n]
 | GSPairLeft  : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
 | GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).

在证明期间，我达到了以下最终目标：

n: nat
l: list nat
a, b: nat
H: implist n (a :: b :: l)
IHl: implist n l -> Nat.Odd (length l)
=======================================
Nat.Odd (length l)

但是似乎倒置无法完成工作...

我该如何证明定理？

感谢您的帮助 ！！

Answer 1

您只需在inmandist谓语上进行诱导即可。例如，

From Coq Require Import List PeanoNat.
Import ListNotations.

Inductive implist : nat -> list nat -> Prop :=
 | GSSingle    : forall (n:nat), implist n [n]
 | GSPairLeft  : forall (a b n:nat) (l:list nat), implist n l -> implist n ([a]++[b]++l)
 | GSPairRight : forall (a b n:nat) (l:list nat), implist n l -> implist n (l++[a]++[b]).

Theorem implistImpliesOdd :
  forall (n:nat) (l:list nat),  implist n l -> Nat.Odd (length l).
Proof.
intros n l H. rewrite <- Nat.odd_spec.
induction H as [n|a b n l _ IH|a b n l _ IH].
- reflexivity.
- simpl. now rewrite Nat.odd_succ_succ.
- rewrite app_length, app_length. simpl. rewrite Nat.add_comm. simpl.
  now rewrite Nat.odd_succ_succ.
Qed.

Answer 2

假设h：inmandist n（a :: b :: b :: l）不一定是从gspairleft开始的证明，它也可以由gspairright的实例，l = l = l'++ [c] ++ [d]，您的归纳假设将不适用。您可以在列表的长度上而不是在列表本身上解决问题来解决问题。