1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
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.
|
