← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Sorting/Permutation.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Sorting/Permutation.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Permutation.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
 
10
 
 
11
Require Import Relations List Multiset Arith.
 
12
 
 
13
(** This file define a notion of permutation for lists, based on multisets: 
 
14
    there exists a permutation between two lists iff every elements have 
 
15
    the same multiplicities in the two lists. 
 
16
 
 
17
    Unlike [List.Permutation], the present notion of permutation requires
 
18
    a decidable equality. At the same time, this definition can be used 
 
19
    with a non-standard equality, whereas [List.Permutation] cannot.
 
20
      
 
21
    The present file contains basic results, obtained without any particular
 
22
    assumption on the decidable equality used.
 
23
        
 
24
    File [PermutSetoid] contains additional results about permutations 
 
25
    with respect to an setoid equality (i.e. an equivalence relation). 
 
26
 
 
27
    Finally, file [PermutEq] concerns Coq equality : this file is similar 
 
28
    to the previous one, but proves in addition that [List.Permutation]
 
29
    and [permutation] are equivalent in this context.
 
30
x*)
 
31
 
 
32
Set Implicit Arguments.
 
33
 
 
34
Section defs.
 
35
 
 
36
  (** * From lists to multisets *)
 
37
 
 
38
  Variable A : Type.
 
39
  Variable eqA : relation A.
 
40
  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
41
 
 
42
  Let emptyBag := EmptyBag A.
 
43
  Let singletonBag := SingletonBag _ eqA_dec.
 
44
 
 
45
  (** contents of a list *)
 
46
 
 
47
  Fixpoint list_contents (l:list A) : multiset A :=
 
48
    match l with
 
49
      | nil => emptyBag
 
50
      | a :: l => munion (singletonBag a) (list_contents l)
 
51
    end.
 
52
 
 
53
  Lemma list_contents_app :
 
54
    forall l m:list A,
 
55
      meq (list_contents (l ++ m)) (munion (list_contents l) (list_contents m)).
 
56
  Proof.
 
57
    simple induction l; simpl in |- *; auto with datatypes.
 
58
    intros.
 
59
    apply meq_trans with
 
60
      (munion (singletonBag a) (munion (list_contents l0) (list_contents m)));
 
61
      auto with datatypes.
 
62
  Qed.
 
63
 
 
64
  
 
65
  (** * [permutation]: definition and basic properties *)
 
66
  
 
67
  Definition permutation (l m:list A) :=
 
68
    meq (list_contents l) (list_contents m).
 
69
 
 
70
  Lemma permut_refl : forall l:list A, permutation l l.
 
71
  Proof.
 
72
    unfold permutation in |- *; auto with datatypes.
 
73
  Qed.
 
74
  
 
75
  Lemma permut_sym :
 
76
    forall l1 l2 : list A, permutation l1 l2 -> permutation l2 l1.
 
77
  Proof.
 
78
    unfold permutation, meq; intros; apply sym_eq; trivial.
 
79
  Qed.
 
80
  
 
81
  Lemma permut_tran :
 
82
    forall l m n:list A, permutation l m -> permutation m n -> permutation l n.
 
83
  Proof.
 
84
    unfold permutation in |- *; intros.
 
85
    apply meq_trans with (list_contents m); auto with datatypes.
 
86
  Qed.
 
87
  
 
88
  Lemma permut_cons :
 
89
    forall l m:list A,
 
90
      permutation l m -> forall a:A, permutation (a :: l) (a :: m).
 
91
  Proof.
 
92
    unfold permutation in |- *; simpl in |- *; auto with datatypes.
 
93
  Qed.
 
94
  
 
95
  Lemma permut_app :
 
96
    forall l l' m m':list A,
 
97
      permutation l l' -> permutation m m' -> permutation (l ++ m) (l' ++ m').
 
98
  Proof.
 
99
    unfold permutation in |- *; intros.
 
100
    apply meq_trans with (munion (list_contents l) (list_contents m)); 
 
101
      auto using permut_cons, list_contents_app with datatypes.
 
102
    apply meq_trans with (munion (list_contents l') (list_contents m')); 
 
103
      auto using permut_cons, list_contents_app with datatypes.
 
104
    apply meq_trans with (munion (list_contents l') (list_contents m));
 
105
      auto using permut_cons, list_contents_app with datatypes.
 
106
  Qed.
 
107
 
 
108
  Lemma permut_add_inside :
 
109
    forall a l1 l2 l3 l4, 
 
110
      permutation (l1 ++ l2) (l3 ++ l4) ->
 
111
      permutation (l1 ++ a :: l2) (l3 ++ a :: l4).
 
112
  Proof.
 
113
    unfold permutation, meq in *; intros.
 
114
    generalize (H a0); clear H.
 
115
    do 4 rewrite list_contents_app.
 
116
    simpl.
 
117
    destruct (eqA_dec a a0); simpl; auto with arith.
 
118
    do 2 rewrite <- plus_n_Sm; f_equal; auto.
 
119
  Qed.
 
120
  
 
121
  Lemma permut_add_cons_inside :
 
122
    forall a l l1 l2, 
 
123
      permutation l (l1 ++ l2) ->
 
124
      permutation (a :: l) (l1 ++ a :: l2).
 
125
  Proof.
 
126
    intros;
 
127
      replace (a :: l) with (nil ++ a :: l); trivial;
 
128
        apply permut_add_inside; trivial.
 
129
  Qed.
 
130
 
 
131
  Lemma permut_middle :
 
132
    forall (l m:list A) (a:A), permutation (a :: l ++ m) (l ++ a :: m).
 
133
  Proof.
 
134
    intros; apply permut_add_cons_inside; auto using permut_sym, permut_refl.
 
135
  Qed.
 
136
  
 
137
  Lemma permut_sym_app :
 
138
    forall l1 l2, permutation (l1 ++ l2) (l2 ++ l1).
 
139
  Proof.
 
140
    intros l1 l2;
 
141
      unfold permutation, meq; 
 
142
        intro a; do 2 rewrite list_contents_app; simpl; 
 
143
          auto with arith.
 
144
  Qed.
 
145
 
 
146
  Lemma permut_rev : 
 
147
    forall l, permutation l (rev l).
 
148
  Proof.
 
149
    induction l.
 
150
    simpl; trivial using permut_refl.
 
151
    simpl.
 
152
    apply permut_add_cons_inside.
 
153
    rewrite <- app_nil_end. trivial.
 
154
  Qed.
 
155
 
 
156
  (** * Some inversion results. *)
 
157
  Lemma permut_conv_inv :
 
158
    forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
 
159
  Proof.
 
160
    intros e l1 l2; unfold permutation, meq; simpl; intros H a;
 
161
      generalize (H a); apply plus_reg_l.
 
162
  Qed.
 
163
 
 
164
  Lemma permut_app_inv1 : 
 
165
    forall l l1 l2, permutation (l1 ++ l) (l2 ++ l) -> permutation l1 l2.
 
166
  Proof.
 
167
    intros l l1 l2; unfold permutation, meq; simpl;
 
168
      intros H a; generalize (H a); clear H.
 
169
    do 2 rewrite list_contents_app.
 
170
    simpl.
 
171
    intros; apply plus_reg_l with (multiplicity (list_contents l) a).
 
172
    rewrite plus_comm; rewrite H; rewrite plus_comm.
 
173
    trivial.
 
174
  Qed.
 
175
 
 
176
  Lemma permut_app_inv2 : 
 
177
    forall l l1 l2, permutation (l ++ l1) (l ++ l2) -> permutation l1 l2.
 
178
  Proof.
 
179
    intros l l1 l2; unfold permutation, meq; simpl;
 
180
      intros H a; generalize (H a); clear H.
 
181
    do 2 rewrite list_contents_app.
 
182
    simpl.
 
183
    intros; apply plus_reg_l with (multiplicity (list_contents l) a).
 
184
    trivial.
 
185
  Qed.
 
186
 
 
187
  Lemma permut_remove_hd :
 
188
    forall l l1 l2 a,   
 
189
      permutation (a :: l) (l1 ++ a :: l2) -> permutation l (l1 ++ l2).
 
190
  Proof.
 
191
    intros l l1 l2 a; unfold permutation, meq; simpl; intros H a0; generalize (H a0); clear H.
 
192
    do 2 rewrite list_contents_app; simpl; intro H.
 
193
    apply plus_reg_l with (if eqA_dec a a0 then 1 else 0).
 
194
    rewrite H; clear H.
 
195
    symmetry; rewrite plus_comm.
 
196
    repeat rewrite <- plus_assoc; f_equal.
 
197
    apply plus_comm.
 
198
  Qed.
 
199
 
 
200
End defs.
 
201
 
 
202
(** For compatibilty *) 
 
203
Notation permut_right := permut_cons.
 
204
Unset Implicit Arguments.