include "cerco/BitVectorTrie.ma". definition BitVectorTrieSet ≝ BitVectorTrie unit. let rec set_member (n: nat) (p: Vector bool n) (b: BitVectorTrieSet n) on p: bool ≝ (match p return λx. λ_. n = x → bool with [ VEmpty ⇒ ( match b return λx. λ_. x = 0 → bool with [ Leaf _ ⇒ λprf. true | Stub _ ⇒ λprf. false | _ ⇒ λabsd. ? ]) | VCons o hd tl ⇒ (match b return λx. λ_. x = S o → bool with [ Leaf _ ⇒ λabsd. ? | Stub _ ⇒ λprf. false | Node p l r ⇒ match hd with [ true ⇒ λprf: S p = S o. set_member o tl (r⌈p ↦ o⌉) | false ⇒ λprf: S p = S o. set_member o tl (l⌈p ↦ o⌉) ] ]) ]) (refl ? n). [3,4: @ injective_S assumption |1,2: destruct ] qed. let rec set_union (n: nat) (b: BitVectorTrieSet n) on b: BitVectorTrieSet n → BitVectorTrieSet n ≝ match b return λx. λ_. BitVectorTrieSet x → BitVectorTrieSet x with [ Stub _ ⇒ λc. c | Leaf l ⇒ λc. Leaf ? l | Node p l r ⇒ λc. (match c return λx. λ_. x = (S p) → BitVectorTrieSet (S p) with [ Node p' l' r' ⇒ λprf. Node ? ? (set_union ? l (l'⌈p' ↦ p⌉)) (set_union ? r (r'⌈p' ↦ p⌉)) | Stub _ ⇒ λprf. Node ? p l r | Leaf _ ⇒ λabsd. ? ] (refl ? (S p))) ]. [1: destruct(absd) |2,3: @ injective_S assumption ] qed. definition set_insert ≝ λn: nat. λb: BitVector n. λs: BitVectorTrieSet n. insert unit n b it s. definition set_empty ≝ λn. Stub unit n.