Skip to content

Instantly share code, notes, and snippets.

@Smaug123

Smaug123/Range.agda

Created May 9, 2020 10:37
Show Gist options
  • Save Smaug123/b5b2407176328756189d5f5e8918f03a to your computer and use it in GitHub Desktop.
Save Smaug123/b5b2407176328756189d5f5e8918f03a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment