source: src/common/PositiveMap.ma @ 1566

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

Pacify changes to destruct tactic.

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.