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