include "basics/types.ma". include "utilities/option.ma". include "ASM/BitVector.ma". inductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝ Leaf: A → BitVectorTrie A O | Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) | Stub: ∀n: nat. BitVectorTrie A n. let rec fold (A, B: Type[0]) (n: nat) (f: BitVector n → A → B → B) (t: BitVectorTrie A n) (b: B) on t: B ≝ (match t return λx.λ_.x = n → B with [ Leaf l ⇒ λ_.f (zero ?) l b | Node h l r ⇒ λK. fold A B h (λx.f ((VCons ? h false x)⌈(S h) ↦ n⌉)) l (fold A B h (λx.f ((VCons ? h true x)⌈(S h) ↦ n⌉)) r b) | Stub _ ⇒ λ_.b ]) (refl ? n). @K qed. (* these two can probably be generalized w/r/t the second type and * some sort of equality relationship *) lemma fold_eq: ∀A: Type[0]. ∀n: nat. ∀f. ∀t. ∀P, Q: Prop. (P → Q) → (∀a,t',P,Q.(P → Q) → f a t' P → f a t' Q) → fold A ? n f t P → fold A ? n f t Q. #A #n #f #t #P #Q #H generalize in match (refl ? n) generalize in match H -H; generalize in match Q -Q; generalize in match P -P; elim t in f ⊢ (? → ? → ? → ???% → ? → ???%%%? → ???%%%?) [ #a #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(Hf (zero 0) a P Q HPQ HP) | #h #l #r #Hl #Hr #f #P #Q #HPQ #_ #Hf #HP normalize normalize in HP; @(Hl ? (fold A Prop h (λx.f (true:::x)) r P) (fold A Prop h (λx.f (true:::x)) r Q) ? (refl ? h) ?) [ @(Hr ? P Q HPQ (refl ? h) ?) #a #t' #X #Y #HXY #Hff @(Hf (true:::a) t' X Y HXY Hff) | #a #t' #X #Y #HXY #Hff @(Hf (false:::a) t' X Y HXY Hff) ] | #h #f #P #Q #HPQ #_ #Hf #HP whd in HP; whd @(HPQ HP) ] @HP qed. lemma fold_init: ∀A:Type[0]. ∀n:nat. ∀f. ∀t. ∀P: Prop. (∀a,t',P.f a t' P → P) → fold A Prop n f t P → P. #A #n #f #t #P #H generalize in match (refl ? n) generalize in match H -H; generalize in match P -P; elim t in f ⊢ (? → ? → ???% → ???%%%? → ?) -t [ #a #f #P #Hf #_ normalize @(Hf [[]]) | #h #l #r #Hl #Hr #f #P #Hf #_ normalize #HP @(Hr (λx.f (true:::x))) [ #a #t' #X @(Hf (true:::a) t' X) | @(refl ? h) | @(Hl (λx.f (false:::x))) [ #a #t' #X @(Hf (false:::a) t' X) | @(refl ? h) | @HP ] ] | #h #f #P #Hf #_ normalize // ] qed. definition forall ≝ λA.λn.λt:BitVectorTrie A n.λP.fold ? ? ? (λk.λa.λacc.(P k a) ∧ acc) t True. lemma forall_nodel: ∀A:Type[0]. ∀n:nat. ∀l,r. ∀P:BitVector (S n) → A → Prop. forall A (S n) (Node ? n l r) P → forall A n l (λx.λa.P (false:::x) a). #A #n #l #r #P #Hl whd @(fold_eq A n ? ? (fold A ? n (λk.λa.λacc.P (true:::k) a∧acc) r True) True) [ // | #n #t' #X #Y #HXY #HX %1 [ @(proj1 ? ? HX) | @HXY @(proj2 ? ? HX) ] | whd in Hl @Hl ] qed. lemma forall_noder: ∀A:Type[0]. ∀n:nat. ∀l,r. ∀P:BitVector (S n) → A → Prop. forall A (S n) (Node ? n l r) P → forall A n r (λx.λa.P (true:::x) a). #A #n #l #r #P #Hr whd @(fold_init A n (λk.λa.λacc.P (false:::k) a∧acc) l) [ #n #t' #P #HP @(proj2 ? ? HP) | @Hr ] qed. lemma forall_node: ∀A.∀n.∀l,r.∀P:BitVector (S n) → A → Prop. forall A n l (λx.λa.P (false:::x) a) → forall A n r (λx.λa.P (true:::x) a) → forall A (S n) (Node ? n l r) P. #A #n #l #r #P #Hl #Hr normalize @(fold_eq … True) [ #_ @Hr | #x #t' #X #Y #HXY #HP %1 [ @(proj1 … HP) | @HXY @(proj2 … HP) ] | @Hl ] qed. let rec lookup_opt (A: Type[0]) (n: nat) (b: BitVector n) (t: BitVectorTrie A n) on t : option A ≝ (match t return λx.λ_. BitVector x → option A with [ Leaf l ⇒ λ_.Some ? l | Node h l r ⇒ λb. lookup_opt A ? (tail … b) (if head' … b then r else l) | Stub _ ⇒ λ_.None ? ]) b. definition member ≝ λA. λn. λb: BitVector n. λt: BitVectorTrie A n. match lookup_opt A n b t with [ None ⇒ false | _ ⇒ true ]. definition member_p ≝ λA. λn. λb: BitVector n. λt: BitVectorTrie A n. match lookup_opt A n b t with [ None ⇒ False | _ ⇒ True ]. lemma forall_lookup: ∀A. ∀n. ∀t:BitVectorTrie A n. ∀P:BitVector n → A → Prop. forall A n t P → ∀a:A.∀b.lookup_opt A n b t = Some ? a → P b a. #A #n #t #P generalize in match (refl ? n) elim t in P ⊢ (???% → ??%%? → ? → ? → ??(??%%%)? → ?) [ #x #f #_ #Hf #a #b whd in Hf; #Hb normalize in Hb; destruct >(BitVector_O b) @(proj1 ? ? Hf) | #h #l #r #Hl #Hr #f #_ #Hf #a #b #Hb cases (BitVector_Sn h b) #hd #bla elim bla -bla #tl #Htl >Htl in Hb; #Hb cases hd in Hb; [ #Hb normalize in Hb; @(Hr (λx.λa.f (true:::x) a) (refl ? h)) [ @(forall_noder A h l r f Hf) | @Hb ] | #Hb normalize in Hb; @(Hl (λx.λa.f (false:::x) a) (refl ? h)) [ @(forall_nodel A h l r f Hf) | @Hb ] ] | #n #f #_ #Hf #a #b #Hb normalize in Hb; destruct qed. lemma lookup_forall: ∀A:Type[0].∀n.∀t:BitVectorTrie A n.∀P:BitVector n → A → Prop. (∀a:A.∀b:BitVector n.lookup_opt A n b t = Some ? a → P b a) → forall A n t P. #A #n #t elim t [ #x #P #HP normalize %1 [ @HP normalize @refl | // ] | #h #l #r #Hl #Hr #P #HP @forall_node [ @Hl #a #b #Hlookup @HP normalize @Hlookup | @Hr #a #b #Hlookup @HP normalize @Hlookup ] | #n #P #HP normalize // ] qed. let rec lookup (A: Type[0]) (n: nat) (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b : A ≝ (match b return λx.λ_. x = n → A with [ VEmpty ⇒ (match t return λx.λ_. O = x → A with [ Leaf l ⇒ λ_.l | Node h l r ⇒ λK.⊥ | Stub s ⇒ λ_.a ]) | VCons o hd tl ⇒ match t return λx.λ_. (S o) = x → A with [ Leaf l ⇒ λK.⊥ | Node h l r ⇒ match hd with [ true ⇒ λK. lookup A h (tl⌈o ↦ h⌉) r a | false ⇒ λK. lookup A h (tl⌈o ↦ h⌉) l a ] | Stub s ⇒ λ_. a] ]) (refl ? n). [1,2: destruct |*: @ injective_S // ] qed. let rec prepare_trie_for_insertion (A: Type[0]) (n: nat) (b: BitVector n) (a:A) on b : BitVectorTrie A n ≝ match b with [ VEmpty ⇒ Leaf A a | VCons o hd tl ⇒ match hd with [ true ⇒ Node A o (Stub A o) (prepare_trie_for_insertion A o tl a) | false ⇒ Node A o (prepare_trie_for_insertion A o tl a) (Stub A o) ] ]. let rec insert (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → BitVectorTrie A n ≝ (match b with [ VEmpty ⇒ λ_. Leaf A a | VCons o hd tl ⇒ λt. match t return λy.λ_. S o = y → BitVectorTrie A (S o) with [ Leaf l ⇒ λprf.⊥ | Node p l r ⇒ λprf. match hd with [ true ⇒ Node A o (l⌈p ↦ o⌉) (insert A o tl a (r⌈p ↦ o⌉)) | false ⇒ Node A o (insert A o tl a (l⌈p ↦ o⌉)) (r⌈p ↦ o⌉) ] | Stub p ⇒ λprf. (prepare_trie_for_insertion A ? (hd:::tl) a) ] (refl ? (S o)) ]). [ destruct |*: @ injective_S // ] qed. let rec update (A: Type[0]) (n: nat) (b: BitVector n) (a: A) on b: BitVectorTrie A n → option (BitVectorTrie A n) ≝ (match b with [ VEmpty ⇒ λt. match t return λy.λ_. O = y → option (BitVectorTrie A O) with [ Leaf _ ⇒ λ_. Some ? (Leaf A a) | Stub _ ⇒ λ_. None ? | Node _ _ _ ⇒ λprf. ⊥ ] (refl ? O) | VCons o hd tl ⇒ λt. match t return λy.λ_. S o = y → option (BitVectorTrie A (S o)) with [ Leaf l ⇒ λprf.⊥ | Node p l r ⇒ λprf. match hd with [ true ⇒ option_map ?? (λv. Node A o (l⌈p ↦ o⌉) v) (update A o tl a (r⌈p ↦ o⌉)) | false ⇒ option_map ?? (λv. Node A o v (r⌈p ↦ o⌉)) (update A o tl a (l⌈p ↦ o⌉)) ] | Stub p ⇒ λprf. None ? ] (refl ? (S o)) ]). [ 1,2: destruct |*: @ injective_S @sym_eq @prf ] qed. let rec merge (A: Type[0]) (n: nat) (b: BitVectorTrie A n) on b: BitVectorTrie A n → BitVectorTrie A n ≝ match b return λx. λ_. BitVectorTrie A x → BitVectorTrie A x with [ Stub _ ⇒ λc. c | Leaf l ⇒ λc. match c with [ Leaf a ⇒ Leaf ? a | _ ⇒ Leaf ? l ] | Node p l r ⇒ λc. (match c return λx. λ_. x = (S p) → BitVectorTrie A (S p) with [ Node p' l' r' ⇒ λprf. Node ? ? (merge ?? l (l'⌈p' ↦ p⌉)) (merge ?? r (r'⌈p' ↦ p⌉)) | Stub _ ⇒ λprf. Node ? p l r | Leaf _ ⇒ λabsd. ? ] (refl ? (S p))) ]. [1: destruct(absd) |2,3: @ injective_S assumption ] qed. lemma BitVectorTrie_O: ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) [ #w #_ %1 %[@w] % | #n #l #r #abs @⊥ destruct(abs) | #n #EQ %2 >EQ %] qed. lemma BitVectorTrie_Sn: ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) [ #m #abs @⊥ destruct(abs) | #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // | #m #EQ %2 // ] qed. lemma lookup_prepare_trie_for_insertion_hit: ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. lookup … b (prepare_trie_for_insertion … b v) a = v. #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // qed. lemma lookup_insert_hit: ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. lookup … b (insert … b v t) a = v. #A #a #v #n #b elim b -b -n // #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) [ * #l * #r #JMEQ >JMEQ cases hd normalize // | #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] qed. lemma lookup_prepare_trie_for_insertion_miss: ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n. (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a. #A #a #v #n #c elim c [ #b >(BitVector_O … b) normalize #abs @⊥ // | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ cases hd cases hd' normalize [2,3: #_ cases tl' // |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]] qed. lemma lookup_insert_miss: ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. #A #a #v #n #c elim c -c -n [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ #t cases(BitVectorTrie_Sn … t) [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // | #JMEQ >JMEQ cases hd cases hd' #H normalize in H; [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize [3,4: cases tl' // | *: @lookup_prepare_trie_for_insertion_miss //]]] qed. lemma lookup_stub: ∀A.∀n.∀b.∀a. lookup A n b (Stub A ?) a = a. #A #n #b #a cases n in b ⊢ (??(??%%%?)?) [ #b >(BitVector_O b) normalize @refl | #h #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd [ normalize @refl | normalize @refl ] ] qed. lemma lookup_opt_lookup: ∀A:Type[0].∀n:nat.∀b:BitVector n.∀t:BitVectorTrie A n.∀a:A. lookup_opt A n b t = Some A a → ∀x.lookup A n b t x = a. #A #n #b #t #a generalize in match (refl ? n) elim t in b ⊢ (???% → ??(??%%%)? → ? → ?) [ #a #B #_ #H #x normalize in H; >(BitVector_O B) normalize destruct @refl | #h #l #r #Hl #Hr #b #_ #H #x cases (BitVector_Sn h b) #hd #X elim X; -X; #tl #Hb >Hb >Hb in H; cases hd [ normalize #Hlookup @(Hr ? (refl ? h)) @Hlookup | normalize #Hlookup @(Hl ? (refl ? h)) @Hlookup ] | #n #B #_ #H #x normalize in H; destruct ] qed. lemma lookup_opt_prepare_trie_for_insertion_hit: ∀A:Type[0].∀v:A.∀n.∀b:BitVector n. lookup_opt … b (prepare_trie_for_insertion … b v) = Some A v. #A #v #n #b elim b // #m #hd #tl #IH cases hd normalize // qed. lemma lookup_opt_insert_hit: ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. lookup_opt … b (insert … b v t) = Some A v. #A #v #n #b #t elim t in b ⊢ (??(??%%%)?) [ #x #b >(BitVector_O b) normalize @refl | #h #l #r #Hl #Hr #b cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd [ normalize @Hr | normalize @Hl ] | #n' #b cases n' in b ⊢ ? [ #b >(BitVector_O b) normalize @refl | #m #b cases (BitVector_Sn m b) #hd #X elim X -X; #tl #Hb >Hb cases hd normalize @lookup_opt_prepare_trie_for_insertion_hit ] ] qed. lemma forall_insert_inv1: ∀A.∀n.∀b.∀a.∀t.∀P. forall A n (insert A n b a t) P → P b a. #A #n #b #a #t #P #H @(forall_lookup ? ? (insert A n b a t)) [ @H | >(lookup_opt_insert_hit A ? n b) @(refl ? (Some A a)) ] qed. lemma forall_insert_inv2a: ∀A:Type[0].∀n:nat.∀b.∀a.∀t.∀P. lookup_opt A n b t = (None A) → forall A n (insert A n b a t) P → forall A n t P. #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → ? → ??(??%%%)? → ??%%% → ??%%%) [ #x #b #_ #P >(BitVector_O b) normalize #H destruct | #h #l #r #Hl #Hr #b #_ #P cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #Hlookup #H [ normalize in H; normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … H) [ #Hfold @(Hr tl (refl ? h) ? Hlookup Hfold) | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ?HP)) ] ] | normalize in H; normalize @(fold_eq … True) [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l)) [ #z #t' #X #HX @(proj2 ? ? HX) | @H ] | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] | @(Hl tl (refl ? h) ? Hlookup) normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True)) [ // | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] | @H ] ] ] | #n #b #_ #P #Hlookup #Hf normalize // ] qed. lemma forall_insert_inv2b: ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P:(BitVector n → A → Prop). (∀x.(lookup_opt A n b t = Some A x) → P b x) → forall A n (insert A n b a t) P → forall A n t P. #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ? → ??%%% → ?) [ #x #b #_ #P >(BitVector_O b) normalize #HP #Hf %1 [ @HP @refl | @(proj2 ? ? Hf) ] | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #HP #Hf [ normalize in Hf; normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) (insert … tl a r) True) … Hf) [ #Hfold @(Hr tl (refl ? h) ? HP Hfold) | #x #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] ] | normalize in H; normalize @(fold_eq … True) [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0 ∧ acc) (insert A h tl a l)) [ #z #t' #X #HX @(proj2 ? ? HX) | @Hf ] | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] | @(Hl tl (refl ? h) ? HP) normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True)) [ // | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] | @Hf ] ] ] | #n #b #_ #P #Hlookup #Hf normalize // ] qed. lemma forall_prepare_tree_for_insertion: ∀A:Type[0].∀h:nat.∀b:BitVector h.∀a:A.∀P. P b a → forall A h (prepare_trie_for_insertion A h b a) P. #A #h #b elim b [ #a #P #HP normalize %1 [ @HP | // ] | #h #x #tl #Ha #a #P cases x #HP normalize @Ha @HP ] qed. lemma forall_insert: ∀A:Type[0].∀n:nat.∀b:BitVector n.∀a:A.∀t.∀P. forall A n t P → P b a → forall A n (insert A n b a t) P. #A #n #b #a #t generalize in match (refl ? n) elim t in b ⊢ (???% → % → ??%%% → %%? → ??%%%) [ #x #b #_ #P >(BitVector_O b) normalize #H1 #H2 /2/ | #h #l #r #Hl #Hr #b #_ cases (BitVector_Sn h b) #hd #X elim X -X; #tl #Hb >Hb cases hd #P #Hf #HP [ normalize in Hf; normalize @(fold_eq A … (fold A … (λx.λa0.λacc.P (true:::x) a0∧acc) r True) … Hf) [ #Hp @(Hr tl (refl ? h) ? Hp HP) | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] ] | normalize in Hf; normalize @(fold_eq … True) [ #_ @(fold_init A h (λx.λa0.λacc.P (false:::x) a0∧acc) l) [ #z #t' #X #HX @(proj2 ? ? HX) | @Hf ] | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] | @(Hl tl (refl ? h) ? ? HP) normalize @(fold_eq … (fold A ? ? (λx.λa0.λacc.P (true:::x) a0∧acc) r True)) [ // | #z #t' #X #Y #HXY #HP %1 [ @(proj1 ? ? HP) | @(HXY (proj2 ? ? HP)) ] | @Hf ] ] ] | #n #b #_ elim b in t ⊢ (% → ? → ? → ??%%%) [ #b #P #Hf #HP normalize %1 [ @HP | // ] | #h #hd #tl #H #b #P #Hf cases hd #HP normalize @(forall_prepare_tree_for_insertion A h tl a ? HP) ] ] qed.