1 | include "basics/types.ma". |
---|
2 | |
---|
3 | include "utilities/option.ma". |
---|
4 | include "ASM/BitVector.ma". |
---|
5 | |
---|
6 | inductive 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 | axiom fold: |
---|
12 | ∀A, B: Type[0]. |
---|
13 | ∀n: nat. |
---|
14 | ∀f: BitVector n → A → B → B. |
---|
15 | ∀t: BitVectorTrie A n. |
---|
16 | ∀b: B. |
---|
17 | B. |
---|
18 | |
---|
19 | let rec lookup_opt (A: Type[0]) (n: nat) |
---|
20 | (b: BitVector n) (t: BitVectorTrie A n) on t |
---|
21 | : option A ≝ |
---|
22 | (match t return λx.λ_. BitVector x → option A with |
---|
23 | [ Leaf l ⇒ λ_.Some ? l |
---|
24 | | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l) |
---|
25 | | Stub _ ⇒ λ_.None ? |
---|
26 | ]) b. |
---|
27 | |
---|
28 | let rec lookup (A: Type[0]) (n: nat) |
---|
29 | (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b |
---|
30 | : A ≝ |
---|
31 | (match b return λx.λ_. x = n → A with |
---|
32 | [ VEmpty ⇒ |
---|
33 | (match t return λx.λ_. O = x → A with |
---|
34 | [ Leaf l ⇒ λ_.l |
---|
35 | | Node h l r ⇒ λK.⊥ |
---|
36 | | Stub s ⇒ λ_.a |
---|
37 | ]) |
---|
38 | | VCons o hd tl ⇒ |
---|
39 | match t return λx.λ_. (S o) = x → A with |
---|
40 | [ Leaf l ⇒ λK.⊥ |
---|
41 | | Node h l r ⇒ |
---|
42 | match hd with |
---|
43 | [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a |
---|
44 | | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a |
---|
45 | ] |
---|
46 | | Stub s ⇒ λ_. a] |
---|
47 | ]) (refl ? n). |
---|
48 | [1,2: |
---|
49 | destruct |
---|
50 | |*: |
---|
51 | @ injective_S |
---|
52 | // |
---|
53 | ] |
---|
54 | qed. |
---|
55 | |
---|
56 | let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝ |
---|
57 | match b with |
---|
58 | [ VEmpty ⇒ Leaf A a |
---|
59 | | VCons o hd tl ⇒ |
---|
60 | match hd with |
---|
61 | [ true ⇒ Node A o (Stub A o) (prepare_trie_for_insertion A o tl a) |
---|
62 | | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o) |
---|
63 | ] |
---|
64 | ]. |
---|
65 | |
---|
66 | let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝ |
---|
67 | (match b with |
---|
68 | [ VEmpty ⇒ λ_. Leaf A a |
---|
69 | | VCons o hd tl ⇒ λt. |
---|
70 | match t return λy.λ_. S o = y → BitVectorTrie A (S o) with |
---|
71 | [ Leaf l ⇒ λprf.⊥ |
---|
72 | | Node p l r ⇒ λprf. |
---|
73 | match hd with |
---|
74 | [ true ⇒ Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉)) |
---|
75 | | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉) |
---|
76 | ] |
---|
77 | | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a) |
---|
78 | ] (refl ? (S o)) |
---|
79 | ]). |
---|
80 | [ destruct |
---|
81 | |*: |
---|
82 | @ injective_S |
---|
83 | // |
---|
84 | ] |
---|
85 | qed. |
---|
86 | |
---|
87 | let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝ |
---|
88 | (match b with |
---|
89 | [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with |
---|
90 | [ Leaf _ ⇒ λ_. Some ? (Leaf A a) |
---|
91 | | Stub _ ⇒ λ_. None ? |
---|
92 | | Node _ _ _ ⇒ λprf. ⊥ |
---|
93 | ] (refl ? O) |
---|
94 | | VCons o hd tl ⇒ λt. |
---|
95 | match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with |
---|
96 | [ Leaf l ⇒ λprf.⊥ |
---|
97 | | Node p l r ⇒ λprf. |
---|
98 | match hd with |
---|
99 | [ true ⇒ option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉)) |
---|
100 | | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉)) |
---|
101 | ] |
---|
102 | | Stub p ⇒ λprf. None ? |
---|
103 | ] (refl ? (S o)) |
---|
104 | ]). |
---|
105 | [ 1,2: destruct |
---|
106 | |*: |
---|
107 | @ injective_S @sym_eq @prf |
---|
108 | ] |
---|
109 | qed. |
---|
110 | |
---|
111 | let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝ |
---|
112 | match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with |
---|
113 | [ Stub _ ⇒ λc. c |
---|
114 | | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ] |
---|
115 | | Node p l r ⇒ |
---|
116 | λc. |
---|
117 | (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with |
---|
118 | [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉)) |
---|
119 | | Stub _ ⇒ λprf. Node ? p l r |
---|
120 | | Leaf _ ⇒ λabsd. ? |
---|
121 | ] (refl ? (S p))) |
---|
122 | ]. |
---|
123 | [1: |
---|
124 | destruct(absd) |
---|
125 | |2,3: |
---|
126 | @ injective_S |
---|
127 | assumption |
---|
128 | ] |
---|
129 | qed. |
---|
130 | |
---|
131 | lemma BitVectorTrie_O: |
---|
132 | ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. |
---|
133 | #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) |
---|
134 | [ #w #_ %1 %[@w] % |
---|
135 | | #n #l #r #abs @⊥ destruct(abs) |
---|
136 | | #n #EQ %2 >EQ %] |
---|
137 | qed. |
---|
138 | |
---|
139 | lemma BitVectorTrie_Sn: |
---|
140 | ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). |
---|
141 | #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) |
---|
142 | [ #m #abs @⊥ destruct(abs) |
---|
143 | | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // |
---|
144 | | #m #EQ %2 // ] |
---|
145 | qed. |
---|
146 | |
---|
147 | lemma lookup_prepare_trie_for_insertion_hit: |
---|
148 | ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. |
---|
149 | lookup … b (prepare_trie_for_insertion … b v) a = v. |
---|
150 | #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // |
---|
151 | qed. |
---|
152 | |
---|
153 | lemma lookup_insert_hit: |
---|
154 | ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. |
---|
155 | lookup … b (insert … b v t) a = v. |
---|
156 | #A #a #v #n #b elim b -b -n // |
---|
157 | #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) |
---|
158 | [ * #l * #r #JMEQ >JMEQ cases hd normalize // |
---|
159 | | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] |
---|
160 | qed. |
---|
161 | |
---|
162 | lemma lookup_prepare_trie_for_insertion_miss: |
---|
163 | ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n. |
---|
164 | (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a. |
---|
165 | #A #a #v #n #c elim c |
---|
166 | [ #b >(BitVector_O … b) normalize #abs @⊥ // |
---|
167 | | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ |
---|
168 | cases hd cases hd' normalize |
---|
169 | [2,3: #_ cases tl' // |
---|
170 | |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]] |
---|
171 | qed. |
---|
172 | |
---|
173 | lemma lookup_insert_miss: |
---|
174 | ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. |
---|
175 | (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. |
---|
176 | #A #a #v #n #c elim c -c -n |
---|
177 | [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // |
---|
178 | | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ |
---|
179 | #t cases(BitVectorTrie_Sn … t) |
---|
180 | [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; |
---|
181 | [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // |
---|
182 | | #JMEQ >JMEQ cases hd cases hd' #H normalize in H; |
---|
183 | [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize |
---|
184 | [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]] |
---|
185 | qed. |
---|