← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Sorting/Heap.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/Heap.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: Heap.v 10698 2008-03-19 18:46:59Z letouzey $ i*)
 
10
 
 
11
(** A development of Treesort on Heap trees *)
 
12
 
 
13
(* G. Huet 1-9-95 uses Multiset *)
 
14
 
 
15
Require Import List Multiset Permutation Relations Sorting.
 
16
 
 
17
Section defs.
 
18
 
 
19
  (** * Trees and heap trees *)
 
20
 
 
21
  (** ** Definition of trees over an ordered set *)
 
22
 
 
23
  Variable A : Type.
 
24
  Variable leA : relation A.
 
25
  Variable eqA : relation A.
 
26
 
 
27
  Let gtA (x y:A) := ~ leA x y.
 
28
  
 
29
  Hypothesis leA_dec : forall x y:A, {leA x y} + {leA y x}.
 
30
  Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
 
31
  Hypothesis leA_refl : forall x y:A, eqA x y -> leA x y.
 
32
  Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
 
33
  Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
34
 
 
35
  Hint Resolve leA_refl.
 
36
  Hint Immediate eqA_dec leA_dec leA_antisym.
 
37
 
 
38
  Let emptyBag := EmptyBag A.
 
39
  Let singletonBag := SingletonBag _ eqA_dec.
 
40
  
 
41
  Inductive Tree :=
 
42
    | Tree_Leaf : Tree
 
43
    | Tree_Node : A -> Tree -> Tree -> Tree.
 
44
 
 
45
  (** [a] is lower than a Tree [T] if [T] is a Leaf
 
46
      or [T] is a Node holding [b>a] *)
 
47
 
 
48
  Definition leA_Tree (a:A) (t:Tree) :=
 
49
    match t with
 
50
      | Tree_Leaf => True
 
51
      | Tree_Node b T1 T2 => leA a b
 
52
    end.
 
53
 
 
54
  Lemma leA_Tree_Leaf : forall a:A, leA_Tree a Tree_Leaf.
 
55
  Proof.
 
56
    simpl in |- *; auto with datatypes.
 
57
  Qed.
 
58
 
 
59
  Lemma leA_Tree_Node :
 
60
    forall (a b:A) (G D:Tree), leA a b -> leA_Tree a (Tree_Node b G D).
 
61
  Proof.
 
62
    simpl in |- *; auto with datatypes.
 
63
  Qed.
 
64
 
 
65
 
 
66
  (** ** The heap property *)
 
67
 
 
68
  Inductive is_heap : Tree -> Prop :=
 
69
    | nil_is_heap : is_heap Tree_Leaf
 
70
    | node_is_heap :
 
71
      forall (a:A) (T1 T2:Tree),
 
72
        leA_Tree a T1 ->
 
73
        leA_Tree a T2 ->
 
74
        is_heap T1 -> is_heap T2 -> is_heap (Tree_Node a T1 T2).
 
75
 
 
76
  Lemma invert_heap :
 
77
    forall (a:A) (T1 T2:Tree),
 
78
      is_heap (Tree_Node a T1 T2) ->
 
79
      leA_Tree a T1 /\ leA_Tree a T2 /\ is_heap T1 /\ is_heap T2.
 
80
  Proof.
 
81
    intros; inversion H; auto with datatypes.
 
82
  Qed.
 
83
 
 
84
  (* This lemma ought to be generated automatically by the Inversion tools *)
 
85
  Lemma is_heap_rect :
 
86
    forall P:Tree -> Type,
 
87
      P Tree_Leaf ->
 
88
      (forall (a:A) (T1 T2:Tree),
 
89
        leA_Tree a T1 ->
 
90
        leA_Tree a T2 ->
 
91
        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
 
92
      forall T:Tree, is_heap T -> P T.
 
93
  Proof.
 
94
    simple induction T; auto with datatypes.
 
95
    intros a G PG D PD PN. 
 
96
    elim (invert_heap a G D); auto with datatypes.
 
97
    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
 
98
    apply X0; auto with datatypes.
 
99
  Qed.
 
100
 
 
101
  (* This lemma ought to be generated automatically by the Inversion tools *)
 
102
  Lemma is_heap_rec :
 
103
    forall P:Tree -> Set,
 
104
      P Tree_Leaf ->
 
105
      (forall (a:A) (T1 T2:Tree),
 
106
        leA_Tree a T1 ->
 
107
        leA_Tree a T2 ->
 
108
        is_heap T1 -> P T1 -> is_heap T2 -> P T2 -> P (Tree_Node a T1 T2)) ->
 
109
      forall T:Tree, is_heap T -> P T.
 
110
  Proof.
 
111
    simple induction T; auto with datatypes.
 
112
    intros a G PG D PD PN. 
 
113
    elim (invert_heap a G D); auto with datatypes.
 
114
    intros H1 H2; elim H2; intros H3 H4; elim H4; intros.
 
115
    apply X; auto with datatypes.
 
116
  Qed.
 
117
 
 
118
  Lemma low_trans :
 
119
    forall (T:Tree) (a b:A), leA a b -> leA_Tree b T -> leA_Tree a T.
 
120
  Proof.
 
121
    simple induction T; auto with datatypes.
 
122
    intros; simpl in |- *; apply leA_trans with b; auto with datatypes.
 
123
  Qed.
 
124
 
 
125
 
 
126
  (** ** From trees to multisets *)
 
127
 
 
128
  (** contents of a tree as a multiset *)
 
129
 
 
130
  (** Nota Bene : In what follows the definition of SingletonBag
 
131
      in not used. Actually, we could just take as postulate:
 
132
      [Parameter SingletonBag : A->multiset].  *)
 
133
 
 
134
  Fixpoint contents (t:Tree) : multiset A :=
 
135
    match t with
 
136
      | Tree_Leaf => emptyBag
 
137
      | Tree_Node a t1 t2 =>
 
138
        munion (contents t1) (munion (contents t2) (singletonBag a))
 
139
    end.
 
140
 
 
141
 
 
142
  (** equivalence of two trees is equality of corresponding multisets *)
 
143
  Definition equiv_Tree (t1 t2:Tree) := meq (contents t1) (contents t2).
 
144
 
 
145
 
 
146
 
 
147
  (** * From lists to sorted lists *)
 
148
 
 
149
  (** ** Specification of heap insertion *)
 
150
 
 
151
  Inductive insert_spec (a:A) (T:Tree) : Type :=
 
152
    insert_exist :
 
153
    forall T1:Tree,
 
154
      is_heap T1 ->
 
155
      meq (contents T1) (munion (contents T) (singletonBag a)) ->
 
156
      (forall b:A, leA b a -> leA_Tree b T -> leA_Tree b T1) ->
 
157
      insert_spec a T.
 
158
 
 
159
 
 
160
  Lemma insert : forall T:Tree, is_heap T -> forall a:A, insert_spec a T.
 
161
  Proof.
 
162
    simple induction 1; intros.
 
163
    apply insert_exist with (Tree_Node a Tree_Leaf Tree_Leaf);
 
164
      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
 
165
    simpl in |- *; unfold meq, munion in |- *; auto using node_is_heap with datatypes.
 
166
    elim (leA_dec a a0); intros.
 
167
    elim (X a0); intros.
 
168
    apply insert_exist with (Tree_Node a T2 T0);
 
169
      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
 
170
    simpl in |- *; apply treesort_twist1; trivial with datatypes. 
 
171
    elim (X a); intros T3 HeapT3 ConT3 LeA.
 
172
    apply insert_exist with (Tree_Node a0 T2 T3); 
 
173
      auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
 
174
    apply node_is_heap; auto using node_is_heap, nil_is_heap, leA_Tree_Leaf with datatypes.
 
175
    apply low_trans with a; auto with datatypes. 
 
176
    apply LeA; auto with datatypes.
 
177
    apply low_trans with a; auto with datatypes.
 
178
    simpl in |- *; apply treesort_twist2; trivial with datatypes. 
 
179
  Qed.
 
180
 
 
181
 
 
182
  (** ** Building a heap from a list *)
 
183
 
 
184
  Inductive build_heap (l:list A) : Type :=
 
185
    heap_exist :
 
186
    forall T:Tree,
 
187
      is_heap T ->
 
188
      meq (list_contents _ eqA_dec l) (contents T) -> build_heap l.
 
189
  
 
190
  Lemma list_to_heap : forall l:list A, build_heap l.
 
191
  Proof.
 
192
    simple induction l.
 
193
    apply (heap_exist nil Tree_Leaf); auto with datatypes.
 
194
    simpl in |- *; unfold meq in |- *; exact nil_is_heap.
 
195
    simple induction 1.
 
196
    intros T i m; elim (insert T i a).
 
197
    intros; apply heap_exist with T1; simpl in |- *; auto with datatypes.
 
198
    apply meq_trans with (munion (contents T) (singletonBag a)).
 
199
    apply meq_trans with (munion (singletonBag a) (contents T)).
 
200
    apply meq_right; trivial with datatypes.
 
201
    apply munion_comm.
 
202
    apply meq_sym; trivial with datatypes.
 
203
  Qed.
 
204
 
 
205
 
 
206
  (** ** Building the sorted list *)
 
207
  
 
208
  Inductive flat_spec (T:Tree) : Type :=
 
209
    flat_exist :
 
210
    forall l:list A,
 
211
      sort leA l ->
 
212
      (forall a:A, leA_Tree a T -> lelistA leA a l) ->
 
213
      meq (contents T) (list_contents _ eqA_dec l) -> flat_spec T.
 
214
 
 
215
  Lemma heap_to_list : forall T:Tree, is_heap T -> flat_spec T.
 
216
  Proof.
 
217
    intros T h; elim h; intros.
 
218
    apply flat_exist with (nil (A:=A)); auto with datatypes.
 
219
    elim X; intros l1 s1 i1 m1; elim X0; intros l2 s2 i2 m2.
 
220
    elim (merge _ leA_dec eqA_dec s1 s2); intros.
 
221
    apply flat_exist with (a :: l); simpl in |- *; auto with datatypes.
 
222
    apply meq_trans with
 
223
      (munion (list_contents _ eqA_dec l1)
 
224
        (munion (list_contents _ eqA_dec l2) (singletonBag a))).
 
225
    apply meq_congr; auto with datatypes.
 
226
    apply meq_trans with
 
227
      (munion (singletonBag a)
 
228
        (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2))).
 
229
    apply munion_rotate.
 
230
    apply meq_right; apply meq_sym; trivial with datatypes.
 
231
  Qed.
 
232
 
 
233
 
 
234
  (** * Specification of treesort *)
 
235
 
 
236
  Theorem treesort :
 
237
    forall l:list A, {m : list A | sort leA m &  permutation _ eqA_dec l m}.
 
238
  Proof.
 
239
    intro l; unfold permutation in |- *.
 
240
    elim (list_to_heap l).
 
241
    intros.
 
242
    elim (heap_to_list T); auto with datatypes.
 
243
    intros.
 
244
    exists l0; auto with datatypes.
 
245
    apply meq_trans with (contents T); trivial with datatypes.
 
246
  Qed.
 
247
 
 
248
End defs.
 
 
b'\\ No newline at end of file'