The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

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.
Set Implicit Arguments.

Require Import List.
Require Import Wellfounded.
Require Import Omega.
Require Import OrderedType.

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).

Hint Constructors two_list_sub.

Lemma two_list_sub_acc : forall (A:Set) (l1 l2: list A),
  Acc (@two_list_sub A) (l1, l2).
Proof.
  cut((forall (n:nat) (A : Set) (l1 l2 : list A), length l1 + length l2 < n 
-> Acc (two_list_sub (A:=A)) (l1, l2))).
  intuition eauto.
  induction n ; intros ; constructor ; intros.
  apply False_ind ; omega.
  destruct l1 ; destruct l2 ; inversion H0 ; subst ; simpl in * ;
  apply IHn ; simpl ; omega.
Defined.

Lemma two_list_sub_well_founded : forall (A: Set), well_founded 
(@two_list_sub A).
Proof.
  unfold well_founded.
  intros.
  destruct a as [l1 l2].  
  apply two_list_sub_acc.
Qed.

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.

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.

Lemma merge_nil :merge (nil, nil) = nil.