# Library Coq.Sorting.Sorting

``` Require Import List. Require Import Multiset. Require Import Permutation. Require Import Relations. Set Implicit Arguments. Section defs. Variable A : Set. Variable leA : relation A. Variable eqA : relation A. Let gtA (x y:A) := ~ leA x y. Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}. Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}. Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y. Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. Hint Resolve leA_refl. Hint Immediate eqA_dec leA_dec leA_antisym. Let emptyBag := EmptyBag A. Let singletonBag := SingletonBag _ eqA_dec. ```
`lelistA`
``` Inductive lelistA (a:A) : list A -> Prop :=   | nil_leA : lelistA a nil   | cons_leA : forall (b:A) (l:list A), leA a b -> lelistA a (b :: l). Hint Constructors lelistA. Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b. Proof.   intros; inversion H; trivial with datatypes. Qed. ```
definition for a list to be sorted
``` Inductive sort : list A -> Prop :=   | nil_sort : sort nil   | cons_sort :       forall (a:A) (l:list A), sort l -> lelistA a l -> sort (a :: l). Hint Constructors sort. Lemma sort_inv :  forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l. Proof. intros; inversion H; auto with datatypes. Qed. Lemma sort_rec :  forall P:list A -> Set,    P nil ->    (forall (a:A) (l:list A), sort l -> P l -> lelistA a l -> P (a :: l)) ->    forall y:list A, sort y -> P y. Proof. simple induction y; auto with datatypes. intros; elim (sort_inv (a:=a) (l:=l)); auto with datatypes. Qed. ```
merging two sorted lists
``` Inductive merge_lem (l1 l2:list A) : Set :=     merge_exist :       forall l:list A,         sort l ->         meq (list_contents _ eqA_dec l)           (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) ->         (forall a:A, lelistA a l1 -> lelistA a l2 -> lelistA a l) ->         merge_lem l1 l2. Lemma merge :  forall l1:list A, sort l1 -> forall l2:list A, sort l2 -> merge_lem l1 l2. Proof.   simple induction 1; intros.   apply merge_exist with l2; auto with datatypes.   elim H3; intros.   apply merge_exist with (a :: l); simpl in |- *; auto with datatypes.   elim (leA_dec a a0); intros.   cut (merge_lem l (a0 :: l0)); auto with datatypes.   intros [l3 l3sorted l3contents Hrec].   apply merge_exist with (a :: l3); simpl in |- *; auto with datatypes.   apply meq_trans with    (munion (singletonBag a)       (munion (list_contents _ eqA_dec l)          (list_contents _ eqA_dec (a0 :: l0)))).   apply meq_right; trivial with datatypes.   apply meq_sym; apply munion_ass.   intros; apply cons_leA.   apply lelistA_inv with l; trivial with datatypes.   elim H5; simpl in |- *; intros.   apply merge_exist with (a0 :: l3); simpl in |- *; auto with datatypes.   apply meq_trans with    (munion (singletonBag a0)       (munion (munion (singletonBag a) (list_contents _ eqA_dec l))          (list_contents _ eqA_dec l0))).   apply meq_right; trivial with datatypes.   apply munion_perm_left.   intros; apply cons_leA; apply lelistA_inv with l0; trivial with datatypes. Qed. End defs. Unset Implicit Arguments. Hint Constructors sort: datatypes v62. Hint Constructors lelistA: datatypes v62. ```