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.

(*
let rec set_diff (n: nat) (b: BitVectorTrieSet n) (c: BitVectorTrieSet n) on b: BitVectorTrieSet n ≝
  match b with
  [ Stub ⇒ 
*)

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 ?).