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

Require Generic.
Require List_of_A.
Require Multiset_of_A.

(**********************)
(* contents of a list *)
(**********************)

Fixpoint list_contents [l:list] : multiset :=
 Cases l of
   nil        => EmptyBag
 | (cons a l) => (munion (SingletonBag a) (list_contents l))
 end.

Lemma list_contents_app : (l,m:list)
  (meq (list_contents (app l m)) (munion (list_contents l) (list_contents m))).
Proof.
Induction l; Simpl; Auto.
Intros.
Apply meq_trans with  
 (munion (SingletonBag a) (munion (list_contents l0) (list_contents m))); Auto.
Qed.
Hint list_contents_app.

Definition permutation := [l,m:list](meq (list_contents l) (list_contents m)).

Lemma permut_refl : (l:list)(permutation l l).
Proof.
Unfold permutation; Auto.
Qed.
Hint permut_refl.

Lemma permut_tran : (l,m,n:list)
   (permutation l m) -> (permutation m n) -> (permutation l n).
Proof.
Unfold permutation; Intros.
Apply meq_trans with (list_contents m); Auto.
Qed.

Lemma permut_right : (l,m:list)
   (permutation l m) -> (a:A)(permutation (cons a l) (cons a m)).
Proof.
Unfold permutation; Simpl; Auto.
Qed.
Hint permut_right.

Lemma permut_app : (l,l',m,m':list)
   (permutation l l') -> (permutation m m') ->
   (permutation (app l m) (app l' m')).
Proof.
Unfold permutation; Intros.
Apply meq_trans with (munion (list_contents l) (list_contents m)); Auto.
Apply meq_trans with (munion (list_contents l') (list_contents m')); Auto.
Apply meq_trans with (munion (list_contents l') (list_contents m)); Auto.
Qed.
Hint permut_app.

Lemma permut_cons : (l,m:list)(permutation l m) ->
    (a:A)(permutation (cons a l) (cons a m)).
Proof.
Intros l m H a.
Change (permutation (app (cons a nil) l) (app (cons a nil) m)).
Apply permut_app; Auto.
Qed.
Hint permut_cons.

Lemma permut_middle : (l,m:list)
   (a:A)(permutation (cons a (app l m)) (app l (cons a m))).
Proof.
Unfold permutation.
Induction l; Simpl; Auto.
Intros.
Apply meq_trans with (munion (SingletonBag a)
          (munion (SingletonBag a0) (list_contents (app l0 m)))); Auto.
Apply munion_perm_left; Auto.
Qed.
Hint permut_middle.

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