source: src/common/PositiveMap.ma @ 1515

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

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 4.9 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
20let rec insert (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : positive_map A ≝
21match b with
22[ one ⇒
23    match t with
24    [ pm_leaf ⇒ pm_node A (Some ? a) (pm_leaf A) (pm_leaf A)
25    | pm_node _ l r ⇒ pm_node A (Some ? a) l r
26    ]
27| p0 tl ⇒
28    match t with
29    [ pm_leaf ⇒ pm_node A (None ?) (insert A tl a (pm_leaf A)) (pm_leaf A)
30    | pm_node x l r ⇒ pm_node A x (insert A tl a l) r
31    ]
32| p1 tl ⇒
33    match t with
34    [ pm_leaf ⇒ pm_node A (None ?) (pm_leaf A) (insert A tl a (pm_leaf A))
35    | pm_node x l r ⇒ pm_node A x l (insert A tl a r)
36    ]
37].
38
39let rec update (A:Type[0]) (b:Pos) (a:A) (t:positive_map A) on b : option (positive_map A) ≝
40match b with
41[ one ⇒
42    match t with
43    [ pm_leaf ⇒ None ?
44    | pm_node x l r ⇒ option_map ?? (λ_. pm_node A (Some ? a) l r) x
45    ]
46| p0 tl ⇒
47    match t with
48    [ pm_leaf ⇒ None ?
49    | pm_node x l r ⇒ option_map ?? (λl. pm_node A x l r) (update A tl a l)
50    ]
51| p1 tl ⇒
52    match t with
53    [ pm_leaf ⇒ None ?
54    | pm_node x l r ⇒ option_map ?? (λr. pm_node A x l r) (update A tl a r)
55    ]
56].
57
58lemma lookup_opt_insert_hit :
59 ∀A:Type[0].∀v:A.∀b:Pos.∀t:positive_map A.
60  lookup_opt … b (insert … b v t) = Some A v.
61#A #v #b elim b
62[ * //
63| #tl #IH *
64  [ whd in ⊢ (??%%) @IH
65  | #x #l #r @IH
66  ]
67| #tl #IH *
68  [ whd in ⊢ (??%%) @IH
69  | #x #l #r @IH
70  ]
71] qed.
72
73lemma lookup_opt_insert_miss:
74 ∀A:Type[0].∀v:A.∀b,c:Pos.∀t:positive_map A.
75  b ≠ c → lookup_opt … b (insert … c v t) = lookup_opt … b t.
76#A #v #b elim b
77[ * [ #t * #H elim (H (refl …))
78    | *: #c' #t #NE cases t //
79    ]
80| #b' #IH *
81  [ * [ #NE @refl | #x #l #r #NE @refl ]
82  | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
83          | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
84          ]
85  | #c' * //
86  ]
87| #b' #IH *
88  [ * [ #NE @refl | #x #l #r #NE @refl ]
89  | #c' * //
90  | #c' * [ #NE whd in ⊢ (??%%) @IH /2/
91          | #x #l #r #NE whd in ⊢ (??%%) @IH /2/
92          ]
93  ]
94] qed.
95
96let rec fold (A, B: Type[0]) (f: Pos → A → B → B)
97 (t: positive_map A) (b: B) on t: B ≝
98match t with
99[ pm_leaf ⇒ b
100| pm_node a l r ⇒
101    let b ≝ match a with [ None ⇒ b | Some a ⇒ f one a b ] in
102    let b ≝ fold A B (λx.f (p0 x)) l b in
103            fold A B (λx.f (p1 x)) r b
104].   
105
106lemma update_fail : ∀A,b,a,t.
107  update A b a t = None ? →
108  lookup_opt A b t = None ?.
109#A #b #a elim b
110[ * [ // | * // #x #l #r normalize #E destruct ]
111| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
112                   cases (update A b' a r) in U ⊢ %
113                   [ // | normalize #t #E destruct ]
114            ]
115| #b' #IH * [ // | #x #l #r #U @IH whd in U:(??%?);
116                   cases (update A b' a l) in U ⊢ %
117                   [ // | normalize #t #E destruct ]
118            ]
119] qed.
120
121lemma update_lookup_opt_same : ∀A,b,a,t,t'.
122  update A b a t = Some ? t' →
123  lookup_opt A b t' = Some ? a.
124#A #b #a elim b
125[ * [ #t' normalize #E destruct
126    | * [ 2: #x ] #l #r #t' whd in ⊢ (??%? → ??%?)
127      #E destruct //
128    ]
129| #b' #IH *
130  [ #t' normalize #E destruct
131  | #x #l #r #t' whd in ⊢ (??%? → ??%?)
132    lapply (IH r)
133    cases (update A b' a r)
134    [ #_ normalize #E destruct
135    | #r' #H normalize #E destruct @H @refl
136    ]
137  ]
138| #b' #IH *
139  [ #t' normalize #E destruct
140  | #x #l #r #t' whd in ⊢ (??%? → ??%?)
141    lapply (IH l)
142    cases (update A b' a l)
143    [ #_ normalize #E destruct
144    | #r' #H normalize #E destruct @H @refl
145    ]
146  ]
147] qed.
148
149lemma update_lookup_opt_other : ∀A,b,a,t,t'.
150  update A b a t = Some ? t' →
151  ∀b'. b ≠ b' →
152  lookup_opt A b' t = lookup_opt A b' t'.
153#A #b #a elim b
154[ * [ #t' normalize #E destruct
155    | * [2: #x] #l #r #t' normalize #E destruct
156      * [ * #H elim (H (refl …)) ]
157      #tl #NE normalize //
158    ]
159| #b' #IH *
160  [ #t' normalize #E destruct
161  | #x #l #r #t' normalize
162    lapply (IH r)
163    cases (update A b' a r)
164    [ #_ normalize #E destruct
165    | #t' #H normalize #E destruct * // #b'' #NE @H /2/
166    ]
167  ]
168| #b' #IH *
169  [ #t' normalize #E destruct
170  | #x #l #r #t' normalize
171    lapply (IH l)
172    cases (update A b' a l)
173    [ #_ normalize #E destruct
174    | #t' #H normalize #E destruct * // #b'' #NE @H /2/
175    ]
176  ]
177] qed.
178
179let rec merge (A: Type[0]) (b: positive_map A) (c:positive_map A) on b: positive_map A ≝
180match b with
181[ pm_leaf ⇒ c
182| pm_node a l r ⇒
183  match c with
184  [ pm_leaf ⇒ pm_node A a l r
185  | pm_node a' l' r' ⇒ pm_node A a' (merge A l l') (merge A r r')
186  ]
187].
188
Note: See TracBrowser for help on using the repository browser.