source: src/common/PositiveMap.ma @ 1651

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

Files ported to new version of the standard library.

File size: 5.1 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
79axiom 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
87lemma lookup_opt_insert_miss:
88 ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A.
89  b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t.
90#A #v #b elim b
91[ * [ #t * #H elim (H (refl …))
92    | *: #c' #t #NE cases t //
93    ]
94| #b' #IH *
95  [ * [ #NE @refl | #x #l #r #NE @refl ]
96  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
97          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
98          ]
99  | #c' * //
100  ]
101| #b' #IH *
102  [ * [ #NE @refl | #x #l #r #NE @refl ]
103  | #c' * //
104  | #c' * [ #NE whd in ⊢ (??%%); @IH /2/
105          | #x #l #r #NE whd in ⊢ (??%%); @IH /2/
106          ]
107  ]
108] qed.
109
110let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
111 (t: positive_map A) (b: B) on t: B ≝
112match t with
113[ pm_leaf ⇒ b
114| pm_node a l r ⇒
115    let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in
116    let b ≝ fold A B (λx.f (p0 x)) l b in
117            fold A B (λx.f (p1 x)) r b
118].   
119
120lemma update_fail : ∀A,b,a,t.
121  update A b a t = None ? →
122  lookup_opt A b t = None ?.
123#A #b #a elim b
124[ * [ // | * // #x #l #r normalize #E destruct ]
125| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
126                   cases (update A b' a r) in U ⊢ %;
127                   [ // | normalize #t #E destruct ]
128            ]
129| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
130                   cases (update A b' a l) in U ⊢ %;
131                   [ // | normalize #t #E destruct ]
132            ]
133] qed.
134
135lemma update_lookup_opt_same : ∀A,b,a,t,t'.
136  update A b a t = Some ? t' →
137  lookup_opt A b t' = Some ? a.
138#A #b #a elim b
139[ * [ #t' normalize #E destruct
140    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?);
141      #E destruct //
142    ]
143| #b' #IH *
144  [ #t' normalize #E destruct
145  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
146    lapply (IH r)
147    cases (update A b' a r)
148    [ #_ normalize #E destruct
149    | #r' #H normalize #E destruct @H @refl
150    ]
151  ]
152| #b' #IH *
153  [ #t' normalize #E destruct
154  | #x #l #r #t' whd in ⊢ (??%? → ??%?);
155    lapply (IH l)
156    cases (update A b' a l)
157    [ #_ normalize #E destruct
158    | #r' #H normalize #E destruct @H @refl
159    ]
160  ]
161] qed.
162
163lemma update_lookup_opt_other : ∀A,b,a,t,t'.
164  update A b a t = Some ? t' →
165  ∀b'. b ≠ b' →
166  lookup_opt A b' t = lookup_opt A b' t'.
167#A #b #a elim b
168[ * [ #t' normalize #E destruct
169    | * [2: #x] #l #r #t' normalize #E destruct
170      * [ * #H elim (H (refl …)) ]
171      #tl #NE normalize //
172    ]
173| #b' #IH *
174  [ #t' normalize #E destruct
175  | #x #l #r #t' normalize
176    lapply (IH r)
177    cases (update A b' a r)
178    [ #_ normalize #E destruct
179    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
180    ]
181  ]
182| #b' #IH *
183  [ #t' normalize #E destruct
184  | #x #l #r #t' normalize
185    lapply (IH l)
186    cases (update A b' a l)
187    [ #_ normalize #E destruct
188    | #t'' #H normalize #E destruct * // #b'' #NE @H /2/
189    ]
190  ]
191] qed.
192
193let rec merge (A: Type[0]) (b: positive_map A) (c:positive_map A) on b: positive_map A ≝
194match b with
195[ pm_leaf ⇒ c
196| pm_node a l r ⇒
197  match c with
198  [ pm_leaf ⇒ pm_node A a l r
199  | pm_node a' l' r' ⇒ pm_node A a' (merge A l l') (merge A r r')
200  ]
201].
202
Note: See TracBrowser for help on using the repository browser.