The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

On Wed, 7 Nov 2007 19:26:23 +0000
Edsko de Vries 
<devriese AT cs.tcd.ie>
 wrote:

> 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).
> 
> And then define an iterator like the list_rec iterator but one that works on
> pairs of lists:
> 
>   Definition two_list_induction (A: Set) (P : (list A * list A) -> Set) :
>     (forall (l: list A), P (nil, l)) ->
>     (forall (l: list A), P (l, nil)) ->
>     (forall (l1 l2: list A) (a1 a2: A), 
>        P (l1, a2 :: l2) ->
>        P (a1 :: l1, l2) ->
>        P (a1 :: l1, a2 :: l2)) ->
>     forall (l1 l2: list A), P (l1, l2).
>   intros.
>   apply (well_founded_induction (@two_list_sub_well_founded A)).
>   intros ; destruct x as [l1' l2'] ; destruct l1' ; destruct l2' ; auto.
>   Defined.
> 
> Finally, I define merge sort using the new iterator:
> 
>   Module SortedList (OT : OrderedType).
>   
>   Definition merge : (list OT.t * list OT.t) -> list OT.t.
>   intros.
>   destruct H as [l1 l2].
>   apply (two_list_induction (fun _ : (list OT.t * list OT.t) => list OT.t)).
>   intros ; exact l2.
>   intros ; exact l1.
>   intros l1_tail l2_tail a1 a2 l1_rec l2_rec.
>   case (OT.compare a1 a2) ; intros.
>   exact (a1 :: l1_rec).
>   exact (a1 :: l1_rec).
>   exact (a2 :: l2_rec).
>   exact l1.
>   exact l2.
>   Defined.
> 
> This seems to work, but I get stuck when I try to define even the
> simplest lemmas about 'merge':
> 
>   Lemma merge_nil :merge (nil, nil) = nil.
> 
> Unfolding merge, and then two_list_induction, and then
> well_founded_induction, etc. yields a very big term on the left hand
> side, but never one that can be simplified to nil. Am I doing something
> stupid?
> 
> Thanks!
> 
> Edsko 
> 
> PS. Full development is attached.

Hi, 
you can try the new Function feature. This will allow you to define
much more simply your function merge AND compute with the obtained
function. Moreover this will give you induction principle to reason on merge 
and an equation lemma. 
New code is attached.


Julien Forest.

Attachment: two_list_induction.v
Description: Binary data