(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                Sorting.v                                 *)
(****************************************************************************)


Require Generic.
Require A_total_ordering.
Require List_of_A.
Require Multiset_of_A.
Require Permutation.

(************)
(* inf_list *)
(************)

Inductive inf_list [a:A] : list -> Prop :=
      nil_inf : (inf_list a nil)
    | cons_inf : (b:A)(l:list)(inf a b)->(inf_list a (cons b l)).
Hint nil_inf cons_inf.


Lemma inf_list_inv : (a,b:A)(l:list)
      (inf_list a (cons b l)) -> (inf a b).
Proof.
Intros; Inversion H; Trivial.
Qed.

(**************************************)
(* definition for a list to be sorted *)
(**************************************)

Inductive sort : list -> Prop :=
   nil_sort : (sort nil)
 | cons_sort : (a:A)(l:list)(sort l) -> (inf_list a l) -> (sort (cons a l)).
Hint nil_sort cons_sort.


Lemma sort_inv : (a:A)(l:list)(sort (cons a l))->(sort l) /\ (inf_list a l).
Proof.
Intros; Inversion H; Auto.
Qed.

Lemma sort_rec : (P:list->Set)
     (P nil) ->
     ((a:A)(l:list)(sort l)->(P l)->(inf_list a l)->(P (cons a l))) ->
     (y:list)(sort y) -> (P y).
Proof.
Induction y; Auto.
Intros; Elim (sort_inv a l); Auto.
Qed.

(****************************)
(* merging two sorted lists *)
(****************************)

Inductive merge_lem [l1:list;l2:list] : Set :=
  merge_exist : (l:list)(sort l) ->
    (meq (list_contents l)
         (munion (list_contents l1) (list_contents l2))) ->
    ((a:A)(inf_list a l1)->(inf_list a l2)->(inf_list a l)) ->
    (merge_lem l1 l2).

Lemma merge : (l1:list)(sort l1)->(l2:list)(sort l2)->(merge_lem l1 l2).
Proof.
Intros l1 s; Elim s; Intros.
Apply merge_exist with l2; Auto.
Elim H2; Intros.
Apply merge_exist with (cons a l); Simpl; Auto.
Elim (inf_total a a0); Intros.
(* 1 (inf a a0) *)
Cut (merge_lem l (cons a0 l0)); Auto.
Intro H_mg; Elim H_mg; Intros. 
Apply merge_exist with (cons a l3); Simpl; Auto.
Apply meq_trans with (munion (SingletonBag a) 
      (munion (list_contents l) (list_contents (cons a0 l0)))).
Apply meq_right; Trivial.
Apply meq_sym; Apply munion_ass.
Intros; Apply cons_inf.
Apply inf_list_inv with l; Trivial.
(* 2 (inf a0 a) *)
Elim H4; Simpl; Intros.
Apply merge_exist with (cons a0 l3); Simpl; Auto.
Apply meq_trans with (munion (SingletonBag a0)
      (munion (munion (SingletonBag a) (list_contents l)) (list_contents l0))).
Apply meq_right; Trivial.
Apply munion_perm_left.
Intros; Apply cons_inf; Apply inf_list_inv with l0; Trivial.
Qed.


(* $Id: Sorting.v,v 1.4 1998/04/30 16:45:57 mohring Exp $ *)
