agda.agda

agda.agda

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ
{-# BUILTIN NATURAL ℕ #-}


infixl 6 _+_
_+_ : (n m : ℕ) → ℕ
n + zero = n
n + suc m = suc (n + m)

infixl 7 _*_
_*_ : (n m : ℕ) → ℕ
n * zero = zero
n * suc m = n * m + n

infix 4 _≡_
data _≡_ {A : Set} (x : A) : A → Set where
  ≡intro : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

≡elim : {A : Set} {x y : A} {α : A → Set} → α x → x ≡ y → α y
≡elim αx x≡y rewrite x≡y = αx


suc-func : (n m : ℕ) → n ≡ m → suc n ≡ suc m
suc-func n m n≡m rewrite n≡m = ≡intro

suc-inj : (n m : ℕ) → suc n ≡ suc m → n ≡ m
suc-inj n .n ≡intro = ≡intro

lem-0+ : (n : ℕ) → (zero + n ≡ n)
lem-0+ zero = ≡intro
lem-0+ (suc n) rewrite lem-0+ n = ≡intro

tut5-3c : (n : ℕ) → (n * 1 ≡ n)
tut5-3c n = lem-0+ n

infix 4 _<_
data _<_ (n m : ℕ) : Set where
  pf< : (k : ℕ) → n + k ≡ m → n < m

data Ordered (n m : ℕ) : Set where
  less : n < m → Ordered n m
  same : n ≡ m → Ordered n m
  more : m < n → Ordered n m

order : (n m : ℕ) → Ordered n m
order zero    zero    = same ≡intro
order zero    (suc m) = less (pf< (suc m) (suc-func (zero + m) m (lem-0+ m)))
order (suc n) zero    = more (pf< (suc n) (tut5-3c (suc n)))
order (suc n) (suc m) with order n m
... | less (pf< k ≡intro) = less (pf< k {!   !})
... | same n≡m = {!   !}
... | more m<n = {!   !}


data isEven : ℕ → Set where
  zero : isEven zero
  2+   : ∀{x} → isEven x → isEven (suc (suc x))

data isOdd : ℕ → Set where
  1+ : ∀{x} → isEven x → isOdd (suc x)

data Partition (n : ℕ) : Set where
  even : isEven n → Partition n
  odd  : isOdd n  → Partition n

even-or-odd : (n : ℕ) → Partition n
even-or-odd zero = even zero
even-or-odd (suc zero) = odd (1+ zero)
even-or-odd (suc (suc n)) with even-or-odd n
... | even x = even (2+ x)
... | odd (1+ x) = odd (1+ (2+ x))

safesub : ∀{n m} → m < n → ℕ
safesub (pf< k x) = k