source: src/utilities/adt/table_adt.ma @ 1599

Last change on this file since 1599 was 1599, checked in by sacerdot, 8 years ago

Start of merging of stuff into the standard library of Matita.

File size: 9.8 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/lists/list.ma".
4
5include "arithmetics/nat.ma".
6
7include "utilities/adt/equal.ma".
8include "utilities/adt/ordering.ma".
9
10include "ASM/Util.ma".
11
12inductive table (dom_type: Type[0]) (rng_type: Type[0]): Type[0] ≝
13  | empty: table dom_type rng_type
14  | node : nat → dom_type → rng_type → table dom_type rng_type → table dom_type rng_type → table dom_type rng_type.
15
16definition tbl_height ≝
17  λdom_type : Type[0].
18  λrng_type : Type[0].
19  λthe_table: table dom_type rng_type.
20  match the_table with
21  [ empty ⇒ 0
22  | node sz key val l r ⇒ sz
23  ].
24
25let rec tbl_size
26  (dom_type : Type[0]) (rng_type : Type[0]) (the_table: table dom_type rng_type)
27    on the_table: nat ≝
28  match the_table with
29  [ empty ⇒ 0
30  | node sz key val l r ⇒ S (tbl_size … l) + (tbl_size … r)
31  ].
32 
33definition tbl_empty ≝
34  λdom_type: Type[0].
35  λrng_type: Type[0].
36    empty dom_type rng_type.
37
38definition tbl_is_empty ≝
39  λdom_type: Type[0].
40  λrng_type: Type[0].
41  λthe_table: table dom_type rng_type.
42  match the_table with
43  [ empty ⇒ true
44  | _     ⇒ false
45  ].
46
47definition tbl_is_empty_p ≝
48  λdom_type: Type[0].
49  λrng_type: Type[0].
50  λthe_table: table dom_type rng_type.
51  match the_table with
52  [ empty ⇒ True
53  | _     ⇒ False
54  ].
55
56let rec tbl_to_list
57  (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type)
58    on the_table: list (dom_type × rng_type) ≝
59  match the_table with
60  [ empty ⇒ [ ]
61  | node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r
62  ].
63
64let rec tbl_min_binding
65  (key_type: Type[0]) (rng_type: Type[0]) (the_table: table key_type rng_type)
66    (proof: ¬ (tbl_is_empty_p … the_table))
67      on the_table: key_type × rng_type ≝
68  match the_table return λx. ¬ (tbl_is_empty_p … x) → key_type × rng_type with
69  [ empty               ⇒ λabsurd. ?
70  | node sz key val l r ⇒ λproof.
71    match l return λx. x = l → key_type × rng_type with
72    [ empty ⇒ λproof. 〈key, val〉
73    | _     ⇒ λproof. tbl_min_binding key_type rng_type l ?
74    ] (refl … l)
75  ] proof.
76  [1: normalize in absurd;
77      elim absurd;
78      #ABSURD
79      @⊥ @ABSURD @I
80  |2: <proof
81      normalize
82      /2/
83  ]
84qed.
85
86definition tbl_create ≝
87  λkey_type: Type[0].
88  λrng_type: Type[0].
89  λleft    : table key_type rng_type.
90  λkey     : key_type.
91  λval     : rng_type.
92  λright   : table key_type rng_type.
93  let hl ≝ tbl_height … left in
94  let hr ≝ tbl_height … right in
95  let height ≝ if gtb hl hr then hl + 1 else hr + 1 in
96    node key_type rng_type height key val left right.
97     
98let rec tbl_balance
99  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
100    (left: table key_type rng_type) (key: key_type) (val: rng_type)
101      (right: table key_type rng_type) (left_proof: ¬ (tbl_is_empty_p … left))
102        (right_proof: ¬ (tbl_is_empty_p … right))
103          on left: table key_type rng_type ≝
104  match gtb (tbl_height … left) ((tbl_height … right) + 2) with
105  [ true  ⇒
106    match left return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
107    [ empty              ⇒ λabsurd. ?
108    | node _ lv ld ll lr ⇒ λnon_empty_proof.
109      if gtb (tbl_height … ll) (tbl_height … lr) then
110        tbl_create … ll lv ld (tbl_create … lr key val right)
111      else
112        match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
113        [ empty ⇒ λabsurd. ?
114        | node _ lrv lrd lrl lrr ⇒ λnon_empty_proof.
115            tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right)
116        ] ?
117    ] left_proof
118  | false ⇒ ?
119  ].
120  [1: normalize in absurd;
121      elim absurd
122      #ABSURD
123      @⊥ @ABSURD @I
124  |3: normalize in absurd;
125      elim absurd
126      #ABSURD
127      @⊥ @ABSURD @I
128  |*: cases daemon
129  ]
130qed.
131 
132let rec tbl_remove_min_binding
133  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
134    (the_table: table key_type rng_type) (proof: ¬ (tbl_is_empty_p … the_table))
135      on the_table: table key_type rng_type ≝
136  match the_table return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
137  [ empty               ⇒ λabsurd. ?
138  | node sz key val l r ⇒ λproof.
139    match l return λx. x = l → table key_type rng_type with
140    [ empty ⇒ λproof. r
141    | _     ⇒ λproof. tbl_balance … ord (tbl_remove_min_binding … ord l ?) key val r
142    ] (refl … l)
143  ] proof.
144  [1: normalize in absurd;
145      elim absurd;
146      #ABSURD
147      @⊥ @ABSURD @I
148  |2: <proof
149      normalize
150      @nmk //
151  ]
152qed.
153   
154let rec tbl_insert
155  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
156    (key: key_type) (val: rng_type) (the_table: table key_type rng_type)
157      on the_table: table key_type rng_type ≝
158  match the_table with
159  [ empty                 ⇒ node … 1 key val (empty …) (empty …)
160  | node sz key' val' l r ⇒
161    match ord key key' with
162    [ order_lt ⇒ tbl_balance … ord (tbl_insert … ord key val l) key' val' r
163    | order_eq ⇒ node … sz key val l r
164    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_insert … ord key val r)
165    ]
166  ].
167 
168let rec tbl_merge
169  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
170    (left: table dom_type rng_type) (right: table dom_type rng_type)
171      on left: table dom_type rng_type ≝
172  match left with
173  [ empty ⇒ right
174  | _     ⇒
175    match right return λx. x = right → table dom_type rng_type with
176    [ empty               ⇒ λid_proof. left
177    | node sz key val l r ⇒ λid_proof.
178      let 〈x, d〉 ≝ tbl_min_binding dom_type rng_type right ? in
179        tbl_balance … ord left x d (tbl_remove_min_binding … ord right ?)
180    ] (refl … right)
181  ].
182  <id_proof
183  normalize /2/
184qed.
185
186let rec tbl_remove
187  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
188    (key: key_type) (the_table: table key_type rng_type)
189      on the_table: table key_type rng_type ≝
190  match the_table with
191  [ empty                 ⇒ empty …
192  | node sz key' val' l r ⇒
193    match ord key key' with
194    [ order_lt ⇒ tbl_balance … ord (tbl_remove … ord key l) key' val' r
195    | order_eq ⇒ tbl_merge … ord l r
196    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_remove … ord key r)
197    ]
198  ].
199 
200let rec tbl_find
201  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
202    (to_find: dom_type) (the_table: table dom_type rng_type)
203      on the_table: option rng_type ≝
204  match the_table with
205  [ empty               ⇒ None …
206  | node sz key val l r ⇒
207    match ord to_find key with
208    [ order_lt ⇒ tbl_find … ord to_find l
209    | order_eq ⇒ Some … val
210    | order_gt ⇒ tbl_find … ord to_find r
211    ]
212  ].
213
214let rec tbl_update
215  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
216    (to_find: dom_type) (update: rng_type → rng_type)
217      (the_table: table dom_type rng_type)
218        on the_table: table dom_type rng_type ≝
219  match the_table with
220  [ empty               ⇒ empty …
221  | node sz key val l r ⇒
222    match ord to_find key with
223    [ order_lt ⇒ tbl_update … ord to_find update l
224    | order_eq ⇒ node … sz key (update val) l r
225    | order_gt ⇒ tbl_update … ord to_find update r
226    ]
227  ].
228
229let rec tbl_forall
230  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
231    (the_table: table dom_type rng_type)
232      on the_table: bool ≝
233  match the_table with
234  [ empty               ⇒ true
235  | node sz key val l r ⇒ f val ∧ tbl_forall … f l ∧ tbl_forall … f r
236  ].
237 
238let rec tbl_exists
239  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
240    (the_table: table dom_type rng_type)
241      on the_table: bool ≝
242  match the_table with
243  [ empty               ⇒ false
244  | node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r
245  ].
246     
247axiom tbl_equal:
248  ∀key_type, rng_type.
249    (key_type → key_type → order) → (rng_type → rng_type → order) →
250      table key_type rng_type → table key_type rng_type → bool.
251
252let rec tbl_mapi
253  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: dom_type → rng_type → a)
254    (the_table: table dom_type rng_type)
255      on the_table: table dom_type a ≝
256  match the_table with
257  [ empty               ⇒ empty …
258  | node sz key val l r ⇒ node  … sz key (f key val) (tbl_mapi … f l) (tbl_mapi … f r)
259  ].
260
261let rec tbl_map
262  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: rng_type → a)
263    (the_table: table dom_type rng_type)
264      on the_table: table dom_type a ≝
265  match the_table with
266  [ empty               ⇒ empty …
267  | node sz key val l r ⇒ node  … sz key (f val) (tbl_map … f l) (tbl_map … f r)
268  ].
269
270let rec tbl_fold
271  (dom_type: Type[0]) (a: Type[0]) (b: Type[0]) (f: dom_type → a → b → b)
272    (the_table: table dom_type a) (seed: b)
273      on the_table: b ≝
274  match the_table with
275  [ empty               ⇒ seed
276  | node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed))
277  ].
278
279definition tbl_singleton ≝
280  λkey_type : Type[0].
281  λrng_type : Type[0].
282  λkey      : key_type.
283  λrng      : rng_type.
284    node key_type rng_type 1 key rng (empty …) (empty …).
285
286definition tbl_from_list ≝
287  λkey_type : Type[0].
288  λrng_type : Type[0].
289  λord      : key_type → key_type → order.
290  λthe_list : list (key_type × rng_type).
291    foldr … (λkey_rng.
292      let 〈key, rng〉 ≝ key_rng in
293        tbl_insert … ord key rng) (tbl_empty …) the_list.
294
295definition tbl_filter ≝
296  λdom_type : Type[0].
297  λrng_type : Type[0].
298  λord      : dom_type → dom_type → order.
299  λf        : rng_type → bool.
300  λthe_table: table dom_type rng_type.
301  let as_list  ≝ tbl_to_list … the_table in
302  let filtered ≝ filter … (λx. f (\snd x)) as_list in
303    tbl_from_list … ord filtered.
304
Note: See TracBrowser for help on using the repository browser.