source: src/ASM/BitVectorTrie.ma @ 2767

Last change on this file since 2767 was 2767, checked in by mckinna, 7 years ago

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File size: 26.6 KB
Line 
1include "basics/types.ma".
2include "ASM/BitVector.ma".
3
4inductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝
5  Leaf: A → BitVectorTrie A O
6| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
7| Stub: ∀n: nat. BitVectorTrie A n.
8
9let rec fold (A, B: Type[0]) (n: nat) (f: BitVector n → A → B → B)
10 (t: BitVectorTrie A n) (b: B) on t: B ≝
11 (match t return λx.λ_.x = n → B with
12  [ Leaf l ⇒ λ_.f (zero ?) l b
13  | Node h l r ⇒ λK.
14    fold A B h (λx.f ((VCons ? h false x)⌈(S h) ↦ n⌉)) l
15      (fold A B h (λx.f ((VCons ? h true x)⌈(S h) ↦ n⌉)) r b)
16  | Stub _ ⇒ λ_.b
17  ]) (refl ? n).
18 @K
19qed.
20
21lemma Sm_leq_n_m_leq_n:
22  ∀m, n: nat.
23    S m ≤ n → m ≤ n.
24  #m #n /2/
25qed.
26
27let rec bvtfold_aux
28  (a, b: Type[0]) (f: BitVector 16 → a → b → b) (seed: b) (n: nat)
29    on n: n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b ≝
30  match n return λn: nat. n ≤ 16 → BitVectorTrie a n → BitVector (16 - n) → b with
31  [ O    ⇒ λinvariant: 0 ≤ 16. λtrie: BitVectorTrie a 0. λpath: BitVector 16.
32    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = 0. b with
33    [ Leaf l      ⇒ λproof. f path l seed
34    | Stub s      ⇒ λproof. seed
35    | Node n' l r ⇒ λabsrd. ⊥
36    ] (refl … 0)
37  | S n' ⇒ λinvariant: S n' ≤ 16. λtrie: BitVectorTrie a (S n'). λpath: BitVector (16 - S n').
38    match trie return λx: nat. λtrie': BitVectorTrie a x. ∀prf: x = S n'. b with
39    [ Leaf l      ⇒ λabsrd. ⊥
40    | Stub s      ⇒ λproof. seed
41    | Node n'' l r ⇒ λproof.
42        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'⌉)
43    ] (refl … (S n'))
44  ].
45  [ 1, 2: destruct(absrd)
46  | 3,8: >minus_S_S <minus_Sn_m // @le_S_S_to_le //
47  | 4,7: destruct(proof) %
48  | 5,6: @Sm_leq_n_m_leq_n // ]
49qed.
50
51(* these two can probably be generalized w/r/t the second type and
52 * some sort of equality relationship *)
53lemma fold_eq:
54  ∀A: Type[0].
55  ∀n: nat.
56  ∀f.
57  ∀t.
58  ∀P, Q: Prop.
59  (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.
60 #A #n #f #t #P #Q #H
61 generalize in match (refl ? n); generalize in match H; -H; generalize in match Q; -Q; generalize in match P; -P;
62 elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?);
63 [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP)
64 | #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) ?)
65   [ @(Hr ? P Q HPQ (refl ? h) ?)
66     #a #t' #X #Y #HXY #Hff @(Hf (true:::a) t' X Y HXY Hff)
67   | #a #t' #X #Y #HXY #Hff @(Hf (false:::a) t' X Y HXY Hff) ]
68 | #h #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(HPQ HP) ]
69  @HP
70qed.
71 
72lemma fold_init:
73  ∀A:Type[0].
74  ∀n:nat.
75  ∀f.
76  ∀t.
77  ∀P: Prop.
78  (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P.
79 #A #n #f #t #P #H generalize in match (refl ? n); generalize in match H; -H; generalize in match P; -P;
80 elim t in f ⊢ (? → ? → ???% → ???%%%? → ?); -t
81 [ #a #f #P #Hf #_ normalize @(Hf [[]])
82 | #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x)))
83   [ #a #t' #X @(Hf (true:::a) t' X) | @(refl ? h) | @(Hl (λx.f (false:::x)))
84     [ #a #t' #X @(Hf (false:::a) t' X) | @(refl ? h) | @HP ]
85   ]
86 | #h #f #P #Hf #_ normalize //
87
88
89 ]
90qed.
91 
92definition forall
93 ≝
94  λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True.
95
96alias id "bvt_forall" = "cic:/matita/cerco/ASM/BitVectorTrie/forall.def(4)".
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
146alias id "bvt_lookup_opt" = "cic:/matita/cerco/ASM/BitVectorTrie/lookup_opt.fix(0,3,2)".
147
148definition member ≝
149  λA.
150  λn.
151  λb: BitVector n.
152  λt: BitVectorTrie A n.
153  match lookup_opt A n b t with
154  [ None ⇒ false
155  | _    ⇒ true
156  ].
157
158definition member_p ≝
159  λA.
160  λn.
161  λb: BitVector n.
162  λt: BitVectorTrie A n.
163  match lookup_opt A n b t with
164  [ None ⇒ False
165  | _    ⇒ True
166  ].
167 
168lemma forall_lookup:
169 ∀A.
170  ∀n.
171  ∀t:BitVectorTrie A n.
172  ∀P:BitVector n → A → Prop.
173  forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a.
174 #A #n #t #P generalize in match (refl ? n); elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?);
175 [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf)
176 | #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b)
177   #hd #bla elim bla -bla #tl #Htl >Htl in Hb; #Hb cases hd in Hb;
178   [ #Hb normalize in Hb; @(Hr (λx.λa.f (true:::x) a) (refl ? h))
179     [ @(forall_noder A h l r f Hf)
180     | @Hb
181     ]
182   | #Hb normalize in Hb; @(Hl (λx.λa.f (false:::x) a) (refl ? h))
183     [ @(forall_nodel A h l r f Hf)
184     | @Hb
185     ]
186   ]
187 | #n #f #_ #Hf #a #b #Hb normalize in Hb; destruct
188qed.
189
190lemma lookup_forall:
191 ∀A:Type[0].∀n.∀t:BitVectorTrie A n.∀P:BitVector n → A → Prop. 
192 (∀a:A.∀b:BitVector n.lookup_opt A n b t = Some ? a → P b a) → forall A n t P.
193 #A #n #t elim t
194 [ #x #P #HP normalize %1 [ @HP normalize @refl | // ]
195 | #h #l #r #Hl #Hr #P #HP @forall_node
196   [ @Hl #a #b #Hlookup @HP normalize @Hlookup
197   | @Hr #a #b #Hlookup @HP normalize @Hlookup
198   ]
199 | #n #P #HP normalize //
200 ]   
201qed.
202 
203let rec lookup (A: Type[0]) (n: nat)
204                (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b
205       : A ≝
206  (match b return λx.λ_. x = n → A with
207    [ VEmpty ⇒
208      (match t return λx.λ_. O = x → A with
209        [ Leaf l ⇒ λ_.l
210        | Node h l r ⇒ λK.⊥
211        | Stub s ⇒ λ_.a
212        ])
213    | VCons o hd tl ⇒
214      match t return λx.λ_. (S o) = x → A with
215        [ Leaf l ⇒ λK.⊥
216        | Node h l r ⇒
217           match hd with
218             [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a
219             | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a
220             ]
221        | Stub s ⇒ λ_. a]
222    ]) (refl ? n).
223  [1,2:
224    destruct
225  |*:
226    @ injective_S
227    //
228  ]
229qed.
230
231alias id "bvt_lookup" = "cic:/matita/cerco/ASM/BitVectorTrie/lookup.fix(0,2,5)".
232
233let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝
234   match b with
235    [ VEmpty ⇒ Leaf A a
236    | VCons o hd tl ⇒
237      match hd with
238        [ true ⇒  Node A o (Stub A o) (prepare_trie_for_insertion A o tl a)
239        | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o)
240        ]
241    ].
242
243let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝
244  (match b with
245    [ VEmpty ⇒ λ_. Leaf A a
246    | VCons o hd tl ⇒ λt.
247          match t return λy.λ_. S o = y → BitVectorTrie A (S o) with
248            [ Leaf l ⇒ λprf.⊥
249            | Node p l r ⇒ λprf.
250               match hd with
251                [ true ⇒  Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉))
252                | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉)
253                ]
254            | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a)
255            ] (refl ? (S o))
256    ]).
257  [ destruct
258  |*:
259    @ injective_S
260    //
261  ]
262qed.
263 
264alias id "bvt_insert" = "cic:/matita/cerco/ASM/BitVectorTrie/insert.fix(0,2,5)".
265
266let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝
267  (match b with
268    [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with
269                   [ Leaf _ ⇒ λ_. Some ? (Leaf A a)
270                   | Stub _ ⇒ λ_. None ?
271                   | Node _ _ _ ⇒ λprf. ⊥
272                   ] (refl ? O)
273    | VCons o hd tl ⇒ λt.
274          match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with
275            [ Leaf l ⇒ λprf.⊥
276            | Node p l r ⇒ λprf.
277               match hd with
278                [ true ⇒  option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉))
279                | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉))
280                ]
281            | Stub p ⇒ λprf. None ?
282            ] (refl ? (S o))
283    ]).
284  [ 1,2: destruct
285  |*:
286    @ injective_S @sym_eq @prf
287  ]
288qed.
289
290let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝
291  match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with
292  [ Stub _ ⇒ λc. c
293  | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ]
294  | Node p l r ⇒
295    λc.
296    (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with
297    [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉))
298    | Stub _ ⇒ λprf. Node ? p l r
299    | Leaf _ ⇒ λabsd. ?
300    ] (refl ? (S p)))
301  ].
302  [1:
303      destruct(absd)
304  |2,3:
305      @ injective_S
306        assumption
307  ]
308qed.
309
310lemma BitVectorTrie_O:
311 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.
312 #A #v generalize in match (refl … O); cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??));
313  [ #w #_ %1 %[@w] %
314  | #n #l #r #abs @⊥ destruct(abs)
315  | #n #EQ %2 >EQ %]
316qed.
317
318lemma BitVectorTrie_Sn:
319 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).
320 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%);
321  [ #m #abs @⊥ destruct(abs)
322  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
323  | #m #EQ %2 // ]
324qed.
325
326lemma lookup_prepare_trie_for_insertion_hit:
327 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.
328  lookup … b (prepare_trie_for_insertion … b v) a = v.
329 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
330qed.
331 
332lemma lookup_insert_hit:
333 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
334  lookup … b (insert … b v t) a = v.
335 #A #a #v #n #b elim b -b -n //
336 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)
337  [ * #l * #r #JMEQ >JMEQ cases hd normalize //
338  | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]
339qed.
340
341lemma lookup_prepare_trie_for_insertion_miss:
342 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.
343  (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.
344 #A #a #v #n #c elim c
345  [ #b >(BitVector_O … b) normalize #abs @⊥ //
346  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
347    cases hd cases hd' normalize
348    [2,3: #_ cases tl' //
349    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]
350qed.
351 
352lemma lookup_insert_miss:
353 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
354  (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.
355 #A #a #v #n #c elim c -c -n
356  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; //
357  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
358    #t cases(BitVectorTrie_Sn … t)
359    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
360     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH //
361    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
362     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize
363     [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]]
364qed.
365
366lemma lookup_stub:
367 ∀A.∀n.∀b.∀a.
368 lookup A n b (Stub A ?) a = a.
369 #A #n #b #a cases n in b ⊢ (??(??%%%?)?);
370 [ #b >(BitVector_O b) normalize @refl
371 | #h #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
372   [ normalize @refl
373   | normalize @refl
374   ]
375 ]   
376qed.   
377
378lemma lookup_opt_lookup_miss:
379  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.
380  lookup_opt A n b t = None A → ∀x.lookup A n b t x = x.
381 #A #n #b #t generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?);
382 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct
383 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
384   >Hb >Hb in H; cases hd
385   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
386   | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup
387   ]
388 | #n #B #_ #H #x @lookup_stub
389 ]
390qed.
391
392lemma lookup_opt_lookup_hit:
393  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A.
394  lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a.
395 #A #n #b #t #a generalize in match (refl ? n); elim t in b ⊢ (???% → ??(??%%%)? → ? → ?);
396 [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl
397 | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb
398   >Hb >Hb in H; cases hd
399   [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup
400   | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup
401   ]
402 | #n #B #_ #H #x normalize in H; destruct
403 ]
404qed.
405
406lemma lookup_lookup_opt_hit:
407  ∀A.∀n.∀b.∀t.∀x,a.
408  lookup A n b t x = a → x ≠ a → lookup_opt A n b t = Some A a.
409 #A #n #b #t #x #a generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ?);
410 [ #z #B #_ #H #Hx >(BitVector_O B) in H; normalize #H >H @refl
411 | #h #l #r #Hl #Hr #B #_ #H #Hx cases (BitVector_Sn h B) #hd #X elim X; -X #tl #HB
412   >HB >HB in H; cases hd
413   [ normalize #H >(Hr tl (refl ? h) H Hx) @refl
414   | normalize #H >(Hl tl (refl ? h) H Hx) @refl
415   ]
416 | #n #B #_ #H #Hx cases B in H;
417   [ normalize #Hx' | #n' #b #v normalize #Hx' ]
418   @⊥ @(absurd (eq ? x a)) [1,3: @Hx' |2,4: @Hx ]
419 ]
420qed.
421
422lemma lookup_opt_lookup:
423  ∀A,n,b,t1,t2,x.
424  lookup_opt A n b t1 = lookup_opt A n b t2 → lookup A n b t1 x = lookup A n b t2 x.
425 #A #n #b #t1 #t2 #x lapply (refl ? (lookup_opt A n b t2))
426 cases (lookup_opt A n b t2) in ⊢ (???% → %);
427 [ #H2 #H1 >(lookup_opt_lookup_miss … H1) >(lookup_opt_lookup_miss … H2) //
428 | #y #H2 #H1 >(lookup_opt_lookup_hit … y H1) >(lookup_opt_lookup_hit … y H2) //
429 ]
430qed.
431   
432lemma lookup_opt_prepare_trie_for_insertion_hit:
433 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.
434  lookup_opt … b (prepare_trie_for_insertion … b v) = Some A v.
435 #A #v #n #b elim b // #m #hd #tl #IH cases hd normalize //
436qed.
437
438lemma lookup_opt_prepare_trie_for_insertion_miss:
439 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.
440  (notb (eq_bv ? b c)) → lookup_opt … b (prepare_trie_for_insertion … c v) = None ?.
441 #A #v #n #c elim c
442  [ #b >(BitVector_O … b) normalize #abs @⊥ //
443  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
444    cases hd cases hd' normalize
445    [2,3: #_ cases tl' //
446    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) @IH ]]
447qed.
448
449lemma lookup_opt_insert_hit:
450 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
451  lookup_opt … b (insert … b v t) = Some A v.
452 #A #v #n #b #t elim t in b ⊢ (??(??%%%)?);
453 [ #x #b >(BitVector_O b) normalize @refl
454 | #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd
455   [ normalize @Hr
456   | normalize @Hl
457   ]
458 | #n' #b cases n' in b ⊢ ?;
459   [ #b >(BitVector_O b) normalize @refl
460   | #m #b cases (BitVector_Sn m b) #hd #X elim X -X; #tl #Hb >Hb cases hd
461     normalize @lookup_opt_prepare_trie_for_insertion_hit
462   ]
463 ]
464qed.
465
466lemma lookup_opt_insert_miss:
467 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
468  (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t.
469 #A #v #n #c elim c -c -n
470  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF; //
471  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
472    #t cases(BitVectorTrie_Sn … t)
473    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
474     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize // @IH //
475    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
476     [1,4: change with (bool_to_Prop (notb (eq_bv ???))) in H; ] normalize
477     [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]]
478qed.
479
480lemma insert_lookup_opt_hit:
481 ∀A:Type[0].∀v,a:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
482   lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ (b = c ∧ a = v).
483 #A #v #a #n #c elim c -c; -n;
484 [ #b #t #Hl normalize in Hl; %2 destruct (Hl) @conj [ @BitVector_O | @refl ]
485 | #n #hd #tl #Hind #b cases (BitVector_Sn … b) #hd' * #tl' #Heq >Heq
486   #t cases (BitVectorTrie_Sn … t)
487   [ * #l * #r #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
488     [1,4: cases (Hind tl' ? H) #Hi2 [1,3: %1 @Hi2 |2,4: %2 @conj
489       [1,3: >(proj1 ?? Hi2) @refl
490       |2,4: @(proj2 ?? Hi2) ] ]
491     |2,3: %1 @H
492     ]
493   | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
494     [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3
495       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 /2 by pair_destruct/
496       |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H;
497         [1,3: #X %1 //
498         |2,4: >Heq3 //
499         ]
500       ]
501     |2,3: destruct (H)
502     ]
503qed.
504
505lemma insert_lookup_opt_miss:
506 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
507   lookup_opt … b (insert … c v t) = None A →
508     (notb (eq_bv n b c)) = true ∧ lookup_opt … b t = None A.
509 #A #v #n #c elim c -c; -n;
510 [ #b #t #Hl normalize in Hl; destruct (Hl)
511 | #n #hd #tl #Hind #b cases (BitVector_Sn … b) #hd' * #tl' #Heq >Heq
512   #t cases (BitVectorTrie_Sn … t)
513   [ * #l * #r #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
514     [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% ->%); #Heq3
515       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_insert_hit #H destruct (H)
516       |2,4: >lookup_opt_insert_miss in H;
517         [1,3: #H whd in match eq_bv in Heq3; >Heq3 @conj
518           [1,3: / by refl/
519           |2,4: @H
520           ]
521         |2,4: >Heq3 / by I/
522         ]
523       ]
524     |2,3: @conj
525       [1,3: @refl
526       |2,4: @H
527       ]
528     ]
529   | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
530     [1,4:  lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3
531       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X)
532       |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H;
533         [1,3: #X @conj
534           [1,3: whd in match (eq_bv ???) in Heq3; >Heq3 / by refl/
535           |2,4: @refl
536           ]
537         |2,4: >Heq3 / by I/
538         ]
539       ]
540     |2,3: @conj @refl
541     ]
542   ]
543 ]
544qed.
545   
546lemma forall_insert_inv1:
547  ∀A.∀n.∀b.∀a.∀t.∀P.
548  forall A n (insert A n b a t) P → P b a.
549 #A #n #b #a #t #P #H @(forall_lookup ? ? (insert A n b a t))
550 [ @H
551 | >(lookup_opt_insert_hit A ? n b) @(refl ? (Some A a))
552 ]
553qed.
554
555lemma forall_insert_inv2a:
556  ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P.
557  lookup_opt A n b t = (None A)  → forall A n (insert A n b a t) P → forall A n t P.
558 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%);
559 [ #x #b #_ #P >(BitVector_O b) normalize #H destruct
560 | #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #Hlookup #H
561   [ normalize in H; normalize
562     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … H)
563     [ #Hfold @(Hr tl (refl ? h) ? Hlookup Hfold)
564     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ?HP)) ]
565     ]
566   | normalize in H; normalize     
567     @(fold_eq … True)
568     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
569       [ #z #t' #X #HX @(proj2 ? ? HX)
570       | @H ]
571     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
572     | @(Hl tl (refl ? h) ? Hlookup) normalize
573       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
574       [ //
575       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
576       | @H
577       ]
578     ]
579   ]
580 | #n #b #_ #P #Hlookup #Hf normalize // ]
581qed.
582
583lemma forall_insert_inv2b:
584  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop).
585  (∀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.
586 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ? → ??%%% → ?);
587 [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl | @(proj2 ? ? Hf) ]
588 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #HP #Hf
589   [ normalize in Hf; normalize
590     @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … Hf)
591     [ #Hfold @(Hr tl (refl ? h) ? HP Hfold)
592     | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
593     ]
594   | normalize in H; normalize     
595     @(fold_eq … True)
596     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l))
597       [ #z #t' #X #HX @(proj2 ? ? HX)
598       | @Hf ]
599     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
600     | @(Hl tl (refl ? h) ? HP) normalize
601       @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
602       [ //
603       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
604       | @Hf
605       ]
606     ]
607   ]
608 | #n #b #_ #P #Hlookup #Hf normalize // ]
609qed.
610
611lemma forall_prepare_tree_for_insertion:
612 ∀A:Type[0].∀h:nat.∀b:BitVector h.∀a:A.∀P.
613 P b a →
614 forall A h (prepare_trie_for_insertion A h b a) P.
615 #A #h #b elim b
616 [ #a #P #HP normalize %1 [ @HP | // ]
617 | #h #x #tl #Ha #a #P cases x #HP normalize @Ha @HP
618 ]
619qed.
620
621lemma forall_insert:
622  ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P.
623  forall A n t P → P b a → forall A n (insert A n b a t) P.
624 #A #n #b #a #t generalize in match (refl ? n); elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%);
625 [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/
626 | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #Hf #HP
627   [ normalize in Hf; normalize
628     @(fold_eq A … (fold A … (λx.λa0.λacc.P (true:::x) a0∧acc) r True) … Hf)
629     [ #Hp @(Hr tl (refl ? h) ? Hp HP)
630     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
631     ]
632   | normalize in Hf; normalize
633     @(fold_eq … True)
634     [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0∧acc) l)
635       [ #z #t' #X #HX @(proj2 ? ? HX)
636       | @Hf ]
637     | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
638     | @(Hl tl (refl ? h) ? ? HP)
639       normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True))
640       [ //
641       | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ]
642       | @Hf
643       ]
644     ]
645   ]
646 | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%);
647   [ #b #P #Hf #HP normalize %1 [ @HP | // ]
648   | #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP)
649   ]
650 ]
651qed.
652
653lemma update_fail : ∀A,n,b,a,t.
654  update A n b a t = None ? →
655  lookup_opt A n b t = None ?.
656#A #n elim n
657[ #b @(vector_inv_n … b) #a #t cases (BitVectorTrie_O … t)
658  [ * #x #E >E normalize #NE destruct
659  | #E >E normalize //
660  ]
661| #m #IH #b @(vector_inv_n … b) #hd #tl #a #t cases (BitVectorTrie_Sn … t)
662  [ * #t1 * #t2 #E >E cases hd whd in ⊢ (??%? → ??%?);
663    #X lapply (option_map_none … X) @IH
664  | #E >E normalize //
665  ]
666] qed.
667
668lemma update_lookup_opt_same : ∀A,n,b,a,t,t'.
669  update A n b a t = Some ? t' →
670  lookup_opt A n b t' = Some ? a.
671#A #n elim n
672[ #b #a #t #t' @(vector_inv_n … b)
673  cases (BitVectorTrie_O … t)
674  [ * #x #E >E normalize #E' destruct @refl
675  | #E >E normalize #E' destruct
676  ]
677| #m #IH #b #a #t #t'
678  @(vector_inv_n … b) #bhd #btl
679  cases (BitVectorTrie_Sn … t)
680  [ * #t1 * #t2 #E' >E'
681    whd in ⊢ (??%? → ??%?); cases bhd #U
682    cases (option_map_some ????? U)
683    #tn' * #U' #E'' <E''
684    whd in ⊢ (??%?); whd in ⊢ (??(???%%)?);
685    @(IH … U')
686  | #E >E normalize #E' destruct
687  ]
688] qed.
689
690lemma update_lookup_opt_other : ∀A,n,b,a,t,t'.
691  update A n b a t = Some ? t' →
692  ∀b'. b ≠ b' →
693  lookup_opt A n b' t = lookup_opt A n b' t'.
694#A #n elim n
695[ #b #a #t #t' #E #b'
696  @(vector_inv_n … b) @(vector_inv_n … b')
697  * #NE cases (NE (refl ??))
698| #m #IH #b #a #t #t'
699  @(vector_inv_n … b) #bhd #btl
700  cases (BitVectorTrie_Sn … t)
701  [ * #t1 * #t2 #E >E whd in ⊢ (??%? → ?); cases bhd
702    #U cases (option_map_some ????? U) #tn' * #U' #E' <E'
703    #b' @(vector_inv_n … b') #bhd' #btl'
704    cases bhd'
705    [ 2,3: #_ @refl
706    | *: #NE whd in ⊢ (??%%); whd in ⊢ (??(???%%)(???%%));
707         @(IH … U') % #E'' >E'' in NE; * #H @H @refl
708    ]
709  | #E >E whd in ⊢ (??%? → ?); #NE destruct
710  ]
711] qed.
712
713include "basics/deqsets.ma".
714
715definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
716 λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a.
717
718definition strong_decidable: Prop → Type[0] ≝
719 λP:Prop. P + ¬ P.
720
721lemma strong_decidable_in_codomain:
722 ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A.
723  strong_decidable (in_codomain A n m a).
724 #A #n #m elim m
725 [ normalize #a' #a inversion (a' == a) #H
726   [ %1 %{(VEmpty …)} >(\P H) %
727   | %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ]
728 | -n #n #L #R #Hl #Hr #a
729   cases (Hl a) -Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl
730   cases (Hr a) -Hr [#K %1 cases K #k #H %{(true:::k)}  <H % ] #Hr
731   %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?);
732   normalize nodelta whd in match (tail ???); #abs [ cases Hr | cases Hl ] /3/
733 | #n #A %2 % * #x normalize #abs destruct ]
734qed.
735
736
Note: See TracBrowser for help on using the repository browser.