CODEWITHSUNDEEP
coqmergesortproof
John Regis
John Regis

Reputation: 21

Solving a split proof in Coq

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:

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.
  - inversion H. simpl. reflexivity.
  - inversion H. simpl. reflexivity.
  - inversion H. destruct (split l1'). inversion H1. simpl. apply perm_skip.
    apply Permutation_cons_app.

And this is the result from my last tactic "apply Permutation_cons_app."

1 subgoal
X : Type
x1, x2 : X
l1', l, l0 : list X
IHl' : forall l1 l2 : list X,
       (l, l0) = (l1, l2) -> Permutation l1' (l1 ++ l2)
l1, l2 : list X
H : split (x1 :: x2 :: l1') = (l1, l2)
H1 : (x1 :: l, x2 :: l0) = (l1, l2)
H2 : x1 :: l = l1
H3 : x2 :: l0 = l2
______________________________________(1/1)
Permutation (x2 :: l1') (l ++ x2 :: l0)

Any leads on how I should continue to prove my goal ?

Upvotes: 1

Views: 229

Answers (1)

Andrey
Andrey

Reputation: 750

Well, actually right now you have result from apply perm_skip. After you have applyed Permutations_cons_app, you need pay attention on your induction hypothises.

Upvotes: 2

Related Questions