Can't find a way to 'reverse' a constructor

Question

I try to prove the following simple Lemma :

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

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

Any idea how to do this ?

Thank you !!

Answer 1

Here it is:

Require Import Program.Equality.

Lemma wayBack :
  forall (a b n:nat) (input:list nat), a <> n -> implist n (a::b::input) -> implist n input.
Proof.
  intros.
  dependent induction H0.
  1: eassumption.
  assert (exists l', l = a :: b :: l' /\ input = l' ++ [a0 ; b0]) as [l' [-> ->]].
  {
    clear - x H0 H.
    change (l ++ [a0] ++ [b0]) with (l ++ [a0; b0]) in x.
    remember [a0; b0] as t in *.
    clear Heqt.
    induction H0 in input, t, x, H |- *.
    + cbn in *.
      inversion x ; subst.
      now destruct H.
    + cbn in *.
      inversion x ; subst ; clear x.
      eexists ; split.
      1: reflexivity.
      reflexivity.
    + cbn in x.
      rewrite <- app_assoc in x.
      edestruct IHimplist as [? []] ; try eassumption.
      subst.
      eexists ; split.
      cbn.
      2: rewrite app_assoc.
      all: reflexivity.
  }
  econstructor.
  eapply IHimplist ; try eassumption.
  reflexivity.
Qed.

There are two main difficulties here: the first is that you want to do an induction on you hypothesis implist n (a::b::input), but since a::b::input is not just a variable, there is a need for some fiddling, that standard induction cannot do, but dependent induction from Program can.

The second difficulty, which actually takes up most of my proof, is to be able to decompose the equality you get in the last case, that where you add values at the beginning rather than at the end of the list.