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.
  bdestruct (x1 <=? x2).
  - omega.
  - reflexivity.

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: