prove some theorems

base/BBT/Balanced.kind

@@ -0,0 +1,23 @@
+BBT.Balanced<K: Type, V: Type>(cmp: K -> K -> Cmp, map: BBT<K, V>): Type
+  case map {
+    tip:
+      Unit
+    bin:
+      And<
+        // if the tree is balanced we can strenghten a proof of membership
+        // with the result of a comparison
+        (key: K) (H: BBT.In<K, V>(map, key))
+        case cmp(key, map.key) {
+          ltn: And<
+            BBT.In<K, V>(map.left, key),
+            Not(BBT.In<K, V>(map.right, key))>
+          eql: Unit
+          gtn: And<
+            Not(BBT.In<K, V>(map.left, key)),
+            BBT.In<K, V>(map.right, key)>
+        },
+        // children are also balanced
+        And<
+          BBT.Balanced<K, V>(cmp, map.left),
+          BBT.Balanced<K, V>(cmp, map.right)>>
+  }!

base/BBT/In.kind

@@ -0,0 +1,45 @@
+// path to get to a value in a BBT
+BBT.In<K: Type, V: Type>(map: BBT<K, V>, key: K): Type
+  case map {
+    tip: 
+      self<P: BBT.In<K, V>(BBT.tip<K, V>, key) -> Type>
+      P(self)
+    bin:
+      def mmap = BBT.bin<K, V>(map.size, map.key, map.val, map.left, map.right)
+      self<P: BBT.In<K, V>(mmap, key) -> Type>
+      (left: (H: BBT.In<K, V>(map.left, key)) P(BBT.In.left<K, V>(map.size, map.key, map.val, map.left, map.right, key, H)))
+      (right: (H: BBT.In<K, V>(map.right, key)) P(BBT.In.right<K, V>(map.size, map.key, map.val, map.left, map.right, key, H)))
+      (here: P(BBT.In.here<K, V>(map.size, key, map.val, map.left, map.right)))
+      P(self)
+  }!
+
+BBT.In.left<K: Type, V: Type>(
+  size: U32
+  key0: K
+  val: V
+  lft: BBT<K, V>
+  rht: BBT<K, V>
+  key1: K
+  H: BBT.In<K, V>(lft, key1)
+): BBT.In<K, V>(BBT.bin<K, V>(size, key0, val, lft, rht), key1)
+  (self, lft, rht, here) lft(H)
+
+BBT.In.right<K: Type, V: Type>(
+  size: U32
+  key0: K
+  val: V
+  lft: BBT<K, V>
+  rht: BBT<K, V>
+  key1: K
+  H: BBT.In<K, V>(rht, key1)
+): BBT.In<K, V>(BBT.bin<K, V>(size, key0, val, lft, rht), key1)
+  (self, lft, rht, here) rht(H)
+
+BBT.In.here<K: Type, V: Type>(
+  size: U32
+  key: K
+  val: V
+  lft: BBT<K, V>
+  rht: BBT<K, V>
+): BBT.In<K, V>(BBT.bin<K, V>(size, key, val, lft, rht), key)
+  (self, rht, rht, here) here

base/BBT/In/lookup.kind

@@ -0,0 +1,30 @@
+// efficiently lookup the value of a key you know it's there
+BBT.In.lookup<K: Type, V: Type>(
+  cmp: K -> K -> Cmp
+  key: K
+  map: BBT<K,V>
+)<H0: BBT.In<K, V>(map, key)
+  H1: BBT.Balanced<K, V>(cmp, map)
+>: V
+  case map with H0 H1 {
+    tip:
+      case H0 {}
+    bin:
+      open H1
+      open H1.snd
+      def its_there = H1.fst(key, H0) // where should I look?
+      case cmp(key, map.key) with its_there {
+        ltn:
+          // now ind is BBT.In<K, V>(map.left, key)
+          // so we can call the function recursively
+          open its_there
+          BBT.In.lookup<K, V>(cmp, key, map.left)<its_there.fst, H1.snd.fst>
+        eql:
+          map.val
+        gtn:
+          // now ind is BBT.In<K, V>(map.right, key)
+          // so we can call the function recursively
+          open its_there
+          BBT.In.lookup<K, V>(cmp, key, map.right)<its_there.snd, H1.snd.snd>
+      }!
+  }!

base/BBT/In/singleton.kind

@@ -0,0 +1,2 @@
+BBT.In.singleton<K: Type, V: Type>(key: K, val: V): BBT.In<K,V>(BBT.singleton<K, V>(key, val), key)
+  BBT.In.here!!!!!!!

base/BBT/Invariant.kind

@@ -0,0 +1,5 @@
+type BBT.Invariant<K: Type, V: Type>(cmp: K -> K -> Cmp, map: BBT<K, V>) {
+  new(
+    bal: BBT.Balanced<K, V>(cmp, map)
+  )
+}

base/BBT/member/In.kind

@@ -0,0 +1,24 @@
+BBT.member.In<K: Type, V: Type>(
+  cmp: K -> K -> Cmp
+  key: K
+  map: BBT<K,V>
+)<H0: BBT.member<K, V>(cmp, key, map) == true
+  H1: BBT.Balanced<K, V>(cmp, map)
+>: BBT.In<K, V>(map, key)
+  case map with H0 H1 {
+    tip:
+      let contra = Bool.false_neq_true(H0)
+      Empty.absurd!(contra)
+    bin:
+      open H1 open H1.snd
+      case cmp(key, map.key) with H0 {
+        ltn:
+          let ind = BBT.member.In<K, V>(cmp, key, map.left, H0, H1.snd.fst)
+          ?ltn
+        eql:
+          BBT.In.here<K, V>(map.size, key, map.val, map.left, map.right)
+        gtn:
+          ?gtn
+      }!
+  }!
+

base/Cmp/Order.kind

@@ -0,0 +1,13 @@
+type Cmp.Order<A: Type>(cmp: A -> A -> Cmp) {
+  new(
+    refl: 
+      (a: A, b: A, H: Equal<Cmp>(cmp(a, b), Cmp.eql))
+      (Equal<A>(a, b))
+    antisym:
+      (a: A, b: A)
+      (Equal<Cmp>(cmp(a, b), Cmp.inv(cmp(b, a)))),
+    trans:
+      (a: A, b: A, c: A, H0: Equal<Cmp>(cmp(a, b), cmp(b, c)))
+      (Equal<Cmp>(cmp(b, c), cmp(a, c)))
+  )
+}

base/Cmp/inv/involutive.kind

@@ -0,0 +1,6 @@
+Cmp.inv.involution(c: Cmp): c == Cmp.inv(Cmp.inv(c))
+  case c {
+    ltn: refl
+    eql: refl
+    gtn: refl
+  }!