The Coq mailing list

[Matthieu Sozeau <sozeau AT lri.fr>]

Edsko de Vries a écrit :
> Hi,
>
>   
Hi,
> I have been trying to define merge sort (because it should be easy to
> prove that merge M1 M2 = merge M2 M1, the property I needed for my sets;
> see previous thread). Obviously, merge sort is structurally recursive on
> two arguments, so we need (I think!) some trickery to make it work. This
> is my attempt so far: I introduce a "substructure" relation on a pair of
> lists:
>
>   Inductive two_list_sub (A: Set) : (list A * list A) -> (list A * list A) -> 
> Prop :=
>     | two_list_sub_l1 : forall (a: A) (l1 l2: list A), 
>         two_list_sub (l1, l2) (a :: l1, l2)
>     | two_list_sub_l2 : forall (a: A) (l1 l2: list A), 
>         two_list_sub (l1, l2) (l1, a :: l2).
>
> I then prove that this relation is well-founded:
>
>   Lemma two_list_sub_well_founded : forall (A: Set), 
>     well_founded (@two_list_sub A).
>   
You need this lemma to be "Defined" so that Coq can unfold its
definition to actually
compute with the fixpoint on this proof.

Then the following works:

Lemma merge_nil :merge (nil, nil) = nil.
simpl.
unfold two_list_induction.
unfold well_founded_induction, well_founded_induction_type.
simpl.
reflexivity.
Qed.

I'm not sure why the unfolding is not done automatically here...

As an alternative you could use Program to write these kind of 
definitions more conveniently. Using a measure already gets rid of all 
this wellfounded code, while it is still using the (transparent) proof 
of Wf_nat instead. Also you get to write code and not tactics. This 
permits to write an efficient version compared to yours where two 
recursive calls were always performed when only one was actually needed.

(* beware the following has been tested with trunk only *)
Require Import List.
Require Import Wellfounded.
Require Import Omega.
Require Import OrderedType.
Require Import Program.

Definition two_list_measure (A:Set) (l1 : list A * list A) :=
 length (fst l1) + length (snd l1).

Module SortedList (OT : OrderedType).

Program Fixpoint merge (p : list OT.t * list OT.t)
 { measure (two_list_measure OT.t) } :=
 match p with
   | (l1, nil) => l1
   | (nil, l2) => l2
   | ((hd1::tl1) as l1, (hd2::tl2) as l2) =>
     match OT.compare hd1 hd2 with
       | GT _ => hd2 :: merge (l1, tl2)
       | _ => hd1 :: merge (tl1, l2)
     end
 end.

(* The two obligations for the two recursive calls *)
Solve Obligations using program_simpl ; intros ;
 autoinjection ; unfold two_list_measure ; simpl ; omega.

Lemma merge_nil :merge (nil, nil) = nil.
Proof with program_simpl.
 simpl...
Qed.

Hope this helps,
--
Matthieu Sozeau
http://www.lri.fr/~sozeau