WIP: adding interval

Mandlebrah/Flot754.lean

@@ -0,0 +1,21 @@
+
+inductive spec_float 
+  | S754_zero (s : Bool)
+  | S754_infinity (s : Bool)
+  | S754_nan
+  | S754_finite (s : Bool) (m: Nat) (e : Int)
+
+#eval max 1 22
+namespace FloatOps
+  variable (prec emax : Int)
+
+  def emin : Int := (3 - emax - prec) 
+  def fexp (e : Int) : Int := max (e - prec) (3 - emax - prec)
+
+
+  section Zdigits
+  end Zdigits
+
+
+
+end FloatOps

Mandlebrah/Interval.lean

@@ -0,0 +1,50 @@
+universe u v w
+
+/- 
+  contains : ω → α → Bool
+  overlaps : ω → α → Bool
+  subInterval :  ω → ω → Bool
+  split : ω → α → ω × ω
+A type class to represent closed intervals
+-/
+---------------- The Interval   The value
+class Interval (α : Type v) (β : Type w)  where
+  max : α -> β 
+  min : α -> β  
+
+
+def NatInterval := Nat × Nat
+namespace NatInterval
+
+
+variable (n : NatInterval)
+@[inline] def ordered: Nat × Nat := if n.fst > n.snd then n else (n.snd, n.fst) 
+@[inline] def max: Nat := n.ordered.fst
+@[inline] def min: Nat := n.ordered.snd 
+@[inline] def l := n.min
+@[inline] def u := n.max
+
+def isEmpty : Bool := n.l == n.u
+
+def contains (hn : Nat) : Bool := n.l ≤ hn ∧ hn ≤ n.u
+
+def overlaps (hni : NatInterval) : Bool := 
+  -- If either the lower bound or the upper
+  -- bound are contained then the interval overlaps
+  n.contains hni.l ∨ n.contains hni.u
+
+def isSubInterval (hni : NatInterval) : Bool :=
+  n.contains hni.l ∧ n.contains hni.u
+
+def split (splitAt : Nat ) : NatInterval × NatInterval := 
+  ((n.l, splitAt), (splitAt, n.u))
+
+
+end NatInterval
+
+instance Interval NatInterval Nat
+  upper := 
+
+
+#check Interval Nat Nat
+

Mandlebrah/QuadTree.lean

@@ -0,0 +1,67 @@
+universe u v w
+
+/- 
+A type class to represent closed intervals
+-/
+---------------- The Interval   The value
+class Interval (ω : Type w) (α : Type v) where
+  contains : ω → α → Bool
+  overlaps : ω → α → Bool
+  subInterval :  ω → ω → Bool
+  split : ω → α → ω × ω
+
+structure NatInterval where
+  l : Nat
+  u : Nat
+
+namespace NatInterval
+
+
+variable (n : NatInterval)
+
+def bld (l₁ u₁ : Nat) : NatInterval := 
+  match (l₁ < u₁ : Bool) with
+  | true => {l := l₁, u:= u₁}
+  | false => {l := u₁, u:= l₁}
+
+def isEmpty : Bool := n.l == n.u
+
+def contains (hn : Nat) : Bool := n.l ≤ hn ∧ hn ≤ n.u
+
+def overlaps (hni : NatInterval) : Bool := 
+  -- If either the lower bound or the upper
+  -- bound are contained then the interval overlaps
+  n.contains hni.l ∨ n.contains hni.u
+
+def isSubInterval (hni : NatInterval) : Bool :=
+  n.contains hni.l ∧ n.contains hni.u
+
+#check bld 1 1
+def split (splitAt : Nat ) : NatInterval × NatInterval := 
+  (bld n.l splitAt, bld splitAt n.u)
+
+
+end NatInterval
+
+#check Interval Nat Nat
+
+scoped 
+--instance : Interval Nat Nat where
+--  isBounded := 
+--  contains: ω → Bool
+--  cut: ω → Interval × Interval
+
+
+inductive QNode (α : Type u) (bound: (w × w) × (w × w)) where
+  | leaf : QNode α bound
+  | node  (n₀₀ : QNode α bound) 
+          (n₀₁ : QNode α bound) 
+          (n₁₀ : QNode α bound) 
+          (n₁₁ : QNode α bound) : QNode α bound
+
+ namespace QNode 
+ variable {α : Type u} {δ : Nat}
+
+ open Nat
+
+ def depth