Fail to prove a permutation property

Question

I have created this simple type :

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

and I try to prove this permutation lemma :

Lemma permutImplist :
  forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) <-> implist n ((c::b::a::input)).

I've tried various induction principles on the type itself or the list, but always end up in a dead end.

Can someone help me with this proof ?

Thanks !!

Answer 1

The induction principle of this predicate is not very useful for proving this directly. It is much better to find an alternative formulation of implist to make your proof go through:

From Coq Require Import List PeanoNat Lia.
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]).

Lemma implist_alt n l :
  implist n l <->
  exists l1 l2,
    l = l1 ++ n :: l2 /\
    Nat.even (length l1) = true /\
    Nat.even (length l2) = true.
Proof.
split.
- intros H. induction H as [n|a b n l _ IH|a b n l _ IH].
  + exists [], []; intuition.
  + destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
    exists (a :: b :: l1), l2; intuition.
  + destruct IH as (l1 & l2 & -> & Hl1 & Hl2).
    exists l1, (l2 ++ [a; b]). simpl.
    rewrite <- app_assoc, app_length, Nat.add_comm.
    intuition.
- intros (l1 & l2 & -> & Hl1 & Hl2).
  assert (Hb1 : exists b, length l1 < b) by (exists (S (length l1)); lia).
  destruct Hb1 as (b1 & Hb1).
  assert (Hb2 : exists b, length l2 < b) by (exists (S (length l2)); lia).
  destruct Hb2 as (b2 & Hb2).
  revert l1 b2 l2 Hl1 Hl2 Hb1 Hb2.
  induction (Nat.lt_wf_0 b1) as [b1 _ IH1].
  intros [| x1 [| y1 l1]]; simpl; try easy.
  + intros b2 l2 _ Hl2 _. revert l2 Hl2.
    induction (Nat.lt_wf_0 b2) as [b2 _ IH2].
    induction l2 as [|x2 l2 _] using rev_ind.
    * intros _ _. apply GSSingle.
    * induction l2 as [|y2 l2 _] using rev_ind; simpl; try easy.
      rewrite !app_length. simpl. rewrite <- Nat.add_assoc, Nat.add_comm. simpl.
      intros Hl2 Hb2. rewrite <- app_assoc.
      change (n :: l2 ++ [y2] ++ [x2]) with ((n::l2) ++ [y2] ++ [x2]).
      apply GSPairRight. apply (IH2 (S (S (length l2)))); eauto; lia.
  + intros b2 l2 Hl1 Hl2 Hb1 Hb2.
    apply (GSPairLeft x1 y1). apply (IH1 (S (S (length l1))) Hb1 _ b2); eauto.
Qed.

Lemma permutImplist_aux :
  forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) -> implist n ((c::b::a::input)).
Proof.
intros n a b c l (l1 & l2 & e & Hl1 & Hl2)%implist_alt.
destruct l1 as [|x l1]; simpl in *.
{ injection e as <- <-; simpl in *.
  apply implist_alt. exists [c; b], l; intuition. }
destruct l1 as [|y l1]; simpl in *; try easy.
injection e as <- <- e.
destruct l1 as [|z l1]; simpl in *.
{ injection e as <- <-.
  apply implist_alt. exists [], (b :: a :: l); intuition. }
destruct l1 as [|w l1]; simpl in *; try easy.
injection e as <- ->.
apply implist_alt. exists (c :: b :: a :: w :: l1), l2.
intuition.
Qed.

Lemma permutImplist :
  forall (n a b c:nat) (input:list nat), implist n ((a::b::c::input)) <-> implist n ((c::b::a::input)).
Proof.
intros n a b c l; split; apply permutImplist_aux.
Qed.

The tricky part, as you can see, is the reverse direction of implist_alt. The ideal way of proving this would be to have an induction principle for lists of even length. Since we do not have this, I have instead used strong induction on the length of the even lists, which works fine as well.