Coq 中归纳类型的证明

Question

我尝试证明以下定理：

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

其中 implist 如下：

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

假设H : implist n (a :: b :: l)不一定来自以GSPairLeft开头的证明，它也可以由GSPairRight和[=13=的实例组成] 并且您的归纳假设不适用。您可以对列表的长度而不是列表本身使用强归纳来解决您的问题。

Answer 2

您只需对 implist 谓词本身进行归纳即可。例如，

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.

Coq 中归纳类型的证明

Proof on inductive type in Coq

coq