lol.agda

module lol where

open import Level
open import Relation.Binary.Core

--------------BOOL---------------------------------------

data 𝔹 : Set where
  tt : 𝔹
  ff : 𝔹


infix 7 ¬_

¬_ : 𝔹 → 𝔹
¬ tt = ff
¬ ff = tt

if_then_else_ : ∀ {ℓ} {A : Set ℓ} → 𝔹 → A → A → A
if tt then a₁ else a₂ = a₁
if ff then a₁ else a₂ = a₂

infixl 5 _∧_

_∧_ : 𝔹 → 𝔹 → 𝔹
tt ∧ tt = tt
a  ∧ b  = ff

infixl 4 _∨_

_∨_ : 𝔹 → 𝔹 → 𝔹
tt ∨ b = tt
ff ∨ b = b

infixl 5 _⊕_

_⊕_ : 𝔹 → 𝔹 → 𝔹
tt ⊕ b  = tt
a  ⊕ tt = tt
a  ⊕ b  = ff

¬¬-elim : ∀ (x : 𝔹) → ¬ ¬ x ≡ x
¬¬-elim tt = refl
¬¬-elim ff = refl

∧-refl : ∀ (x : 𝔹) → x ∧ x ≡ x
∧-refl tt = refl
∧-refl ff = refl

∧-elim₁ : ∀ {x y} → x ∧ y ≡ tt → x ≡ tt
∧-elim₁ {tt} proof = refl
∧-elim₁ {ff} ()


∧-elim₂ : ∀ {x y} → x ∧ y ≡ tt → y ≡ tt
∧-elim₂ {tt} {tt} proof = refl
∧-elim₂ {tt} {ff} ()
∧-elim₂ {ff} ()

∨-∧-absorp : ∀ {a b} → (a ∨ (a ∧ b)) ≡ tt → a ≡ tt
∨-∧-absorp {tt} p = refl
∨-∧-absorp {ff} ()

∧-∨-absorp : ∀ {a b} → (a ∧ (a ∨ b)) ≡ tt → a ≡ tt
∧-∨-absorp {tt} p = refl
∧-∨-absorp {ff} ()

∧-comm : ∀ {a b} → (a ∧ b) ≡ tt → (b ∧ a) ≡ tt
∧-comm {tt} {tt} p = refl
∧-comm {tt} {ff} ()
∧-comm {ff} ()



∨-comm : ∀ {a b} → (a ∨ b) ≡ tt → (b ∨ a) ≡ tt
∨-comm {tt} {tt} p = refl
∨-comm {tt} {ff} p = refl
∨-comm {ff} {tt} p = refl
∨-comm {ff} {ff} ()

--------------NATS---------------------------------------

data ℕ : Set where
  ℤ : ℕ
  𝕊 : ℕ → ℕ

infixl 5 _+_ 

_+_ : ℕ → ℕ → ℕ
a + ℤ = a
a + (𝕊 b) = (𝕊 a) + b

infixl 3 _>_

_>_ : ℕ → ℕ → 𝔹
ℤ > (𝕊 x) = ff
(𝕊 x) > ℤ = tt
(𝕊 a) > (𝕊 b) = a > b
ℤ > ℤ = ff

infixl 3 _≥_

_≥_ : ℕ → ℕ → 𝔹
ℤ ≥ ℤ = tt
ℤ ≥ (𝕊 x) = ff
(𝕊 x) ≥ ℤ = tt
(𝕊 a) ≥ (𝕊 b) = a ≥ b



infixl 2 _≊_

_≊_ : ℕ → ℕ → 𝔹
ℤ ≊ ℤ = tt
(𝕊 a) ≊ (𝕊 b) = a ≊ b
_≊_ a b = ff


three : ℕ
three = 𝕊 (𝕊 (𝕊 ℤ))

four : ℕ
four = 𝕊 three

--≥-antisymm : ∀ {a b} → (a ≥ b) ≡ tt → (b ≥ a) ≡ tt → (a ≊ b) ≡ tt

-->-implies-≥ : ∀ {a b} → (a > b) ≡ tt → (a ≥ b) ≡ tt