# Software Foundations/ Verified Functional Algorithms Exercise

Hi, I’m trying to solve this exercise. It’s from the merge part

Lemma sorted_merge : forall l1, sorted l1 ->
forall l2, sorted l2 ->
sorted (merge l1 l2).

intros. induction l1.

• simpl. induction l2.
• auto.
• auto.
• induction l2.
• auto.
• simpl. bdestruct (a<=?a0).
• inv H.
** auto. constructor. auto. auto.
** apply sorted_merge1. auto. auto. auto.

but in the second part of the proof, I don’t know how to follow.
Thank you

Here are a few hints:

1. You should introduce names in `intros` and `induction`. This makes the proofs easier to understand, because the names are more reasonable. (See the proof script skeleton below)
2. In the second step, instead of `simpl`, you should use a rewriting lemma like `merge2`. You should do a case analysis on `x <= y`, where `x` and `y` are the first elements of the lists. In the first case, you can rewrite `merge (x :: l1) (y :: l2)` with `merge2`. For the second case, you need a symmetric lemma:
``````Lemma merge3 : forall (x1 x2:nat) r1 r2,
x2 < x1 ->
merge (x1::r1) (x2::r2) =
x2::merge (x1::r1) r2.
Proof.
intros.
simpl.
bdestruct (x1 <=? x2).
- omega.
- reflexivity.
Qed.
``````

I also used the following two inversion lemmas:

``````Lemma sorted_cons_inv : forall x y l1, sorted (x :: y :: l1) -> x <= y /\ sorted (y :: l1).
Proof. intros. now inversion H. Qed.

Lemma sorted_cons_inv' : forall x l1, sorted (x :: l1) -> sorted l1.
Proof. intros. now inversion H. Qed.
``````

Now, here’s the skeleton of the proof script. You should be able to fill in the gaps yourself.

``````  intros l1.
induction l1 as [ | x l1 IHl1]; intros Hsorted1.
- intros [ | x l2']; simpl; tauto.
- induction l2 as [ | y l2 IHl2]; intros Hsorted2.
+ simpl. tauto.
+ bdestruct (x <=? y).
* (* ... *)
* (* ... *)
``````

PS: Please surround code with ```, like this:

`````````
code
```
``````