bspset.lean

import tactic 
universe u

/-- 
The term *Dense* means that a given subset contains all the elements of its particular
bounds. E.g. the whole set would be dense w.r.t. the bounds of the whole space. Or
if a set represents an interval [a, b), then it would be dense, if there are no holes in it,
i.e. the set is represented exactly using the current bounds.
-/
mutual inductive bsp_set, sparse_node
with bsp_set : Type
| empty
| dense
| sparse (root : sparse_node)
with sparse_node : Type
| dense_empty
| empty_dense
| left_sparse (left : sparse_node) (right : bsp_set)
| right_sparse (left : bsp_set) (right : sparse_node)
open bsp_set
open sparse_node

def sparse_node.left : sparse_node → bsp_set
| dense_empty := dense
| empty_dense := empty
| (left_sparse left _) := sparse left
| (right_sparse left _) := left

def sparse_node.right : sparse_node → bsp_set
| dense_empty := empty
| empty_dense := dense
| (left_sparse _ right) := right
| (right_sparse _ right) := sparse right

@[simp]
mutual def sparse_node_size, bsp_set_size
with sparse_node_size : sparse_node → ℕ 
| (left_sparse left right) := sparse_node_size left + bsp_set_size right
| (right_sparse left right) := bsp_set_size left + sparse_node_size right
| _ := 2
with bsp_set_size : bsp_set → ℕ
| (sparse root) := sparse_node_size root 
| _ := 1

instance sparse_node_has_sizeof : has_sizeof sparse_node := ⟨sparse_node_size⟩ 
instance bsp_set_has_sizeof : has_sizeof bsp_set := ⟨bsp_set_size⟩ 

lemma sparse_node_size_larger_than_1 (node : sparse_node) : sizeof node > 1 :=
begin
    induction node; unfold sizeof has_sizeof.sizeof sparse_node_size at *; simp; linarith,
end

lemma bsp_set_size_positive (node : bsp_set) : sizeof node > 0 :=
begin
    unfold sizeof has_sizeof.sizeof,
    cases node; unfold bsp_set_size; try {simp},
    have : sparse_node_size node > 1,
    apply sparse_node_size_larger_than_1, linarith,
end

lemma left_shrinks_size (node : sparse_node) : sizeof node.left < sizeof node := 
begin
    induction node; unfold sparse_node.left sizeof has_sizeof.sizeof; try {simp},
    apply bsp_set_size_positive,
    have : sparse_node_size node_right > 1,
    apply sparse_node_size_larger_than_1, linarith,
end

lemma right_shrinks_size (node : sparse_node) : sizeof node.right < sizeof node := 
begin
    induction node; unfold sparse_node.right sizeof has_sizeof.sizeof; try {simp},
    have : sparse_node_size node_left > 1,
    apply sparse_node_size_larger_than_1, linarith, apply bsp_set_size_positive,
end

/-- this is just a local combination, not a proper union. We use it to have simpler code elsewehere -/
def combine_children : bsp_set → bsp_set → bsp_set
| (sparse left) right := sparse (left_sparse left right)
| left (sparse right) := sparse (right_sparse left right)
| empty empty := empty
| dense dense := dense
| empty dense := sparse empty_dense
| dense empty := sparse dense_empty

def union : bsp_set → bsp_set → bsp_set
| empty right := right
| left empty := left
| dense _ := dense
| _ dense := dense
| (sparse left) (sparse right) := 
    have bsp_set_size left.left < sparse_node_size left := left_shrinks_size left,
    have bsp_set_size left.right < sparse_node_size left := right_shrinks_size left,
    combine_children (union left.left right.left) (union left.right right.right)

def intersect : bsp_set → bsp_set → bsp_set
| empty _ := empty
| _ empty := empty
| dense right := right
| left dense := left
| (sparse left) (sparse right) := 
    have bsp_set_size left.left < sparse_node_size left := left_shrinks_size left,
    have bsp_set_size left.right < sparse_node_size left := right_shrinks_size left,
    combine_children (intersect left.left right.left) (intersect left.right right.right)

def minus : bsp_set → bsp_set → bsp_set
| empty _ := empty
| left empty := left
| _ dense := empty
| (sparse left) (sparse right) := 
    have bsp_set_size right.left < sparse_node_size right := left_shrinks_size right,
    have bsp_set_size right.right < sparse_node_size right := right_shrinks_size right,
    combine_children (minus left.left right.left) (minus left.right right.right)
| dense (sparse right) := 
    have 1 < sparse_node_size right := sparse_node_size_larger_than_1 right,
    combine_children (minus right.left dense) (minus right.right dense)
using_well_founded { rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, bsp_set_size x.2)⟩]}

def complement (set : bsp_set) : bsp_set := minus dense set

inductive color
| black
| white
| rgb (r g b: ℕ)

/-- example encodings -/
def num_to_bsp : ℕ → sparse_node
| nat.zero := dense_empty 
| (nat.succ n) := empty_dense

def col_to_bsp : color → bsp_set 
| color.black := sparse (left_sparse dense_empty empty)
| color.white := sparse (left_sparse empty_dense empty)
| (color.rgb r g b) := 
    sparse (right_sparse 
        empty 
        (left_sparse 
            (num_to_bsp r) 
            (sparse (left_sparse 
                (num_to_bsp g)
                (sparse (num_to_bsp g))))))