Unprovable list lemma split_of_app_right

[palmskog]

The lemma split_of_app_right in systems/chord-props/QueryInvariant.v is unprovable as currently stated:

Lemma split_of_app_right :
  forall A (l l' : list A) xs a ys,
    l ++ l' = xs ++ a :: ys ->
    In a l' ->
    exists xs',
      xs = l ++ xs' /\
      l' = xs' ++ a :: ys.

To see why, set l = a0 :: l0 (for some a0 : A and l0 : list A) and xs = []. Then, we have to prove exists xs', [] = a0 :: l0 ++ xs', which is clearly impossible.

It may be possible to save the lemma by ruling out this case (e.g., by requiring xs <> []).

[palmskog]

I believe split_of_app_left is similarly unprovable. However, here are two variants of the lemmas that work:

Lemma split_of_app_right' :
  forall A (l l' : list A) xs a ys,
    l ++ l' = xs ++ a :: ys ->
    ~ In a l ->
    In a l' ->
    exists xs',
      xs = l ++ xs' /\
      l' = xs' ++ a :: ys.
Proof.
move => A.
elim => /=; first by move => l' xs a ys Hl Hin Hin'; exists xs.
move => a l IH l'.
case => //=.
- move => a0 ys Ha Hin Hin'.
  inversion Ha; subst.
  by case: Hin; left.
- move => a0 l0 a1 ys Hl Hin Hin'.
  inversion Hl; subst.
  have Hn: a0 <> a1.
    move => Hn.
    case: Hin.
    by left.
  have Hn': ~ In a1 l.
    move => Hn'.
    case: Hin.
    by right.
  have [xs' [Hl0 IH']] := IH _ _ _ _ H1 Hn' Hin'.
  exists xs'.
  split => //.
  by rewrite Hl0.
Qed.

Lemma split_of_app_left' :
  forall A (l l' : list A) xs a ys,
    l ++ l' = xs ++ a :: ys ->
    In a l ->
    ~ In a l' ->
    exists ys',
      ys = ys' ++ l' /\
      l = xs ++ a :: ys'.
Proof.
move => A.
elim => //=.
move => a l IH l'.
case => /= [|a' xs] //.
- move => a0 ys Hl.
  inversion Hl; subst.
  move => Hin Hin'.  
  by exists l.
- move => a0 ys Hl Ha Ha'.
  inversion Hl; subst.
  case: Ha => Ha.
  * subst.
    have Hin: In a0 (l ++ l').
      rewrite H1.
      apply in_or_app.
      by right; left.
    apply in_app_or in Hin.
    case: Hin => Hin //.
    have [ys' [Hn IH']] := IH _ _ _ _ H1 Hin Ha'.
    exists ys'; split => //.
    by rewrite IH'.
  * have [ys' [Hn IH']] := IH _ _ _ _ H1 Ha Ha'.
    exists ys'; split => //.
    by rewrite IH'.
Qed.