Proof on inductive type in Coq

Question

I try to prove the following theorem:

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

where implist is as follows :

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]).

During the proof, I reach the following final goal :

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)

But it seems an inversion can't do the job...

How can I prove the theorem ?

Thank you for your help !!

Answer 1

You can just proceed by induction on the implist predicate itself. E.g.,

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.