Library Coq.Sorting.Sorting
Require Import List Multiset Permutation Relations.
Section defs.
Variable A : Type.
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).
Lemma lelistA_inv : forall (a b:A) (l:list A), lelistA a (b :: l) -> leA a b.
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).
Lemma sort_inv :
forall (a:A) (l:list A), sort (a :: l) -> sort l /\ lelistA a l.
Lemma sort_rect :
forall P:list A -> Type,
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.
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.
Inductive merge_lem (l1 l2:list A) : Type :=
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.
End defs.
Hint Constructors sort: datatypes v62.
Hint Constructors lelistA: datatypes v62.