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