Solving a mergesort split proof in Coq

Question

I am currently working on the volume 3 of the Software Foundations' textbook Verified Functional Algorithm and I am stuck on the proof of one exercise.

You can find the chapter about Mergesort which I am dealing with at the moment here: https://softwarefoundations.cis.upenn.edu/vfa-current/Merge.html

This is where I am stuck so far:

(** **** Exercise: 3 stars, standard (split_perm)  *)

(** Here's another fact about [split] that we will find useful later on.  
*)

Lemma split_perm : forall {X:Type} (l l1 l2: list X),
    split l = (l1,l2) -> Permutation l (l1 ++ l2).
Proof.
  induction l as [| x | x1 x2 l1' IHl'] using list_ind2; intros.
- inv H. simpl. reflexivity.
- inv H. simpl. reflexivity.
- inv H. 

And this is the result from my last tactic "inv H."

1 subgoal
X : Type
x1, x2 : X
l1' : list X
IHl' : forall l1 l2 : list X, split l1' = (l1, l2) -> Permutation l1' (l1 ++ l2)
l1, l2 : list X
H1 : (let (l1, l2) := split l1' in (x1 :: l1, x2 :: l2)) = (l1, l2)
______________________________________(1/1)
Permutation (x1 :: x2 :: l1') (l1 ++ l2)

Any leads on how I should continue to prove my goal ? Permutation (x1 :: x2 :: l1') (l1 ++ l2)

Answer 1

I think a first step is to get rid of split l', so destruct (split l') and then an inversion on H1 should simplify your goal