Range.agda

module Range where

-- Preliminaries

record True : Set where
data False : Set where
data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
data _||_ (A : Set) (B : Set) : Set where
  inl : A → A || B
  inr : B → A || B

exFalso : {A : Set} → False → A
exFalso ()

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

succInjective : {a b : ℕ} → succ a ≡ succ b → a ≡ b
succInjective {zero} {zero} _ = refl
succInjective {succ a} {succ .a} refl = refl

ℕDecideEquality : (x y : ℕ) → (x ≡ y) || ((x ≡ y) → False)
ℕDecideEquality zero zero = inl refl
ℕDecideEquality zero (succ y) = inr λ ()
ℕDecideEquality (succ x) zero = inr λ ()
ℕDecideEquality (succ x) (succ y) with ℕDecideEquality x y
... | inl refl = inl refl
... | inr neq = inr λ p → neq (succInjective p)

_<N_ : ℕ → ℕ → Set
zero <N zero = False
zero <N succ b = True
succ a <N zero = False
succ a <N succ b = a <N b

_≤N_ : ℕ → ℕ → Set
a ≤N b = (a <N b) || (a ≡ b)

notLessZero : (a : ℕ) → a <N 0 → False
notLessZero zero ()
notLessZero (succ a) ()

contractLessSucc : (a b : ℕ) → a <N succ b → a ≤N b
contractLessSucc zero zero pr = inr refl
contractLessSucc zero (succ b) pr = inl (record {})
contractLessSucc (succ a) zero pr = exFalso (notLessZero a pr)
contractLessSucc (succ a) (succ b) pr with contractLessSucc a b pr
... | inl x = inl x
... | inr refl = inr refl

---

data FinSet (A : Set) : Set where
  empty : FinSet A
  add : A → FinSet A → FinSet A

contains : {A : Set} → ((x y : A) → (x ≡ y) || ((x ≡ y) → False)) → FinSet A → A → Set
contains dec empty t = False
contains dec (add x s) t with dec t x
... | inl t=x = True
... | inr t!=x = contains dec s t

------

range : (n : ℕ) → FinSet ℕ
range zero = add zero empty
range (succ n) = add (succ n) (range n)

rangeContains : (n : ℕ) → contains ℕDecideEquality (range n) n
rangeContains zero = record {}
rangeContains (succ n) with ℕDecideEquality n n
... | inl refl = record {}
... | inr n!=n = exFalso (n!=n refl)

rangeClosed : (n a : ℕ) → contains ℕDecideEquality (range n) a → (v : ℕ) → (v ≤N a) → contains ℕDecideEquality (range n) v
rangeClosed zero a cont v v<=a with ℕDecideEquality a 0

rangeClosed zero .0 cont v (inl v<0) | inl refl = exFalso (notLessZero v v<0)
rangeClosed zero .0 cont .0 (inr refl) | inl refl = record {}
... | inr a!=0 with ℕDecideEquality v 0
... | inl v=0 = record {}
... | inr v!=0 = cont
rangeClosed (succ n) a cont v v<=a with ℕDecideEquality v (succ n)
rangeClosed (succ n) a cont v v<=a               | inl v=sn = record {}
rangeClosed (succ n) a cont v v<=a               | inr v!=sn with ℕDecideEquality a (succ n)
rangeClosed (succ n) .(succ n) cont v (inl x)    | inr v!=sn | inl refl = rangeClosed n n (rangeContains n) v (contractLessSucc v n x)
rangeClosed (succ n) .(succ n) cont v (inr v=sn) | inr v!=sn | inl refl = exFalso (v!=sn v=sn)
rangeClosed (succ n) a cont v v<=a               | inr v!=sn | inr a!=sn = rangeClosed n a cont v v<=a