The Coq mailing list

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

On Wed, Nov 07, 2007 at 11:00:40PM +0100, Yevgeniy Makarov wrote:
> Hello,
> 
> I followed Benjamin's hint, and here's my version of merge on lists of
> natural numbers:
> 
> Require Import List.
> Require Import Compare_dec.
> 
> Fixpoint merge (l1 : list nat) : list nat -> list nat :=
> fix merge_helper (l2 : list nat) :=
> match l1, l2 with
> | nil, nil => nil
> | nil, l => l
> | l, nil => l
> | x1 :: l1, x2 :: l2 =>
>   if leb x1 x2
>   then x1 :: merge l1 (x2 :: l2)
>   else x2 :: merge_helper l2
> end.

Thanks for the code, I didn't quite understand the original hint. This
is a nice trick, I hadn't come across it before.

Thanks all for the help!

Edsko

PS. I've attached my preferred 'symmetric' merge plus a proof that it is
indeed symmetric, in that 'merge l1 l2 = merge l2 l1', for arbitrary
lists l1 l2.
Require Import List.
Require Import OrderedType.
Require Import OrderedTypeEx.

Tactic Notation "unsimpl" constr(E) :=
  let F := (eval simpl in E) in change F with E.

Module MultiSet (OT : UsualOrderedType).

Fixpoint merge (l1: list OT.t) : list OT.t -> list OT.t := 
  fix merge_aux (l2: list OT.t) : list OT.t :=
    match (l1, l2) with
    | (nil, nil) => nil
    | (nil, l2) => l2
    | (l1, nil) => l1
    | (a1 :: l1_tail, a2 :: l2_tail) => 
        match OT.compare a1 a2 with
        | LT _ => a1 :: merge l1_tail l2
        | EQ _ => a1 :: a2 :: merge l1_tail l2_tail
        | GT _ => a2 :: merge_aux l2_tail
        end
    end.

Lemma not_ltab_ltba : forall a b,
  OT.lt a b -> OT.lt b a -> False.
Proof (fun a b H H0 => OT.lt_not_eq _ _ (OT.lt_trans _ _ _ H H0) (OT.eq_refl 
a)).

Lemma not_ltab_eqab : forall a b,
  OT.lt a b -> OT.eq a b -> False.
Proof (fun a b H H0 => OT.lt_not_eq _ _ H H0).

Lemma not_ltab_eqba : forall a b,
  OT.lt a b -> OT.eq b a -> False.
Proof (fun a b H H0 => OT.lt_not_eq _ _ H (OT.eq_sym _ _ H0)).

Hint Resolve not_ltab_ltba not_ltab_eqab not_ltab_eqba : lt_contradictions.

Lemma merge_comm : forall l1 l2,
  merge l1 l2 = merge l2 l1.
Proof.
  induction l1 ; induction l2 ; simpl ; auto.
  case (OT.compare a a0) ; case (OT.compare a0 a) ; intros ;
    try (apply False_ind ; eauto with lt_contradictions ; fail).
  unsimpl (merge (a0 :: l2) l1).
  rewrite IHl1 ; reflexivity.
  rewrite e ; rewrite IHl1 ; reflexivity.
  unsimpl (merge (a :: l1) l2).
  rewrite IHl2 ; reflexivity.
Qed.

End MultiSet.