source: src/ASM/BitVectorTrie.ma @ 1006

Last change on this file since 1006 was 1006, checked in by boender, 8 years ago
  • added fold + lemmas on fold
File size: 10.6 KB
Line 
1include "basics/types.ma".
2
3include "utilities/option.ma".
4include "ASM/BitVector.ma".
5
6inductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
7  Leaf: A → BitVectorTrie A O
8| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
9| Stub: ∀n: nat. BitVectorTrie A n.
10
11let rec fold (A, B: Type[0]) (n: nat) (f: BitVector n → A → B → B)
12 (t: BitVectorTrie A n) (b: B) on t: B ≝
13 (match t return λx.λ_.x = n → B with
14  [ Leaf l ⇒ λ_.f (zero ?) l b
15  | Node h l r ⇒ λK.
16    fold A B h (λx.f ((VCons ? h false x)⌈(S h) ↦ n⌉)) l
17      (fold A B h (λx.f ((VCons ? h true x)⌈(S h) ↦ n⌉)) r b)
18  | Stub _ ⇒ λ_.b
19  ]) (refl ? n).
20 @K
21qed.
22
23(* these two can probably be generalized w/r/t the second type and
24 * some sort of equality relationship *)
25lemma fold_eq:
26  ∀A: Type[0].
27  ∀n: nat.
28  ∀f.
29  ∀t.
30  ∀P, Q: Prop.
31  (P → Q) → (∀a,t',P,Q.(P → Q) → f a t' P → f a t' Q) → fold A ? n f t P → fold A ? n f t Q.
32 #A #n #f #t #P #Q #H
33 generalize in match (refl ? n) generalize in match H -H; generalize in match Q -Q; generalize in match P -P;
34 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?)
35 [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP)
36 | #h #l #r #Hl #Hr #f #P #Q #HPQ #_ #Hf #HP normalize normalize in HP; @(Hl ? (fold A Prop h (λx.f (true:::x)) r P) (fold A Prop h (λx.f (true:::x)) r Q) ? (refl ? h) ?)
37   [ @(Hr ? P Q HPQ (refl ? h) ?)
38     #a #t' #X #Y #HXY #Hff @(Hf (true:::a) t' X Y HXY Hff)
39   | #a #t' #X #Y #HXY #Hff @(Hf (false:::a) t' X Y HXY Hff) ]
40 | #h #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(HPQ HP) ]
41  @HP
42qed.
43 
44lemma fold_init:
45  ∀A:Type[0].
46  ∀n:nat.
47  ∀f.
48  ∀t.
49  ∀P: Prop.
50  (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P.
51 #A #n #f #t #P #H generalize in match (refl ? n) generalize in match H -H; generalize in match P -P;
52 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?) -t
53 [ #a #f #P #Hf #_ normalize @(Hf [[]])
54 | #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x)))
55   [ #a #t' #X @(Hf (true:::a) t' X) | @(refl ? h) | @(Hl (λx.f (false:::x)))
56     [ #a #t' #X @(Hf (false:::a) t' X) | @(refl ? h) | @HP ]
57   ]
58 | #h #f #P #Hf #_ normalize //
59 ]
60qed.
61 
62(* definition forall
63 ≝
64  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λ_.λa.λacc.(P a) ∧ acc) t True. *)
65
66definition forall
67 ≝
68  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True.
69 
70(* lemma forall_nodel:
71  ∀A:Type[0].
72  ∀n:nat.
73  ∀l,r.
74  ∀P:A → Prop.
75  forall A (S n) (Node ? n l r) P → forall A n l P.
76 #A #n #l #r #P generalize in match (refl ? n) #_ #Hl
77 whd in Hl; whd @(fold_eq A n ? ? (fold A ? n (λx.λa.λacc.P a∧acc) r True) True)
78 [ //
79 | #n #t' #X #Y #HXY #HX %1
80   [ @(proj1 ? ? HX) | @HXY @(proj2 ? ? HX) ]
81 | @Hl ]
82qed.
83 
84lemma forall_noder:
85  ∀A:Type[0].
86  ∀n:nat.
87  ∀l,r.
88  ∀P.
89  forall A (S n) (Node ? n l r) P → forall A n r P.
90 #A #n #l #r #P generalize in match (refl ? n) #_ #Hr
91 whd in Hr; whd @(fold_init A n (λx.λa.λacc.P a∧acc) l) 
92 [ #n #t' #P #HP @(proj2 ? ? HP)
93 | @Hr
94 ]
95qed. *)
96
97lemma forall_nodel:
98  ∀A:Type[0].
99  ∀n:nat.
100  ∀l,r.
101  ∀P:BitVector (S n) → A → Prop.
102  forall A (S n) (Node ? n l r) P → forall A n l (λx.λa.P (false:::x) a).
103 #A #n #l #r #P #Hl
104 whd @(fold_eq A n ? ? (fold A ? n (λk.λa.λacc.P (true:::k) a∧acc) r True) True)
105 [ //
106 | #n #t' #X #Y #HXY #HX %1
107   [ @(proj1 ? ? HX) | @HXY @(proj2 ? ? HX) ]
108 | whd in Hl @Hl ]
109qed.
110 
111lemma forall_noder:
112  ∀A:Type[0].
113  ∀n:nat.
114  ∀l,r.
115  ∀P:BitVector (S n) → A → Prop.
116  forall A (S n) (Node ? n l r) P → forall A n r (λx.λa.P (true:::x) a).
117 #A #n #l #r #P #Hr
118 whd @(fold_init A n (λk.λa.λacc.P (false:::k) a∧acc) l) 
119 [ #n #t' #P #HP @(proj2 ? ? HP)
120 | @Hr
121 ]
122qed.
123
124let rec lookup_opt (A: Type[0]) (n: nat)
125                (b: BitVector n) (t: BitVectorTrie A n) on t
126       : option A ≝
127 (match t return λx.λ_. BitVector x → option A with
128  [ Leaf l ⇒ λ_.Some ? l
129  | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l)
130  | Stub _ ⇒ λ_.None ?
131  ]) b.
132 
133lemma forall_lookup:
134 ∀A.
135  ∀n.
136  ∀t:BitVectorTrie A n.
137  ∀P:BitVector n → A → Prop.
138  forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a.
139 #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?)
140 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf)
141 | #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b)
142   #hd #bla elim bla -bla #tl #Htl >Htl in Hb; #Hb cases hd in Hb;
143   [ #Hb normalize in Hb; @(Hr (λx.λa.f (true:::x) a) (refl ? h))
144     [ @(forall_noder A h l r f Hf)
145     | @Hb
146     ]
147   | #Hb normalize in Hb; @(Hl (λx.λa.f (false:::x) a) (refl ? h))
148     [ @(forall_nodel A h l r f Hf)
149     | @Hb
150     ]
151   ]
152 | #n #f #_ #Hf #a #b #Hb normalize in Hb; destruct
153qed.
154
155let rec lookup (A: Type[0]) (n: nat)
156                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
157       : A ≝
158  (match b return λx.λ_. x = n → A with
159    [ VEmpty ⇒
160      (match t return λx.λ_. O = x → A with
161        [ Leaf l ⇒ λ_.l
162        | Node h l r ⇒ λK.⊥
163        | Stub s ⇒ λ_.a
164        ])
165    | VCons o hd tl ⇒
166      match t return λx.λ_. (S o) = x → A with
167        [ Leaf l ⇒ λK.⊥
168        | Node h l r ⇒
169           match hd with
170             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
171             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
172             ]
173        | Stub s ⇒ λ_. a]
174    ]) (refl ? n).
175  [1,2:
176    destruct
177  |*:
178    @ injective_S
179    //
180  ]
181qed.
182
183let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝
184   match b with
185    [ VEmpty ⇒ Leaf A a
186    | VCons o hd tl ⇒
187      match hd with
188        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
189        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
190        ]
191    ].
192
193let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝
194  (match b with
195    [ VEmpty ⇒ λ_. Leaf A a
196    | VCons o hd tl ⇒ λt.
197          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
198            [ Leaf l ⇒ λprf.⊥
199            | Node p l r ⇒ λprf.
200               match hd with
201                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
202                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
203                ]
204            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
205            ] (refl ? (S o))
206    ]).
207  [ destruct
208  |*:
209    @ injective_S
210    //
211  ]
212qed.
213
214let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
215  (match b with
216    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
217                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
218                   | Stub _ ⇒ λ_. None ?
219                   | Node _ _ _ ⇒ λprf. ⊥
220                   ] (refl ? O)
221    | VCons o hd tl ⇒ λt.
222          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
223            [ Leaf l ⇒ λprf.⊥
224            | Node p l r ⇒ λprf.
225               match hd with
226                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
227                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
228                ]
229            | Stub p ⇒ λprf. None ?
230            ] (refl ? (S o))
231    ]).
232  [ 1,2: destruct
233  |*:
234    @ injective_S @sym_eq @prf
235  ]
236qed.
237
238let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝
239  match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with
240  [ Stub _ ⇒ λc. c
241  | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ]
242  | Node p l r ⇒
243    λc.
244    (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with
245    [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉))
246    | Stub _ ⇒ λprf. Node ? p l r
247    | Leaf _ ⇒ λabsd. ?
248    ] (refl ? (S p)))
249  ].
250  [1:
251      destruct(absd)
252  |2,3:
253      @ injective_S
254        assumption
255  ]
256qed.
257
258lemma BitVectorTrie_O:
259 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
260 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
261  [ #w #_ %1 %[@w] %
262  | #n #l #r #abs @⊥ destruct(abs)
263  | #n #EQ %2 >EQ %]
264qed.
265
266lemma BitVectorTrie_Sn:
267 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
268 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
269  [ #m #abs @⊥ destruct(abs)
270  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
271  | #m #EQ %2 // ]
272qed.
273
274lemma lookup_prepare_trie_for_insertion_hit:
275 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
276  lookup … b (prepare_trie_for_insertion … b v) a = v.
277 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
278qed.
279 
280lemma lookup_insert_hit:
281 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
282  lookup … b (insert … b v t) a = v.
283 #A #a #v #n #b elim b -b -n //
284 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
285  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
286  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
287qed.
288
289lemma lookup_prepare_trie_for_insertion_miss:
290 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
291  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
292 #A #a #v #n #c elim c
293  [ #b >(BitVector_O … b) normalize #abs @⊥ //
294  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
295    cases hd cases hd' normalize
296    [2,3: #_ cases tl' //
297    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
298qed.
299 
300lemma lookup_insert_miss:
301 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
302  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
303 #A #a #v #n #c elim c -c -n
304  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
305  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
306    #t cases(BitVectorTrie_Sn … t)
307    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
308     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
309    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
310     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
311     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
312qed.
Note: See TracBrowser for help on using the repository browser.