module Core where

infix 4 _,_

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    prj₁ : A
    prj₂ : B prj₁

open Σ

infix 0 _⨄_

data _⨄_ (A B : Set) : Set where
  inj₁ : A → A ⨄ B
  inj₂ : B → A ⨄ B

_×_ : Set → Set → Set
A × B = Σ A λ _ → B


data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

infix 2 _≡_

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}

ap : ∀ {A B} {x y : A} (f : A → B) → x ≡ y → f x ≡ f y
ap f refl = refl

subst : ∀ {A} {B : A → Set} {x y : A} → x ≡ y → B x → B y
subst refl b = b

sym : ∀ {A} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : ∀ {A} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl y=z = y=z

_∙_ = trans

infix 9 _<_
infix 9 _>_

data _<_ : ℕ → ℕ → Set where
  z<s : ∀ {n} → zero < suc n
  sx<sy : ∀ {x y} → x < y → suc x < suc y

<-trans : ∀ {x y z} → x < y → y < z → x < z
<-trans z<s (sx<sy y<z) = z<s
<-trans (sx<sy x<y) (sx<sy y<z) = sx<sy (<-trans x<y y<z)

_>_ : ℕ → ℕ → Set
x > y = y < x

_≤_ : ℕ → ℕ → Set
x ≤ y = x < suc y

_≥_ : ℕ → ℕ → Set
x ≥ y = y ≤ x

≤-weaken : ∀ {x y} → x < y → x ≤ y
≤-weaken z<s = z<s
≤-weaken (sx<sy x<y) = sx<sy (≤-weaken x<y)

≤-refl : ∀ {x} → x ≤ x
≤-refl {zero} = z<s
≤-refl {suc x} = sx<sy ≤-refl

≤-trans : ∀ {x y z} → x ≤ y → y ≤ z → x ≤ z
≤-trans {zero} {_} {_} _ _ = z<s
≤-trans {suc x} {suc y} {suc z} (sx<sy x≤y) (sx<sy y≤z) = sx<sy (≤-trans x≤y y≤z)

x<sx : ∀ {x} → x < suc x
x<sx {zero} = z<s
x<sx {suc x} = sx<sy x<sx

≤⇒<∨= : ∀ {x y} → x ≤ y → x < y ⨄ x ≡ y
≤⇒<∨= {zero} {zero} x≤y = inj₂ refl
≤⇒<∨= {zero} {suc y} x≤y = inj₁ z<s
≤⇒<∨= {suc x} {suc y} (sx<sy x≤y) with ≤⇒<∨= x≤y
... | inj₁ x<y = inj₁ (sx<sy x<y)
... | inj₂ x=y = inj₂ (ap suc x=y)

<-≤-trans : ∀ {x y z} → x < y → y ≤ z → x < z
<-≤-trans x<y y≤z with ≤⇒<∨= y≤z
... | inj₁ y<z = <-trans x<y y<z
... | inj₂ y=z = subst y=z x<y

≤-<-trans : ∀ {x y z} → x ≤ y → y < z → x < z
≤-<-trans x≤y y<z with ≤⇒<∨= x≤y
... | inj₁ x<y = <-trans x<y y<z
... | inj₂ x=y = subst (sym x=y) y<z



data _<=>_ : ℕ → ℕ → Set where
  le : ∀ {x y} → x < y → x <=> y
  eq : ∀ {x y} → x ≡ y → x <=> y
  gt : ∀ {x y} → x > y → x <=> y

_<?>_ : (x y : ℕ) → x <=> y
zero <?> zero = eq refl
zero <?> suc y = le z<s
suc x <?> zero = gt z<s
suc x <?> suc y with x <?> y
... | le x<y = le (sx<sy x<y)
... | eq x=y = eq (ap suc x=y)
... | gt x>y = gt (sx<sy x>y)


min : ℕ → ℕ → ℕ
min x y with x <?> y
... | le x<y = x
... | eq x=y = x
... | gt x>y = y

max : ℕ → ℕ → ℕ
max x y with x <?> y
... | le x<y = y
... | eq x=y = y
... | gt x>y = x


data Bool : Set where
  false true : Bool


data ⊥ : Set where

⊥-elim : {A : Set} → ⊥ → A
⊥-elim ()

infix 0 ¬_

¬_ : Set → Set
¬ A = A → ⊥

data Decidable (A : Set) : Set where
  yes : A → Decidable A
  no : ¬ A → Decidable A


_≟_ : (x y : ℕ) → Decidable (x ≡ y)
zero ≟ zero = yes refl
zero ≟ suc y = no λ ()
suc x ≟ zero = no λ ()
suc x ≟ suc y with x ≟ y
... | yes x=y = yes (ap suc x=y)
... | no ¬x=y = no λ { refl → ¬x=y refl }
