source: src/common/PositiveMap.ma @ 1555

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