1 | include "BitVector.ma". |
---|
2 | |
---|
3 | include "basics/bool.ma". |
---|
4 | include "datatypes/sums.ma". |
---|
5 | |
---|
6 | ninductive 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 | |
---|
11 | nlet rec lookup (A: Type[0]) (n: nat) |
---|
12 | (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b |
---|
13 | : A ≝ |
---|
14 | (match b return λx.λ_. x = n → A with |
---|
15 | [ VEmpty ⇒ |
---|
16 | (match t return λx.λ_. O = x → A with |
---|
17 | [ Leaf l ⇒ λ_.l |
---|
18 | | Node h l r ⇒ λK.⊥ |
---|
19 | | Stub s ⇒ λ_.a |
---|
20 | ]) |
---|
21 | | VCons o hd tl ⇒ |
---|
22 | match t return λx.λ_. (S o) = x → A with |
---|
23 | [ Leaf l ⇒ λK.⊥ |
---|
24 | | Node h l r ⇒ |
---|
25 | match hd with |
---|
26 | [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a |
---|
27 | | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a |
---|
28 | ] |
---|
29 | | Stub s ⇒ λ_. a] |
---|
30 | ]) (refl ? n). |
---|
31 | ##[##1,2: ndestruct |##*: napply injective_S; //] |
---|
32 | nqed. |
---|
33 | |
---|
34 | nlet rec prepare_trie_for_insertion (A: Type[0]) (n: nat) |
---|
35 | (b: BitVector n) (a:A) on b |
---|
36 | : BitVectorTrie A n ≝ |
---|
37 | match b with |
---|
38 | [ VEmpty ⇒ Leaf A a |
---|
39 | | VCons o hd tl ⇒ |
---|
40 | match hd with |
---|
41 | [ true ⇒ Node A o (Stub A o) (prepare_trie_for_insertion A o tl a) |
---|
42 | | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o) |
---|
43 | ] |
---|
44 | ]. |
---|
45 | |
---|
46 | nlet rec insert (A: Type[0]) (n: nat) |
---|
47 | (b: BitVector n) (a: A) on b: |
---|
48 | BitVectorTrie A n → BitVectorTrie A n ≝ |
---|
49 | (match b with |
---|
50 | [ VEmpty ⇒ λ_. Leaf A a |
---|
51 | | VCons o hd tl ⇒ λt. |
---|
52 | match t return λy.λ_. S o = y → BitVectorTrie A (S o) with |
---|
53 | [ Leaf l ⇒ λprf.⊥ |
---|
54 | | Node p l r ⇒ λprf. |
---|
55 | match hd with |
---|
56 | [ true ⇒ Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉)) |
---|
57 | | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉) |
---|
58 | ] |
---|
59 | | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a) |
---|
60 | ] (refl ? (S o)) |
---|
61 | ]). |
---|
62 | ##[ ndestruct; |
---|
63 | ##|##*: napply injective_S; // ] |
---|
64 | nqed. |
---|
65 | |
---|
66 | (* |
---|
67 | nlemma insert_lookup_stub: |
---|
68 | ∀A: Type[0]. |
---|
69 | ∀n: nat. |
---|
70 | ∀b: BitVector n. |
---|
71 | ∀t: BitVectorTrie A n. |
---|
72 | ∀a, c: A. |
---|
73 | (lookup A n b (insert A n b a (Stub A n)) a) = a. |
---|
74 | #A n b t a c. |
---|
75 | nelim b. |
---|
76 | //. |
---|
77 | #N H V H2. |
---|
78 | nnormalize. |
---|
79 | @. |
---|
80 | nqed. |
---|
81 | *) |
---|
82 | (* |
---|
83 | nlemma test: |
---|
84 | ∀n: nat. |
---|
85 | ∀b: BitVector n. |
---|
86 | length n b = n. |
---|
87 | #n b. |
---|
88 | nelim b. |
---|
89 | //. |
---|
90 | #N H V IH. |
---|
91 | ncases H. |
---|
92 | |
---|
93 | nlemma insert_lookup_leaf: |
---|
94 | ∀A: Type[0]. |
---|
95 | ∀n: nat. |
---|
96 | ∀b: BitVector n. |
---|
97 | ∀a, c: A. |
---|
98 | ∀t: BitVectorTrie A n. |
---|
99 | lookup A ? b (insert A ? b a t) c = a. |
---|
100 | #A n b a c t. |
---|
101 | nelim b. |
---|
102 | nnormalize. |
---|
103 | @. |
---|
104 | #N H V IH. |
---|
105 | *) |
---|