source: src/common/PositiveMap.ma @ 2104

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

Fill in misc axiom.

File size: 7.7 KB
Line 
1include "basics/types.ma".
2include "utilities/binary/positive.ma".
3
4inductive positive_map (A:Type[0]) : Type[0] ≝
5| pm_leaf : positive_map A
6| pm_node : option A → positive_map A → positive_map A → positive_map A.
7
8let rec lookup_opt (A:Type[0]) (b:Pos) (t:positive_map A) on t : option A ≝
9match t with
10[ pm_leaf ⇒ None ?
11| pm_node a l r ⇒
12    match b with
13    [ one ⇒ a
14    | p0 tl ⇒ lookup_opt A tl l
15    | p1 tl ⇒ lookup_opt A tl r
16    ]
17].
18
19definition lookup: ∀A:Type[0].Pos → positive_map A → A → A ≝ 
20 λA.λb.λt.λx.
21 match lookup_opt A b t with
22 [ None ⇒ x
23 | Some r ⇒ r
24 ].
25
26let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
27match b with
28[ one ⇒
29    match t with
30    [ pm_leaf ⇒ pm_node A (Some ? a) (pm_leaf A) (pm_leaf A)
31    | pm_node _ l r ⇒ pm_node A (Some ? a) l r
32    ]
33| p0 tl ⇒
34    match t with
35    [ pm_leaf ⇒ pm_node A (None ?) (insert A tl a (pm_leaf A)) (pm_leaf A)
36    | pm_node x l r ⇒ pm_node A x (insert A tl a l) r
37    ]
38| p1 tl ⇒
39    match t with
40    [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A))
41    | pm_node x l r ⇒ pm_node A x l (insert A tl a r)
42    ]
43].
44
45let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
46match b with
47[ one ⇒
48    match t with
49    [ pm_leaf ⇒ None ?
50    | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x
51    ]
52| p0 tl ⇒
53    match t with
54    [ pm_leaf ⇒ None ?
55    | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l)
56    ]
57| p1 tl ⇒
58    match t with
59    [ pm_leaf ⇒ None ?
60    | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r)
61    ]
62].
63
64lemma lookup_opt_insert_hit :
65 ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A.
66  lookup_opt … b (insert … b v t) = Some A v.
67#A #v #b elim b
68[ * //
69| #tl #IH *
70  [ whd in ⊢ (??%%); @IH
71  | #x #l #r @IH
72  ]
73| #tl #IH *
74  [ whd in ⊢ (??%%); @IH
75  | #x #l #r @IH
76  ]
77] qed.
78
79lemma lookup_insert_hit:
80  ∀a: Type[0].
81  ∀v: a.
82  ∀b: Pos.
83  ∀t: positive_map a.
84  ∀d: a.
85    lookup … b (insert … b v t) d = v.
86#A #v #b #t #d whd in ⊢ (??%?); >lookup_opt_insert_hit %
87qed.
88
89lemma lookup_opt_insert_miss:
90 ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A.
91  b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t.
92#A #v #b elim b
93[ * [ #t * #H elim (H (refl …))
94    | *: #c' #t #NE cases t //
95    ]
96| #b' #IH *
97  [ * [ #NE @refl | #x #l #r #NE @refl ]
98  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
99          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
100          ]
101  | #c' * //
102  ]
103| #b' #IH *
104  [ * [ #NE @refl | #x #l #r #NE @refl ]
105  | #c' * //
106  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
107          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
108          ]
109  ]
110] qed.
111
112let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
113 (t: positive_map A) (b: B) on t: B ≝
114match t with
115[ pm_leaf ⇒ b
116| pm_node a l r ⇒
117    let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in
118    let b ≝ fold A B (λx.f (p0 x)) l b in
119            fold A B (λx.f (p1 x)) r b
120].   
121
122lemma update_fail : ∀A,b,a,t.
123  update A b a t = None ? →
124  lookup_opt A b t = None ?.
125#A #b #a elim b
126[ * [ // | * // #x #l #r normalize #E destruct ]
127| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
128                   cases (update A b' a r) in U ⊢ %;
129                   [ // | normalize #t #E destruct ]
130            ]
131| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
132                   cases (update A b' a l) in U ⊢ %;
133                   [ // | normalize #t #E destruct ]
134            ]
135] qed.
136
137lemma update_lookup_opt_same : ∀A,b,a,t,t'.
138  update A b a t = Some ? t' →
139  lookup_opt A b t' = Some ? a.
140#A #b #a elim b
141[ * [ #t' normalize #E destruct
142    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
143      #E destruct //
144    ]
145| #b' #IH *
146  [ #t' normalize #E destruct
147  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
148    lapply (IH r)
149    cases (update A b' a r)
150    [ #_ normalize #E destruct
151    | #r' #H normalize #E destruct @H @refl
152    ]
153  ]
154| #b' #IH *
155  [ #t' normalize #E destruct
156  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
157    lapply (IH l)
158    cases (update A b' a l)
159    [ #_ normalize #E destruct
160    | #r' #H normalize #E destruct @H @refl
161    ]
162  ]
163] qed.
164
165lemma update_lookup_opt_other : ∀A,b,a,t,t'.
166  update A b a t = Some ? t' →
167  ∀b'. b ≠ b' →
168  lookup_opt A b' t = lookup_opt A b' t'.
169#A #b #a elim b
170[ * [ #t' normalize #E destruct
171    | * [2: #x] #l #r #t' normalize #E destruct
172      * [ * #H elim (H (refl …)) ]
173      #tl #NE normalize //
174    ]
175| #b' #IH *
176  [ #t' normalize #E destruct
177  | #x #l #r #t' normalize
178    lapply (IH r)
179    cases (update A b' a r)
180    [ #_ normalize #E destruct
181    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
182    ]
183  ]
184| #b' #IH *
185  [ #t' normalize #E destruct
186  | #x #l #r #t' normalize
187    lapply (IH l)
188    cases (update A b' a l)
189    [ #_ normalize #E destruct
190    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
191    ]
192  ]
193] qed.
194
195include "utilities/option.ma".
196
197let rec map_opt A B (f : A → option B) (b : positive_map A) on b : positive_map B ≝
198match b with
199[ pm_leaf ⇒ pm_leaf ?
200| pm_node a l r ⇒ pm_node ? (a »= f)
201    (map_opt ?? f l)
202    (map_opt ?? f r)
203].
204
205definition map ≝ λA,B,f.map_opt A B (λx. Some ? (f x)).
206
207lemma lookup_opt_map : ∀A,B,f,b,p.
208  lookup_opt … p (map_opt A B f b) = ! x ← lookup_opt … p b ; f x.
209#A#B#f#b elim b [//]
210#a #l #r #Hil #Hir * [//]
211#p
212whd in ⊢ (??(???%)(????%?));
213whd in ⊢ (??%?); //
214qed.
215
216lemma map_opt_id_eq_ext : ∀A,m,f.(∀x.f x = Some ? x) → map_opt A A f m = m.
217#A #m #f #Hf elim m [//]
218* [2:#x] #l #r #Hil #Hir normalize [>Hf] //
219qed.
220
221lemma map_opt_id : ∀A,m.map_opt A A (λx. Some ? x) m = m.
222#A #m @map_opt_id_eq_ext //
223qed.
224
225let rec merge A B C (choice : option A → option B → option C)
226  (a : positive_map A) (b : positive_map B) on a : positive_map C ≝
227match a with
228[ pm_leaf ⇒ map_opt ?? (λx.choice (None ?) (Some ? x)) b
229| pm_node o l r ⇒
230  match b with
231  [ pm_leaf ⇒ map_opt ?? (λx.choice (Some ? x) (None ?)) a
232  | pm_node o' l' r' ⇒
233    pm_node ? (choice o o')
234      (merge … choice l l')
235      (merge … choice r r')
236  ]
237].
238
239lemma lookup_opt_merge : ∀A,B,C,choice,a,b,p.
240  choice (None ?) (None ?) = None ? →
241  lookup_opt … p (merge A B C choice a b) =
242    choice (lookup_opt … p a) (lookup_opt … p b).
243 #A#B#C#choice#a elim a
244[ normalize #b
245| #o#l#r#Hil#Hir * [2: #o'#l'#r' * normalize /2 by /]
246]
247#p#choice_good >lookup_opt_map
248elim (lookup_opt ???)
249normalize //
250qed.
251
252let rec domain_size (A : Type[0]) (b : positive_map A) on b : ℕ ≝
253match b with
254[ pm_leaf ⇒ 0
255| pm_node a l r ⇒
256  (match a with
257   [ Some _ ⇒ 1
258   | None ⇒ 0
259   ]) + domain_size A l + domain_size A r
260].
261
262(* just to load notation for 'norm (list.ma's notation overrides core's 'card)*)
263include "basics/lists/list.ma".
264interpretation "positive map size" 'norm p = (domain_size ? p).
265
266lemma map_opt_size : ∀A,B,f,b.|map_opt A B f b| ≤ |b|.
267#A#B#f#b elim b [//]
268*[2:#x]#l#r#Hil#Hir normalize
269[elim (f ?) normalize [@(transitive_le ? ? ? ? (le_n_Sn ?)) | #y @le_S_S ] ]
270@le_plus assumption
271qed.
272
273lemma map_size : ∀A,B,f,b.|map A B f b| = |b|.
274#A#B#f#b elim b [//]
275*[2:#x]#l#r#Hil#Hir normalize
276>Hil >Hir @refl
277qed.
278
279lemma lookup_opt_O_lt_size : ∀A,m,p. lookup_opt A p m ≠ None ? → 0 < |m|.
280#A#m elim m
281[#p normalize #F elim (absurd ? (refl ??) F)
282|* [2: #x]  #l #r #Hil #Hir * normalize
283  [1,2,3: //
284  |4:  #F elim (absurd ? (refl ??) F)]
285  #p #H [@(transitive_le … (Hir ? H)) | @(transitive_le … (Hil ? H))] //
286qed.
287
288lemma insert_size : ∀A,p,a,m. |insert A p a m| =
289  (match lookup_opt … p m with [Some _ ⇒ 0 | None ⇒ 1]) + |m|.
290#A#p elim p
291[ #a * [2: * [2: #x] #l #r] normalize //
292|*: #p #Hi #a * [2,4: * [2,4: #x] #l #r] normalize >Hi //
293] qed.
Note: See TracBrowser for help on using the repository browser.