diff options
Diffstat (limited to 'theories/Sorting/Permutation.v')
-rw-r--r-- | theories/Sorting/Permutation.v | 120 |
1 files changed, 120 insertions, 0 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v new file mode 100644 index 00000000..43a0f0bc --- /dev/null +++ b/theories/Sorting/Permutation.v @@ -0,0 +1,120 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Permutation.v,v 1.4.2.1 2004/07/16 19:31:19 herbelin Exp $ i*) + +Require Import Relations. +Require Import List. +Require Import Multiset. + +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 x y}. +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: default. +Hint Immediate eqA_dec leA_dec leA_antisym: default. + +Let emptyBag := EmptyBag A. +Let singletonBag := SingletonBag _ eqA_dec. + +(** contents of a list *) + +Fixpoint list_contents (l:list A) : multiset A := + match l with + | nil => emptyBag + | a :: l => munion (singletonBag a) (list_contents l) + end. + +Lemma list_contents_app : + forall l m:list A, + meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)). +Proof. +simple induction l; simpl in |- *; auto with datatypes. +intros. +apply meq_trans with + (munion (singletonBag a) (munion (list_contents l0) (list_contents m))); + auto with datatypes. +Qed. +Hint Resolve list_contents_app. + +Definition permutation (l m:list A) := + meq (list_contents l) (list_contents m). + +Lemma permut_refl : forall l:list A, permutation l l. +Proof. +unfold permutation in |- *; auto with datatypes. +Qed. +Hint Resolve permut_refl. + +Lemma permut_tran : + forall l m n:list A, permutation l m -> permutation m n -> permutation l n. +Proof. +unfold permutation in |- *; intros. +apply meq_trans with (list_contents m); auto with datatypes. +Qed. + +Lemma permut_right : + forall l m:list A, + permutation l m -> forall a:A, permutation (a :: l) (a :: m). +Proof. +unfold permutation in |- *; simpl in |- *; auto with datatypes. +Qed. +Hint Resolve permut_right. + +Lemma permut_app : + forall l l' m m':list A, + permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m'). +Proof. +unfold permutation in |- *; intros. +apply meq_trans with (munion (list_contents l) (list_contents m)); + auto with datatypes. +apply meq_trans with (munion (list_contents l') (list_contents m')); + auto with datatypes. +apply meq_trans with (munion (list_contents l') (list_contents m)); + auto with datatypes. +Qed. +Hint Resolve permut_app. + +Lemma permut_cons : + forall l m:list A, + permutation l m -> forall a:A, permutation (a :: l) (a :: m). +Proof. +intros l m H a. +change (permutation ((a :: nil) ++ l) ((a :: nil) ++ m)) in |- *. +apply permut_app; auto with datatypes. +Qed. +Hint Resolve permut_cons. + +Lemma permut_middle : + forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m). +Proof. +unfold permutation in |- *. +simple induction l; simpl in |- *; auto with datatypes. +intros. +apply meq_trans with + (munion (singletonBag a) + (munion (singletonBag a0) (list_contents (l0 ++ m)))); + auto with datatypes. +apply munion_perm_left; auto with datatypes. +Qed. +Hint Resolve permut_middle. + +End defs. +Unset Implicit Arguments. |