include "ASM/BitVectorTrie.ma". include "ASM/Util.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. let rec set_eq (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: bool ≝ match b return λh. λ_. n = h → bool with [ Stub s ⇒ match c with [ Stub s' ⇒ λ_. eq_nat s s' | _ ⇒ λ_. false ] | Leaf l ⇒ match c with [ Leaf l' ⇒ λ_. true (* dpm: l and l' both unit *) | _ ⇒ λ_. false ] | Node h l r ⇒ match c with [ Node h' l' r' ⇒ λprf. andb (set_eq h l ?) (set_eq h r ?) | _ ⇒ λ_. false ] ] (refl ? n). [ 1: @ r | 2: lapply (injective_S … prf) # H < H @ r' ] 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. definition set_singleton ≝ λn: nat. λb: BitVector n. insert unit n b it (set_empty ?).