source: src/ASM/BitVectorTrie.ma @ 985

Last change on this file since 985 was 985, checked in by sacerdot, 8 years ago

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File size: 6.4 KB
Line 
1include "basics/types.ma".
2
3include "utilities/option.ma".
4include "ASM/BitVector.ma".
5
6inductive 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
11axiom 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
19let 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
28let 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  ]
54qed.
55
56let 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
66let 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  ]
85qed.
86
87let 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  ]
109qed.
110
111let 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  ]
129qed.
130
131lemma 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 @⊥ //
136  | #n #EQ %2 >EQ %]
137qed.
138
139lemma 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 @⊥ //
143  | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //
144  | #m #EQ %2 // ]
145qed.
146
147lemma 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 //
151qed.
152 
153lemma 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 ]
160qed.
161
162lemma 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/ ]]
171qed.
172 
173lemma 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 //]]]
185qed.
Note: See TracBrowser for help on using the repository browser.