source: src/common/PositiveMap.ma @ 2303

Last change on this file since 2303 was 2303, checked in by campbell, 8 years ago

Some preliminary checking of cost labelling properties in RTLabs.

File size: 10.9 KB
Line 
1include "basics/types.ma".
2include "utilities/binary/positive.ma".
3include "ASM/Util.ma". (* bool_to_Prop *)
4
5inductive positive_map (A:Type[0]) : Type[0] ≝
6| pm_leaf : positive_map A
7| pm_node : option A → positive_map A → positive_map A → positive_map A.
8
9let rec lookup_opt (A:Type[0]) (b:Pos) (t:positive_map A) on t : option A ≝
10match t with
11[ pm_leaf ⇒ None ?
12| pm_node a l r ⇒
13    match b with
14    [ one ⇒ a
15    | p0 tl ⇒ lookup_opt A tl l
16    | p1 tl ⇒ lookup_opt A tl r
17    ]
18].
19
20definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝ 
21 λA.λb.λt.λx.
22 match lookup_opt A b t with
23 [ None ⇒ x
24 | Some r ⇒ r
25 ].
26
27let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
28match b with
29[ one ⇒
30    match t with
31    [ pm_leaf ⇒ pm_node A (Some ? a) (pm_leaf A) (pm_leaf A)
32    | pm_node _ l r ⇒ pm_node A (Some ? a) l r
33    ]
34| p0 tl ⇒
35    match t with
36    [ pm_leaf ⇒ pm_node A (None ?) (insert A tl a (pm_leaf A)) (pm_leaf A)
37    | pm_node x l r ⇒ pm_node A x (insert A tl a l) r
38    ]
39| p1 tl ⇒
40    match t with
41    [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A))
42    | pm_node x l r ⇒ pm_node A x l (insert A tl a r)
43    ]
44].
45
46let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
47match b with
48[ one ⇒
49    match t with
50    [ pm_leaf ⇒ None ?
51    | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x
52    ]
53| p0 tl ⇒
54    match t with
55    [ pm_leaf ⇒ None ?
56    | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l)
57    ]
58| p1 tl ⇒
59    match t with
60    [ pm_leaf ⇒ None ?
61    | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r)
62    ]
63].
64
65lemma lookup_opt_insert_hit :
66 ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A.
67  lookup_opt … b (insert … b v t) = Some A v.
68#A #v #b elim b
69[ * //
70| #tl #IH *
71  [ whd in ⊢ (??%%); @IH
72  | #x #l #r @IH
73  ]
74| #tl #IH *
75  [ whd in ⊢ (??%%); @IH
76  | #x #l #r @IH
77  ]
78] qed.
79
80lemma lookup_insert_hit:
81  ∀a: Type[0].
82  ∀v: a.
83  ∀b: Pos.
84  ∀t: positive_map a.
85  ∀d: a.
86    lookup … b (insert … b v t) d = v.
87#A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit %
88qed.
89
90lemma lookup_opt_insert_miss:
91 ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A.
92  b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t.
93#A #v #b elim b
94[ * [ #t * #H elim (H (refl …))
95    | *: #c' #t #NE cases t //
96    ]
97| #b' #IH *
98  [ * [ #NE @refl | #x #l #r #NE @refl ]
99  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
100          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
101          ]
102  | #c' * //
103  ]
104| #b' #IH *
105  [ * [ #NE @refl | #x #l #r #NE @refl ]
106  | #c' * //
107  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
108          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
109          ]
110  ]
111] qed.
112
113let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
114 (t: positive_map A) (b: B) on t: B ≝
115match t with
116[ pm_leaf ⇒ b
117| pm_node a l r ⇒
118    let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in
119    let b ≝ fold A B (λx.f (p0 x)) l b in
120            fold A B (λx.f (p1 x)) r b
121].   
122
123lemma update_fail : ∀A,b,a,t.
124  update A b a t = None ? →
125  lookup_opt A b t = None ?.
126#A #b #a elim b
127[ * [ // | * // #x #l #r normalize #E destruct ]
128| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
129                   cases (update A b' a r) in U ⊢ %;
130                   [ // | normalize #t #E destruct ]
131            ]
132| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
133                   cases (update A b' a l) in U ⊢ %;
134                   [ // | normalize #t #E destruct ]
135            ]
136] qed.
137
138lemma update_lookup_opt_same : ∀A,b,a,t,t'.
139  update A b a t = Some ? t' →
140  lookup_opt A b t' = Some ? a.
141#A #b #a elim b
142[ * [ #t' normalize #E destruct
143    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
144      #E destruct //
145    ]
146| #b' #IH *
147  [ #t' normalize #E destruct
148  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
149    lapply (IH r)
150    cases (update A b' a r)
151    [ #_ normalize #E destruct
152    | #r' #H normalize #E destruct @H @refl
153    ]
154  ]
155| #b' #IH *
156  [ #t' normalize #E destruct
157  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
158    lapply (IH l)
159    cases (update A b' a l)
160    [ #_ normalize #E destruct
161    | #r' #H normalize #E destruct @H @refl
162    ]
163  ]
164] qed.
165
166lemma update_lookup_opt_other : ∀A,b,a,t,t'.
167  update A b a t = Some ? t' →
168  ∀b'. b ≠ b' →
169  lookup_opt A b' t = lookup_opt A b' t'.
170#A #b #a elim b
171[ * [ #t' normalize #E destruct
172    | * [2: #x] #l #r #t' normalize #E destruct
173      * [ * #H elim (H (refl …)) ]
174      #tl #NE normalize //
175    ]
176| #b' #IH *
177  [ #t' normalize #E destruct
178  | #x #l #r #t' normalize
179    lapply (IH r)
180    cases (update A b' a r)
181    [ #_ normalize #E destruct
182    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
183    ]
184  ]
185| #b' #IH *
186  [ #t' normalize #E destruct
187  | #x #l #r #t' normalize
188    lapply (IH l)
189    cases (update A b' a l)
190    [ #_ normalize #E destruct
191    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
192    ]
193  ]
194] qed.
195
196include "utilities/option.ma".
197
198let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
199match b with
200[ pm_leaf ⇒ pm_leaf ?
201| pm_node a l r ⇒ pm_node ? (a »= f)
202    (map_opt ?? f l)
203    (map_opt ?? f r)
204].
205
206definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
207
208lemma lookup_opt_map : ∀A,B,f,b,p.
209  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
210#A#B#f#b elim b [//]
211#a #l #r #Hil #Hir * [//]
212#p
213whd in ⊢ (??(???%)(????%?));
214whd in ⊢ (??%?); //
215qed.
216
217lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
218#A #m #f #Hf elim m [//]
219* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
220qed.
221
222lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
223#A #m @map_opt_id_eq_ext //
224qed.
225
226let rec merge A B C (choice : option A → option B → option C)
227  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
228match a with
229[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
230| pm_node o l r ⇒
231  match b with
232  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
233  | pm_node o' l' r' ⇒
234    pm_node ? (choice o o')
235      (merge … choice l l')
236      (merge … choice r r')
237  ]
238].
239
240lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
241  choice (None ?) (None ?) = None ? →
242  lookup_opt … p (merge A B C choice a b) =
243    choice (lookup_opt … p a) (lookup_opt … p b).
244 #A#B#C#choice#a elim a
245[ normalize #b
246| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
247]
248#p#choice_good >lookup_opt_map
249elim (lookup_opt ???)
250normalize //
251qed.
252
253let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
254match b with
255[ pm_leaf ⇒ 0
256| pm_node a l r ⇒
257  (match a with
258   [ Some _ ⇒ 1
259   | None ⇒ 0
260   ]) + domain_size A l + domain_size A r
261].
262
263(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
264include "basics/lists/list.ma".
265interpretation "positive map size" 'norm p = (domain_size ? p).
266
267lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
268#A#B#f#b elim b [//]
269*[2:#x]#l#r#Hil#Hir normalize
270[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
271@le_plus assumption
272qed.
273
274lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
275#A#B#f#b elim b [//]
276*[2:#x]#l#r#Hil#Hir normalize
277>Hil >Hir @refl
278qed.
279
280lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
281#A#m elim m
282[#p normalize #F elim (absurd ? (refl ??) F)
283|* [2: #x]  #l #r #Hil #Hir * normalize
284  [1,2,3: //
285  |4:  #F elim (absurd ? (refl ??) F)]
286  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
287qed.
288
289lemma insert_size : ∀A,p,a,m. |insert A p a m| =
290  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
291#A#p elim p
292[ #a * [2: * [2: #x] #l #r] normalize //
293|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
294] qed.
295
296(* Testing all of the entries with a boolean predicate, where the predicate
297   is given a proof that the entry is in the map. *)
298
299let rec pm_all_aux (A:Type[0]) (m,t:positive_map A) (pre:Pos → Pos) on t : (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool ≝
300match t return λt. (∀p. lookup_opt A (pre p) m = lookup_opt A p t) → (∀p,a.lookup_opt A p m = Some A a → bool) → bool with
301[ pm_leaf ⇒ λ_.λ_. true
302| pm_node a l r ⇒ λH,f.
303    pm_all_aux A m l (λx. pre (p0 x)) ? f ∧
304    ((match a return λa. (∀p. ? = lookup_opt A p (pm_node ? a ??)) → ? with [ None ⇒ λ_. true | Some a' ⇒ λH. f (pre one) a' ? ]) H) ∧
305    pm_all_aux A m r (λx. pre (p1 x)) ? f
306].
307[ >H %
308| #p >H %
309| #p >H %
310] qed.
311
312definition pm_all : ∀A. ∀m:positive_map A. (∀p,a. lookup_opt A p m = Some A a → bool) → bool ≝
313λA,m,f. pm_all_aux A m m (λx.x) (λp. refl ??) f.
314
315(* Proof irrelevance doesn't seem to apply to arbitrary variables, but we can
316   use the function graph to show that it's fine. *)
317   
318inductive pm_all_pred_graph : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. bool → Prop ≝
319| pmallpg : ∀A,m,p,a,L. ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool. pm_all_pred_graph A m p a L f (f p a L).
320
321lemma pm_all_pred_irr : ∀A,m,p,a,L,L'.
322 ∀f:∀p:Pos.∀a:A.lookup_opt A p m=Some A a→bool.
323 f p a L = f p a L'.
324#A #m #p #a #L #L' #f
325cut (pm_all_pred_graph A m p a L f (f p a L)) [ % ]
326cases (f p a L) #H cut (pm_all_pred_graph A m p a L' f ?) [2,5: @H | 1,4: skip]
327* //
328qed.
329
330lemma pm_all_aux_ok_aux : ∀A,m,t,pre,H,f,a,L.
331  pm_all_aux A m t pre H f →
332  lookup_opt A one t = Some A a →
333  f (pre one) a L.
334#A #m *
335[ #pre #H #f #a #L #H #L' normalize in L'; destruct
336| * [ #l #r #pre #H #f #a #L #H' #L' normalize in L'; destruct
337    | #a' #l #r #pre #H #f #a #L #AUX #L' normalize in L'; destruct
338      cases (andb_Prop_true … AUX) #AUX' cases (andb_Prop_true … AUX')
339      #_ #HERE #_ whd in HERE:(?%); @eq_true_to_b <HERE @pm_all_pred_irr
340    ]
341] qed.
342
343lemma pm_all_aux_ok : ∀A,m,t,pre,H,f.
344  bool_to_Prop (pm_all_aux A m t pre H f) ↔ (∀p,a,H. f (pre p) a H).
345#A #m #t #pre #H #f %
346[ #H' #p generalize in match pre in H H' ⊢ %; -pre generalize in match t; elim p
347  [ #t #pre #H #H' #a #L lapply (refl ? (Some A a)) <L in ⊢ (??%? → ?); >H @pm_all_aux_ok_aux //
348  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
349             | #x #l #r #pre #H #H' #a #L @(IH r)
350               [ #x >H % | cases (andb_Prop_true … H') #_ // ]
351             ]
352  | #q #IH * [ #pre #H #H' #a #L @⊥ >H in L; normalize #E destruct
353             | #x #l #r #pre #H #H' #a #L @(IH l)
354               [ #x >H % | cases (andb_Prop_true … H') #H'' cases (andb_Prop_true … H'') // ]
355             ]
356  ]
357| #H' generalize in match pre in H H' ⊢ %; -pre elim t
358  [ //
359  | * [2:#x] #l #r #IHl #IHr #pre #H #H' @andb_Prop
360    [ 1,3: @andb_Prop
361      [ 1,3: @IHl //
362      | @(H' one x)
363      | %
364      ]
365    | 2,4: @IHr //
366    ]
367  ]
368] qed.
369
370lemma pm_all_ok : ∀A,m,f.
371  bool_to_Prop (pm_all A m f) ↔ (∀p,a,H. f p a H).
372#A #m #f @pm_all_aux_ok
373qed.
374
Note: See TracBrowser for help on using the repository browser.