source: src/common/PositiveMap.ma @ 1562

Last change on this file since 1562 was 1562, checked in by mulligan, 10 years ago

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

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