Coq 中归纳类型的证明答案

【问题标题】：Proof on inductive type in CoqCoq 中归纳类型的证明
【发布时间】：2022-05-10 21:20:57
【问题描述】：

我试图证明以下定理：

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)

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

我怎样才能证明这个定理？

谢谢您的帮助！！

【问题讨论】：

标签： coq

【解决方案1】：

您可以对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.

【讨论】：

【解决方案2】：

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

【讨论】：