source: src/ASM/BitVectorTrie.ma @ 1424

Last change on this file since 1424 was 1424, checked in by sacerdot, 8 years ago
  1. fold function over BitVectorTries? moved from ERTLToLTL to ASM/BitVectorTrie
  2. ERTLToLTL now compiles again after removal of spill.ma
File size: 22.5 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
23lemma Sm_leq_n_m_leq_n:
24  ∀m, n: nat.
25    S m ≤ n → m ≤ n.
26  #m #n /2/
27qed.
28
29let rec bvtfold_aux
30  (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat)
31    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b ≝
32  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with
33  [ O    ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16.
34    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with
35    [ Leaf l      ⇒ λproof. f path l seed
36    | Stub s      ⇒ λproof. seed
37    | Node n' l r ⇒ λabsrd. ⊥
38    ] (refl … 0)
39  | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n').
40    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with
41    [ Leaf l      ⇒ λabsrd. ⊥
42    | Stub s      ⇒ λproof. seed
43    | Node n'' l r ⇒ λproof.
44        bvtfold_aux a b f (bvtfold_aux a b f seed n' ? (l⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((false:::path)⌈S (16 - S n') ↦ 16 - n'⌉)) n' ? (r⌈BitVectorTrie a n'' ↦ BitVectorTrie a n'⌉) ((true:::path)⌈S (16 - S n') ↦ 16 - n'⌉)
45    ] (refl … (S n'))
46  ].
47  [ 1, 2: destruct(absrd)
48  | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le //
49  | 4,7: destruct(proof) %
50  | 5,6: @Sm_leq_n_m_leq_n // ]
51qed.
52
53(* these two can probably be generalized w/r/t the second type and
54 * some sort of equality relationship *)
55lemma fold_eq:
56  ∀A: Type[0].
57  ∀n: nat.
58  ∀f.
59  ∀t.
60  ∀P, Q: Prop.
61  (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.
62 #A #n #f #t #P #Q #H
63 generalize in match (refl ? n) generalize in match H -H; generalize in match Q -Q; generalize in match P -P;
64 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?)
65 [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP)
66 | #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) ?)
67   [ @(Hr ? P Q HPQ (refl ? h) ?)
68     #a #t' #X #Y #HXY #Hff @(Hf (true:::a) t' X Y HXY Hff)
69   | #a #t' #X #Y #HXY #Hff @(Hf (false:::a) t' X Y HXY Hff) ]
70 | #h #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(HPQ HP) ]
71  @HP
72qed.
73 
74lemma fold_init:
75  ∀A:Type[0].
76  ∀n:nat.
77  ∀f.
78  ∀t.
79  ∀P: Prop.
80  (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P.
81 #A #n #f #t #P #H generalize in match (refl ? n) generalize in match H -H; generalize in match P -P;
82 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?) -t
83 [ #a #f #P #Hf #_ normalize @(Hf [[]])
84 | #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x)))
85   [ #a #t' #X @(Hf (true:::a) t' X) | @(refl ? h) | @(Hl (λx.f (false:::x)))
86     [ #a #t' #X @(Hf (false:::a) t' X) | @(refl ? h) | @HP ]
87   ]
88 | #h #f #P #Hf #_ normalize //
89
90
91 ]
92qed.
93 
94definition forall
95 ≝
96  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True.
97 
98lemma forall_nodel:
99  ∀A:Type[0].
100  ∀n:nat.
101  ∀l,r.
102  ∀P:BitVector (S n) → A → Prop.
103  forall A (S n) (Node ? n l r) P → forall A n l (λx.λa.P (false:::x) a).
104 #A #n #l #r #P #Hl
105 whd @(fold_eq A n ? ? (fold A ? n (λk.λa.λacc.P (true:::k) a∧acc) r True) True)
106 [ //
107 | #n #t' #X #Y #HXY #HX %1
108   [ @(proj1 ? ? HX) | @HXY @(proj2 ? ? HX) ]
109 | whd in Hl @Hl ]
110qed.
111 
112lemma forall_noder:
113  ∀A:Type[0].
114  ∀n:nat.
115  ∀l,r.
116  ∀P:BitVector (S n) → A → Prop.
117  forall A (S n) (Node ? n l r) P → forall A n r (λx.λa.P (true:::x) a).
118 #A #n #l #r #P #Hr
119 whd @(fold_init A n (λk.λa.λacc.P (false:::k) a∧acc) l) 
120 [ #n #t' #P #HP @(proj2 ? ? HP)
121 | @Hr
122 ]
123qed.
124
125lemma forall_node:
126  ∀A.∀n.∀l,r.∀P:BitVector (S n) → A → Prop.
127  forall A n l (λx.λa.P (false:::x) a) → forall A n r (λx.λa.P (true:::x) a) →
128  forall A (S n) (Node ? n l r) P.
129 #A #n #l #r #P #Hl #Hr
130 normalize @(fold_eq … True)
131 [ #_ @Hr
132 | #x #t' #X #Y #HXY #HP %1 [ @(proj1 … HP) | @HXY @(proj2 … HP) ]
133 | @Hl
134 ]
135qed.
136
137let rec lookup_opt (A: Type[0]) (n: nat)
138                (b: BitVector n) (t: BitVectorTrie A n) on t
139       : option A ≝
140 (match t return λx.λ_. BitVector x → option A with
141  [ Leaf l ⇒ λ_.Some ? l
142  | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l)
143  | Stub _ ⇒ λ_.None ?
144  ]) b.
145
146definition member ≝
147  λA.
148  λn.
149  λb: BitVector n.
150  λt: BitVectorTrie A n.
151  match lookup_opt A n b t with
152  [ None ⇒ false
153  | _    ⇒ true
154  ].
155
156definition member_p ≝
157  λA.
158  λn.
159  λb: BitVector n.
160  λt: BitVectorTrie A n.
161  match lookup_opt A n b t with
162  [ None ⇒ False
163  | _    ⇒ True
164  ].
165 
166lemma forall_lookup:
167 ∀A.
168  ∀n.
169  ∀t:BitVectorTrie A n.
170  ∀P:BitVector n → A → Prop.
171  forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a.
172 #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?)
173 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf)
174 | #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b)
175   #hd #bla elim bla -bla #tl #Htl >Htl in Hb; #Hb cases hd in Hb;
176   [ #Hb normalize in Hb; @(Hr (λx.λa.f (true:::x) a) (refl ? h))
177     [ @(forall_noder A h l r f Hf)
178     | @Hb
179     ]
180   | #Hb normalize in Hb; @(Hl (λx.λa.f (false:::x) a) (refl ? h))
181     [ @(forall_nodel A h l r f Hf)
182     | @Hb
183     ]
184   ]
185 | #n #f #_ #Hf #a #b #Hb normalize in Hb; destruct
186qed.
187
188lemma lookup_forall:
189 ∀A:Type[0].∀n.∀t:BitVectorTrie A n.∀P:BitVector n → A → Prop. 
190 (∀a:A.∀b:BitVector n.lookup_opt A n b t = Some ? a → P b a) → forall A n t P.
191 #A #n #t elim t
192 [ #x #P #HP normalize %1 [ @HP normalize @refl | // ]
193 | #h #l #r #Hl #Hr #P #HP @forall_node
194   [ @Hl #a #b #Hlookup @HP normalize @Hlookup
195   | @Hr #a #b #Hlookup @HP normalize @Hlookup
196   ]
197 | #n #P #HP normalize //
198 ]   
199qed.
200 
201let rec lookup (A: Type[0]) (n: nat)
202                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
203       : A ≝
204  (match b return λx.λ_. x = n → A with
205    [ VEmpty ⇒
206      (match t return λx.λ_. O = x → A with
207        [ Leaf l ⇒ λ_.l
208        | Node h l r ⇒ λK.⊥
209        | Stub s ⇒ λ_.a
210        ])
211    | VCons o hd tl ⇒
212      match t return λx.λ_. (S o) = x → A with
213        [ Leaf l ⇒ λK.⊥
214        | Node h l r ⇒
215           match hd with
216             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
217             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
218             ]
219        | Stub s ⇒ λ_. a]
220    ]) (refl ? n).
221  [1,2:
222    destruct
223  |*:
224    @ injective_S
225    //
226  ]
227qed.
228
229let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝
230   match b with
231    [ VEmpty ⇒ Leaf A a
232    | VCons o hd tl ⇒
233      match hd with
234        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
235        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
236        ]
237    ].
238
239let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝
240  (match b with
241    [ VEmpty ⇒ λ_. Leaf A a
242    | VCons o hd tl ⇒ λt.
243          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
244            [ Leaf l ⇒ λprf.⊥
245            | Node p l r ⇒ λprf.
246               match hd with
247                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
248                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
249                ]
250            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
251            ] (refl ? (S o))
252    ]).
253  [ destruct
254  |*:
255    @ injective_S
256    //
257  ]
258qed.
259 
260let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
261  (match b with
262    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
263                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
264                   | Stub _ ⇒ λ_. None ?
265                   | Node _ _ _ ⇒ λprf. ⊥
266                   ] (refl ? O)
267    | VCons o hd tl ⇒ λt.
268          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
269            [ Leaf l ⇒ λprf.⊥
270            | Node p l r ⇒ λprf.
271               match hd with
272                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
273                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
274                ]
275            | Stub p ⇒ λprf. None ?
276            ] (refl ? (S o))
277    ]).
278  [ 1,2: destruct
279  |*:
280    @ injective_S @sym_eq @prf
281  ]
282qed.
283
284let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝
285  match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with
286  [ Stub _ ⇒ λc. c
287  | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ]
288  | Node p l r ⇒
289    λc.
290    (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with
291    [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉))
292    | Stub _ ⇒ λprf. Node ? p l r
293    | Leaf _ ⇒ λabsd. ?
294    ] (refl ? (S p)))
295  ].
296  [1:
297      destruct(absd)
298  |2,3:
299      @ injective_S
300        assumption
301  ]
302qed.
303
304lemma BitVectorTrie_O:
305 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
306 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))
307  [ #w #_ %1 %[@w] %
308  | #n #l #r #abs @⊥ destruct(abs)
309  | #n #EQ %2 >EQ %]
310qed.
311
312lemma BitVectorTrie_Sn:
313 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
314 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)
315  [ #m #abs @⊥ destruct(abs)
316  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
317  | #m #EQ %2 // ]
318qed.
319
320lemma lookup_prepare_trie_for_insertion_hit:
321 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
322  lookup … b (prepare_trie_for_insertion … b v) a = v.
323 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
324qed.
325 
326lemma lookup_insert_hit:
327 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
328  lookup … b (insert … b v t) a = v.
329 #A #a #v #n #b elim b -b -n //
330 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
331  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
332  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
333qed.
334
335lemma lookup_prepare_trie_for_insertion_miss:
336 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
337  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
338 #A #a #v #n #c elim c
339  [ #b >(BitVector_O … b) normalize #abs @⊥ //
340  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
341    cases hd cases hd' normalize
342    [2,3: #_ cases tl' //
343    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
344qed.
345 
346lemma lookup_insert_miss:
347 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
348  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
349 #A #a #v #n #c elim c -c -n
350  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
351  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
352    #t cases(BitVectorTrie_Sn … t)
353    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
354     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
355    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
356     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
357     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
358qed.
359
360lemma lookup_stub:
361 ∀A.∀n.∀b.∀a.
362 lookup A n b (Stub A ?) a = a.
363 #A #n #b #a cases n in b ⊢ (??(??%%%?)?)
364 [ #b >(BitVector_O b) normalize @refl
365 | #h #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
366   [ normalize @refl
367   | normalize @refl
368   ]
369 ]   
370qed.   
371
372lemma lookup_opt_lookup_miss:
373  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
374  lookup_opt A n b t = None A → ∀x.lookup A n b t x = x.
375 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
376 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct
377 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
378   >Hb >Hb in H; cases hd
379   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
380   | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup
381   ]
382 | #n #B #_ #H #x @lookup_stub
383 ]
384qed.
385
386lemma lookup_opt_lookup_hit:
387  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
388  lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a.
389 #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?)
390 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl
391 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
392   >Hb >Hb in H; cases hd
393   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
394   | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup
395   ]
396 | #n #B #_ #H #x normalize in H; destruct
397 ]
398qed.
399
400lemma lookup_lookup_opt_hit:
401  ∀A.∀n.∀b.∀t.∀x,a.
402  lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a.
403 #A #n #b #t #x #a generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ?)
404 [ #z #B #_ #H #Hx >(BitVector_O B) in H; normalize #H >H @refl
405 | #h #l #r #Hl #Hr #B #_ #H #Hx cases (BitVector_Sn h B) #hd #X elim X; -X #tl #HB
406   >HB >HB in H; cases hd
407   [ normalize #H >(Hr tl (refl ? h) H Hx) @refl
408   | normalize #H >(Hl tl (refl ? h) H Hx) @refl
409   ]
410 | #n #B #_ #H #Hx cases B in H;
411   [ normalize #Hx' | #n' #b #v normalize #Hx' ]
412   @⊥ @(absurd (eq ? x a)) [1,3: @Hx' |2,4: @Hx ]
413 ]
414qed.
415
416lemma lookup_opt_prepare_trie_for_insertion_hit:
417 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
418  lookup_opt … b (prepare_trie_for_insertion … b v) = Some A v.
419 #A #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
420qed.
421
422lemma lookup_opt_prepare_trie_for_insertion_miss:
423 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.
424  (notb (eq_bv ? b c)) → lookup_opt … b (prepare_trie_for_insertion … c v) = None ?.
425 #A #v #n #c elim c
426  [ #b >(BitVector_O … b) normalize #abs @⊥ //
427  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
428    cases hd cases hd' normalize
429    [2,3: #_ cases tl' //
430    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) @IH ]]
431qed.
432
433lemma lookup_opt_insert_hit:
434 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
435  lookup_opt … b (insert … b v t) = Some A v.
436 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?)
437 [ #x #b >(BitVector_O b) normalize @refl
438 | #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
439   [ normalize @Hr
440   | normalize @Hl
441   ]
442 | #n' #b cases n' in b ⊢ ?
443   [ #b >(BitVector_O b) normalize @refl
444   | #m #b cases (BitVector_Sn m b) #hd #X elim X -X; #tl #Hb >Hb cases hd
445     normalize @lookup_opt_prepare_trie_for_insertion_hit
446   ]
447 ]
448qed.
449
450lemma lookup_opt_insert_miss:
451 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
452  (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t.
453 #A #v #n #c elim c -c -n
454  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
455  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
456    #t cases(BitVectorTrie_Sn … t)
457    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
458     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
459    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
460     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
461     [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]]
462qed.
463
464lemma forall_insert_inv1:
465  ∀A.∀n.∀b.∀a.∀t.∀P.
466  forall A n (insert A n b a t) P → P b a.
467 #A #n #b #a #t #P #H @(forall_lookup ? ? (insert A n b a t))
468 [ @H
469 | >(lookup_opt_insert_hit A ? n b) @(refl ? (Some A a))
470 ]
471qed.
472
473lemma forall_insert_inv2a:
474  ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P.
475  lookup_opt A n b t = (None A)  → forall A n (insert A n b a t) P → forall A n t P.
476 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%)
477 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct
478 | #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #Hlookup #H
479   [ normalize in H; normalize
480     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … H)
481     [ #Hfold @(Hr tl (refl ? h) ? Hlookup Hfold)
482     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ?HP)) ]
483     ]
484   | normalize in H; normalize     
485     @(fold_eq … True)
486     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
487       [ #z #t' #X #HX @(proj2 ? ? HX)
488       | @H ]
489     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
490     | @(Hl tl (refl ? h) ? Hlookup) normalize
491       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
492       [ //
493       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
494       | @H
495       ]
496     ]
497   ]
498 | #n #b #_ #P #Hlookup #Hf normalize // ]
499qed.
500
501lemma forall_insert_inv2b:
502  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop).
503  (∀x.(lookup_opt A n b t = Some A x) → P b x) → forall A n (insert A n b a t) P → forall A n t P.
504 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?)
505 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl | @(proj2 ? ? Hf) ]
506 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #HP #Hf
507   [ normalize in Hf; normalize
508     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … Hf)
509     [ #Hfold @(Hr tl (refl ? h) ? HP Hfold)
510     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
511     ]
512   | normalize in H; normalize     
513     @(fold_eq … True)
514     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
515       [ #z #t' #X #HX @(proj2 ? ? HX)
516       | @Hf ]
517     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
518     | @(Hl tl (refl ? h) ? HP) normalize
519       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
520       [ //
521       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
522       | @Hf
523       ]
524     ]
525   ]
526 | #n #b #_ #P #Hlookup #Hf normalize // ]
527qed.
528
529lemma forall_prepare_tree_for_insertion:
530 ∀A:Type[0].∀h:nat.∀b:BitVector h.∀a:A.∀P.
531 P b a →
532 forall A h (prepare_trie_for_insertion A h b a) P.
533 #A #h #b elim b
534 [ #a #P #HP normalize %1 [ @HP | // ]
535 | #h #x #tl #Ha #a #P cases x #HP normalize @Ha @HP
536 ]
537qed.
538
539lemma forall_insert:
540  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P.
541  forall A n t P → P b a → forall A n (insert A n b a t) P.
542 #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%)
543 [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/
544 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #Hf #HP
545   [ normalize in Hf; normalize
546     @(fold_eq A … (fold A … (λx.λa0.λacc.P (true:::x) a0∧acc) r True) … Hf)
547     [ #Hp @(Hr tl (refl ? h) ? Hp HP)
548     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
549     ]
550   | normalize in Hf; normalize
551     @(fold_eq … True)
552     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0∧acc) l)
553       [ #z #t' #X #HX @(proj2 ? ? HX)
554       | @Hf ]
555     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
556     | @(Hl tl (refl ? h) ? ? HP)
557       normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
558       [ //
559       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
560       | @Hf
561       ]
562     ]
563   ]
564 | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%)
565   [ #b #P #Hf #HP normalize %1 [ @HP | // ]
566   | #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP)
567   ]
568 ]
569qed.
570
571lemma update_fail : ∀A,n,b,a,t.
572  update A n b a t = None ? →
573  lookup_opt A n b t = None ?.
574#A #n elim n
575[ #b @(vector_inv_n … b) #a #t cases (BitVectorTrie_O … t)
576  [ * #x #E >E normalize #NE destruct
577  | #E >E normalize //
578  ]
579| #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t)
580  [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?)
581    #X lapply (option_map_none … X) @IH
582  | #E >E normalize //
583  ]
584] qed.
585
586lemma update_lookup_opt_same : ∀A,n,b,a,t,t'.
587  update A n b a t = Some ? t' →
588  lookup_opt A n b t' = Some ? a.
589#A #n elim n
590[ #b #a #t #t' @(vector_inv_n … b)
591  cases (BitVectorTrie_O … t)
592  [ * #x #E >E normalize #E' destruct @refl
593  | #E >E normalize #E' destruct
594  ]
595| #m #IH #b #a #t #t'
596  @(vector_inv_n … b) #bhd #btl
597  cases (BitVectorTrie_Sn … t)
598  [ * #t1 * #t2 #E' >E'
599    whd in ⊢ (??%? → ??%?) cases bhd #U
600    cases (option_map_some ????? U)
601    #tn' * #U' #E'' <E''
602    whd in ⊢ (??%?) whd in ⊢ (??(???%%)?)
603    @(IH … U')
604  | #E >E normalize #E' destruct
605  ]
606] qed.
607
608lemma update_lookup_opt_other : ∀A,n,b,a,t,t'.
609  update A n b a t = Some ? t' →
610  ∀b'. b ≠ b' →
611  lookup_opt A n b' t = lookup_opt A n b' t'.
612#A #n elim n
613[ #b #a #t #t' #E #b'
614  @(vector_inv_n … b) @(vector_inv_n … b')
615  * #NE cases (NE (refl ??))
616| #m #IH #b #a #t #t'
617  @(vector_inv_n … b) #bhd #btl
618  cases (BitVectorTrie_Sn … t)
619  [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?) cases bhd
620    #U cases (option_map_some ????? U) #tn' * #U' #E' <E'
621    #b' @(vector_inv_n … b') #bhd' #btl'
622    cases bhd'
623    [ 2,3: #_ @refl
624    | *: #NE whd in ⊢ (??%%) whd in ⊢ (??(???%%)(???%%))
625         @(IH … U') % #E'' >E'' in NE * #H @H @refl
626    ]
627  | #E >E whd in ⊢ (??%? → ?) #NE destruct
628  ]
629] qed.
Note: See TracBrowser for help on using the repository browser.