public
Last active

Implementation of Patrica Tries in Coq

  • Download Gist
PatriciaTrie.v
Coq
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
Require Import Bvector.
Require Import Eqdep_dec.
 
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
 
Definition bCompare (x y : bool) : comparison :=
match x, y with
| false, false => Eq
| false, true => Lt
| true , false => Gt
| true , true => Eq
end.
 
Lemma bCompare_CompOpp : forall b1 b2, bCompare b1 b2 = CompOpp (bCompare b2 b1).
Proof. intros [|] [|]; reflexivity. Qed.
 
Lemma bCompare_refl : forall b, bCompare b b = Eq.
Proof. intros [|]; reflexivity. Qed.
 
Lemma bCompare_elim : forall P : bool -> bool -> comparison -> Type,
(forall b, P b b Eq) ->
(P false true Lt) ->
(P true false Gt) ->
forall b1 b2, P b1 b2 (bCompare b1 b2).
Proof.
intros P H0 H1 H2 [|] [|]; auto.
Qed.
 
Lemma vector_rect2:
forall (A : Type) (P : forall n : nat, vector A n -> vector A n -> Type),
P 0 (Vnil A) (Vnil A) ->
(forall (a1 a2 : A) (n : nat) (v1 v2 : vector A n),
P n v1 v2 -> P (S n) (Vcons A a1 n v1) (Vcons A a2 n v2)) ->
forall (n : nat) (v1 v2 : vector A n), P n v1 v2.
Proof.
intros A P H0 H1 n v1 v2.
change v2 with (eq_rect n (vector A) v2 n (eq_refl n)).
generalize (eq_refl n).
set (a:=n).
unfold a at 1 4.
revert v2.
induction v1; intros v2; dependent inversion v2; intros e.
replace e with (refl_equal 0);[|apply UIP_dec; decide equality].
assumption.
replace e with (refl_equal (S n));[|apply UIP_dec; decide equality].
apply H1.
apply (IHv1 v (refl_equal n)).
Qed.
 
Lemma vector_dec : forall A, (forall a1 a2 : A, {a1 = a2} + {a1 <> a2}) ->
forall n (v1 v2 : vector A n), {v1 = v2} + {v1 <> v2}.
Proof.
intros A A_dec.
set (P := fun n (v1 v2 : vector A n) => {v1 = v2} + {v1 <> v2}).
apply (vector_rect2 (A := A) (P := P)).
left; reflexivity.
intros a1 a2 n v1 v2 [IH|IH].
rewrite IH.
case (A_dec a1 a2); intros Ha.
rewrite Ha.
left; reflexivity.
right; intros H.
apply Ha.
injection H; auto.
right; intros H.
apply IH.
refine (@inj_pair2_eq_dec _ _ (fun n => vector A n) _ _ _ _).
decide equality.
injection H.
auto.
Defined.
 
Section PatriciaTrie.
 
Variable A:Set.
 
Inductive PatriciaTrieR : nat -> Set :=
| Tip : A -> PatriciaTrieR 0
| Arm : bool -> forall n, PatriciaTrieR n -> PatriciaTrieR (S n)
| Branch : forall n, PatriciaTrieR n -> PatriciaTrieR n -> PatriciaTrieR (S n).
 
Definition PatriciaTrie n := option (PatriciaTrieR n).
 
Fixpoint singletonR (n : nat) (k:Bvector n) (v:A) : PatriciaTrieR n :=
match k in vector _ n return PatriciaTrieR n with
| Vnil => Tip v
| Vcons r m k' => Arm r (singletonR k' v)
end.
 
Definition singleton n k v : PatriciaTrie n := option_map (singletonR k) v.
 
Fixpoint getR n (k:Bvector n) : PatriciaTrieR n -> option A :=
match k with
| Vnil => fun t =>
match t with
| Tip v => Some v
| _ => @id
end
| Vcons b n k' => fun t =>
match t with
| Arm b0 m t0 => fun rec =>
match bCompare b b0 with
| Eq => rec t0
| Lt | Gt => None
end
| Branch m t0 t1 => fun rec =>
if b then rec t1 else rec t0
end (fun t => getR k' t)
end.
 
Definition get n (k:Bvector n) (ot:PatriciaTrie n) : option A :=
match ot with
| Some t => getR k t
| None => None
end.
 
Fixpoint setR n (k:Bvector n) : PatriciaTrieR n -> option A -> PatriciaTrie n :=
match k with
| Vnil => fun t =>
match t with
| Tip v => option_map Tip
| _ => @id
end
| Vcons b n k' => fun t =>
match t with
| Arm b0 m t0 => fun k' rec =>
match bCompare b b0 with
| Lt => fun ov =>
match ov with
| None => Some (Arm b0 t0)
| Some v => Some (Branch (singletonR k' v) t0)
end
| Eq => fun ov => option_map (@Arm b0 m) (rec t0 ov)
| Gt => fun ov =>
match ov with
| None => Some (Arm b0 t0)
| Some v => Some (Branch t0 (singletonR k' v))
end
end
| Branch m t0 t1 => fun _ rec =>
if b
then
fun ov => Some
match rec t1 ov with
| None => Arm false t0
| Some t1' => Branch t0 t1'
end
else
fun ov => Some
match rec t0 ov with
| None => Arm true t1
| Some t0' => Branch t0' t1
end
end k' (fun t => setR k' t)
end.
 
Definition set n (k:Bvector n) (ot : PatriciaTrie n) : option A -> PatriciaTrie n :=
match ot with
| Some t => setR k t
| None => option_map (singletonR k)
end.
 
Lemma trieR_nonempty : forall n (t : PatriciaTrieR n), {p : (Bvector n*A) | getR (fst p) t = Some (snd p)}.
Proof.
intros n t.
induction t.
exists (pair (Vnil _) a).
reflexivity.
destruct IHt as [[k a] IHt].
exists (pair (Vcons _ b _ k) a).
simpl; rewrite bCompare_refl.
assumption.
destruct IHt1 as [[k a] IHt].
exists (pair (Vcons _ false _ k) a).
assumption.
Qed.
 
Lemma trie_ext : forall n (ot1 ot2 : PatriciaTrie n), (forall k, get k ot1 = get k ot2) -> ot1 = ot2.
Proof.
assert (L1 : forall n (t : PatriciaTrieR n), ~(forall k : Bvector n, getR k t = None)).
intros n t H.
destruct (trieR_nonempty t) as [[k a] Hk].
rewrite H in Hk.
discriminate.
intros n [t1|] [t2|] Hot;
[|elim (L1 _ t1)|elim (L1 _ t2);symmetry|reflexivity]; try firstorder.
apply f_equal.
revert Hot.
change t2 with (eq_rec n PatriciaTrieR t2 n (eq_refl n)).
generalize (eq_refl n).
set (a:=n).
unfold a at 1 8 11.
revert t2.
induction t1; dependent inversion_clear t2;
(intros E; elim E using K_dec_set; try decide equality; simpl; intros Hot).
generalize (Hot (Vnil _)); simpl; congruence.
generalize (fun (k : Bvector n) => Hot (Vcons _ b _ k)).
simpl.
rewrite bCompare_refl.
apply bCompare_elim; try (intros Hot'; elim (L1 _ t1); congruence).
intros b1 Hot'.
apply f_equal.
apply (IHt1 p (refl_equal n)).
assumption.
elim (L1 _ (if b then p else p0)).
intros k.
generalize (Hot (Vcons _ (negb b) _ k)).
case b; simpl; congruence.
elim (L1 _ (if b then t1_1 else t1_2)).
intros k.
generalize (Hot (Vcons _ (negb b) _ k)).
case b; simpl; congruence.
apply f_equal2.
apply (IHt1_1 _ (refl_equal n)).
intros k; apply (Hot (Vcons _ false _ k)).
apply (IHt1_2 _ (refl_equal n)).
intros k; apply (Hot (Vcons _ true _ k)).
Qed.
 
Lemma getR_singletonR : forall n (k : Bvector n) nv, getR k (singletonR k nv) = Some nv.
Proof.
intros n k nv.
induction k as [|b m k].
reflexivity.
case b; auto.
Qed.
 
Theorem lens2 : forall n (k : Bvector n) ot nv, get k (set k ot nv) = nv.
Proof.
intros n k [t|] nv; simpl;
[|destruct nv as [nv|]; simpl; auto using getR_singletonR].
change t with (eq_rec n PatriciaTrieR t n (eq_refl n)).
generalize (eq_refl n).
set (a:=n).
unfold a at 1 5.
revert t.
induction k as [|b m k].
intros t;dependent inversion t.
intros E; elim E using K_dec_set; try decide equality.
destruct nv; reflexivity.
intros t;dependent inversion t;
intros E; elim E using K_dec_set; try decide equality;
simpl (eq_rec _ _ _ _ _);
pose (IHkp := fun p => IHk p (refl_equal m));
simpl in IHkp.
case b; case b0;
destruct nv as [nv|]; simpl; try auto using getR_singletonR;
apply (fun x => eq_trans x (IHkp p));
case (setR _ _ _); reflexivity.
case b;
[apply (fun x => eq_trans x (IHkp p0))
|apply (fun x => eq_trans x (IHkp p))
]; simpl; case (setR _ _ _); reflexivity.
Qed.
 
Lemma getR_singletonR_indep : forall n (k1 k2 : Bvector n) nv, k1 <> k2 -> getR k1 (singletonR k2 nv) = None.
Proof.
set (P := fun n (k1 k2 : Bvector n) => forall nv : A,
k1 <> k2 -> getR k1 (singletonR k2 nv) = None).
apply (vector_rect2 (A:=bool) (P:=P)).
intros nv.
congruence.
unfold P; simpl.
intros b1 b2.
apply bCompare_elim; try reflexivity.
intros b n k1 k2 IH nv Hk.
apply IH.
congruence.
Qed.
 
Theorem get_indep : forall n (k1 k2 : Bvector n) ot nv, k1 <> k2 -> get k1 (set k2 ot nv) = get k1 ot.
Proof.
set (P := fun n (k1 k2 : Bvector n) => forall ot nv,
k1 <> k2 -> get k1 (set k2 ot nv) = get k1 ot).
apply (vector_rect2 (A:=bool) (P:=P)); unfold P.
congruence.
intros b1 b2 n k1 k2 IH [t|] nv Hk;
[|destruct nv as [nv|]; simpl;
[revert Hk; apply bCompare_elim|];
try (intros b Hk; apply getR_singletonR_indep);
congruence].
change t with (eq_rec (S n) PatriciaTrieR t (S n) (eq_refl (S n))).
generalize (eq_refl (S n)).
set (a:=(S n)).
unfold a at 1 6 10.
dependent inversion t;
intros E; elim E using K_dec_set; try decide equality;
simpl (eq_rec _ _ _ _ _).
revert Hk.
simpl.
apply bCompare_elim.
intros b0.
apply bCompare_elim.
intros b3 Hk.
assert (IHp := (IH (Some p) nv)).
simpl in IHp.
rewrite <- IHp by congruence.
destruct (setR k2 p nv);
[simpl; rewrite bCompare_refl|]; reflexivity.
destruct (setR k2 p nv); reflexivity.
destruct (setR k2 p nv); reflexivity.
destruct b1;
destruct nv; try reflexivity.
intros Hk.
apply getR_singletonR_indep.
congruence.
destruct b1;
destruct nv; try reflexivity.
intros Hk.
apply getR_singletonR_indep.
congruence.
unfold set.
destruct b1.
assert (IHp0 := (IH (Some p0) nv)).
simpl in IHp0.
destruct b2; simpl.
rewrite <- IHp0 by congruence.
destruct (setR k2 p0 nv); reflexivity.
destruct (setR k2 p nv); reflexivity.
assert (IHp := (IH (Some p) nv)).
simpl in IHp.
destruct b2; simpl.
destruct (setR k2 p0 nv); reflexivity.
rewrite <- IHp by congruence.
destruct (setR k2 p nv); reflexivity.
Qed.
 
Theorem lens1 : forall n (k : Bvector n) ot, set k ot (get k ot) = ot.
Proof.
intros n k ot.
apply trie_ext.
intros k'.
case (vector_dec bool_dec k k').
intros eq; rewrite <- eq; clear eq k'.
rewrite !lens2; reflexivity.
intros Hk.
rewrite !get_indep; congruence.
Qed.
 
Theorem lens3 : forall n (k : Bvector n) ot nv1 nv2, set k (set k ot nv1) nv2 = set k ot nv2.
Proof.
intros n k ot nv1 nv2.
apply trie_ext.
intros k'.
case (vector_dec bool_dec k k').
intros eq; rewrite <- eq; clear eq k'.
rewrite !lens2; reflexivity.
intros Hk.
rewrite !get_indep; congruence.
Qed.
 
Theorem set_indep : forall n (k1 k2 : Bvector n) ot nv1 nv2, k1 <> k2 ->
set k2 (set k1 ot nv1) nv2 = set k1 (set k2 ot nv2) nv1.
Proof.
intros n k1 k2 ot nv1 nv2 Hk.
apply trie_ext.
intros k3.
case (vector_dec bool_dec k3 k2); intros Hk'.
rewrite Hk'; clear k3 Hk'.
rewrite lens2, get_indep, lens2; congruence.
case (vector_dec bool_dec k3 k1); intros Hk''.
rewrite Hk''; clear k3 Hk' Hk''.
rewrite lens2, get_indep, lens2; congruence.
rewrite !get_indep; congruence.
Qed.
 
End PatriciaTrie.

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.