Programming Language Foundations in Agda: Relations

Relations.agda

module Relations where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong)
open Eq.≡-Reasoning

open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
open import Data.Nat.DivMod using (_/_)
open import Data.Nat.Properties using (+-comm; *-comm; +-identityʳ; +-suc; +-assoc)
open import Function using (_∘_)

infix 4 _≤_

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {a : ℕ} → zero ≤ a
  s≤s : ∀ {a b : ℕ} → a ≤ b → suc a ≤ suc b

inv-s≤s : ∀ {a b : ℕ} → suc a ≤ suc b → a ≤ b
inv-s≤s (s≤s a≤b) = a≤b

≤-refl : ∀ {a : ℕ} → a ≤ a
≤-refl {zero}  = z≤n
≤-refl {suc a} = s≤s ≤-refl

≤-trans : ∀ {a b c : ℕ} → a ≤ b → b ≤ c → a ≤ c
≤-trans z≤n      bc       = z≤n
≤-trans (s≤s ab) (s≤s bc) = s≤s (≤-trans ab bc)

≤-antisym : ∀ {a b : ℕ} → a ≤ b → b ≤ a → a ≡ b
≤-antisym z≤n z≤n                                   = refl
≤-antisym (s≤s ab) (s≤s ba) rewrite ≤-antisym ab ba = refl

data Total (a b : ℕ) : Set where
  forward : a ≤ b → Total a b
  flipped : b ≤ a → Total a b

≤-total : ∀ (a b : ℕ) → Total a b
≤-total zero    b    = forward z≤n
≤-total (suc a) zero = flipped z≤n
≤-total (suc a) (suc b) with ≤-total a b
...                        | forward ab = forward (s≤s ab)
...                        | flipped ba = flipped (s≤s ba)

+mono-r≤ : ∀ (a b c : ℕ) → b ≤ c → a + b ≤ a + c
+mono-r≤ zero    b c bc = bc
+mono-r≤ (suc a) b c bc = s≤s (+mono-r≤ a b c bc)

+mono-l≤ : ∀ (a b c : ℕ) → a ≤ b → a + c ≤ b + c
+mono-l≤ a b c ab rewrite +-comm a c | +-comm b c = +mono-r≤ c a b ab

+mono≤ : ∀ (a b c d : ℕ) → a ≤ b → c ≤ d → a + c ≤ b + d
+mono≤ a b c d ab cd = ≤-trans (+mono-l≤ a b c ab) (+mono-r≤ b c d cd)
  -- +mono-l≤ a b c ab => a + c ≤ b + c
  -- +mono-r≤ b c d cd => b + c ≤ b + d
  -- ≤-trans ... ...   => a + c ≤ b + d

*helper : ∀ (a b : ℕ) → a * b + b ≡ suc a * b
*helper a b rewrite +-comm (a * b) b | *-comm a b = refl

*+≤ : ∀ (a b c : ℕ) → a * b + b ≤ a * c + c → suc a * b ≤ suc a * c
*+≤ a b c bc rewrite *helper a b | *helper a c = bc

*mono-r≤ : ∀ (a b c : ℕ) → b ≤ c → a * b ≤ a * c
*mono-r≤ zero b c bc = z≤n
*mono-r≤ (suc a) b c bc =
  *+≤ a b c (+mono≤ (a * b) (a * c) b c (*mono-r≤ a b c bc) bc)
  -- *mono-r≤ a b c bc => a * b ≤ a * c
  -- +mono≤ ...        => (a * b) + b ≤ (a * c) + c
  -- *+≤ ...           => suc a * b ≤ suc a * c

*mono-l≤ : ∀ (a b c : ℕ) → a ≤ b → a * c ≤ b * c
*mono-l≤ a b c ab rewrite *-comm a c | *-comm b c = *mono-r≤ c a b ab

*mono≤ : ∀ (a b c d : ℕ) → a ≤ b → c ≤ d → a * c ≤ b * d
*mono≤ a b c d ab cd = ≤-trans (*mono-l≤ a b c ab) (*mono-r≤ b c d cd)

infix 4 _<_

data _<_ : ℕ → ℕ → Set where
  z<s : ∀ {a : ℕ} → zero < suc a
  s<s : ∀ {a b : ℕ} → a < b → suc a < suc b

<-trans : ∀ {a b c : ℕ} → a < b → b < c → a < c
<-trans z<s      (s<s bc) = z<s
<-trans (s<s ab) (s<s bc) = s<s (<-trans ab bc)

data Trichotomy (a b : ℕ) : Set where
  less : a < b → Trichotomy a b
  equal : a ≡ b → Trichotomy a b
  greater : b < a → Trichotomy a b

<-trichotomy : ∀ (a b : ℕ) → Trichotomy a b
<-trichotomy zero    zero    = equal refl
<-trichotomy zero    (suc b) = less z<s
<-trichotomy (suc a) zero    = greater z<s
<-trichotomy (suc a) (suc b) with <-trichotomy a b
...                             | equal ab   = equal (cong suc ab)
...                             | less ab    = less (s<s ab)
...                             | greater ab = greater (s<s ab)

+mono-r< : ∀ (a b c : ℕ) → b < c → a + b < a + c
+mono-r< zero    b c bc = bc
+mono-r< (suc a) b c bc = s<s (+mono-r< a b c bc)

+mono-l< : ∀ (a b c : ℕ) → a < b → a + c < b + c
+mono-l< a b c ab rewrite +-comm a c | +-comm b c = +mono-r< c a b ab

+mono< : ∀ (a b c d : ℕ) → a < b → c < d → a + c < b + d
+mono< a b c d ab cd = <-trans (+mono-l< a b c ab) (+mono-r< b c d cd)

≤-iff-< : ∀ (a b : ℕ) → suc a ≤ b → a < b
≤-iff-< zero    b       (s≤s z≤n) = z<s
≤-iff-< (suc a) (suc b) (s≤s a≤b) = s<s (≤-iff-< a b a≤b)

<-iff-≤ : ∀ (a b : ℕ) → a < b → suc a ≤ b
<-iff-≤ a       b       z<s       = (s≤s z≤n)
<-iff-≤ (suc a) (suc b) (s<s a<b) = s≤s (<-iff-≤ a b a<b)

data even : ℕ → Set
data odd : ℕ → Set

data even where
    zero : even zero
    suc : ∀ {n : ℕ} → odd n → even (suc n)

data odd where
    suc : ∀ {n : ℕ} → even n → odd (suc n)

e+e≡e : ∀ {m n : ℕ} → even m → even n → even (m + n)
o+e≡o : ∀ {m n : ℕ} → odd m → even n → odd (m + n)

e+e≡e zero    n = n
e+e≡e (suc m) n = suc (o+e≡o m n)

o+e≡o (suc m) n = suc (e+e≡e m n)

o+o≡e : ∀ {m n : ℕ} → odd m → odd n → even (m + n)
o+o≡e (suc zero)    n = suc n
o+o≡e (suc (suc m)) n = suc (suc (o+o≡e m n))

-- https://gist.github.com/pedrominicz/6c3dfe3fc35a5c3f7115f561fd0ac25d
open import Naturals using (Bin; <>; _O; _I; inc; from; to)

data One : Bin → Set where
    <>I : One (<> I)
    _O : ∀ {b : Bin} → One b → One (b O)
    _I : ∀ {b : Bin} → One b → One (b I)

data Can : Bin → Set where
    <>O : Can (<> O)
    <>I : Can (<> I)
    _O : ∀ {b : Bin} {one : One b} → Can b → Can (b O)
    _I : ∀ {b : Bin} {one : One b} → Can b → Can (b I)

One-inc : ∀ {b : Bin} → One b → One (inc b)
One-inc <>I   = <>I O
One-inc (b O) = b I
One-inc (b I) = (One-inc b) O

Can-inc : ∀ {b : Bin} → Can b → Can (inc b)
Can-inc <>O                = <>I
Can-inc <>I                = _O {<> I} {<>I} <>I
Can-inc (_O {b} {one} can) = _I {b} {one} can
Can-inc (_I {b} {one} can) = _O {inc b} {One-inc one} (Can-inc can)

One-to : ∀ (n : ℕ) → One (to (suc n))
One-to zero    = <>I
One-to (suc n) = One-inc (One-to n)

Can-to : ∀ (n : ℕ) → Can (to n)
Can-to zero    = <>O
Can-to (suc n) = Can-inc (Can-to n)

data Suc : ℕ → Set where
    suc : ∀ (n : ℕ) → Suc (suc n)

suc-+ : ∀ {n m : ℕ} → Suc n → Suc m → Suc (n + m)
suc-+ (suc zero)    (suc m) = suc (suc m)
suc-+ (suc (suc n)) (suc m) with suc-+ (suc n) (suc m)
...                            | suc n+m = suc (suc n+m)

from-One : ∀ {b : Bin} → One b → Suc (from b)
from-One <>I = suc zero
from-One {b O} (b' O)
    with from b | from-One b'
...    | suc n  | suc n' rewrite +-identityʳ n = suc-+ (suc n') (suc n')
from-One {b I} (b' I)
    with from b | from-One b'
...    | suc n  | suc n' rewrite +-identityʳ n = suc-+ (suc (suc n')) (suc n')

+* : ∀ (n : ℕ) → n + n ≡ 2 * n
+* n rewrite +-identityʳ n = refl

inc-O : ∀ (b : Bin) → (inc b) O ≡ inc (inc (b O))
inc-O <>                    = refl
inc-O (b O) rewrite inc-O b = refl
inc-O (b I) rewrite inc-O b = refl

to-O-helper : ∀ (n : ℕ) → n + suc (suc n) ≡ 2 * suc n
to-O-helper zero = refl
to-O-helper (suc n)
    rewrite *-comm 2 (suc (suc n))
          | to-O-helper n
          | +-suc n (suc (suc n))
          | +-suc n (suc n)
          | +-suc n n
          | *-comm n 2
          | +-identityʳ n
          = refl

to-O : ∀ {n : ℕ} → Suc n → to (2 * n) ≡ (to n) O
to-O (suc zero) = refl
to-O (suc (suc n))                      -- to (2 * suc (suc n))
    rewrite +-identityʳ n               -- to (suc (suc n) + suc (suc n))
          | to-O-helper n
          | to-O (suc n)
          | inc-O (inc (to n))
          | inc-O (to n)
          = refl

helper₀ : ∀ {b : Bin} {one : One b} → Can b → to (2 * from b) ≡ to (from b) O
helper₀ {<> I} {<>I} <>I = refl
helper₀ {b O} {one O} (can O)
    with from (b O) | from-One (one O)
...    | suc n      | suc n' rewrite to-O (suc n) = refl
helper₀ {b I} {one I} (can I)
    with from (b I) | from-One (one I)
...    | suc n      | suc n' rewrite to-O (suc (from (b O))) = refl

helper₁ : ∀ {b : Bin} {one : One b} → Can b → to (1 + 2 * from b) ≡ to (from b) I
helper₁ {<> I} {<>I} <>I = refl
helper₁ {b O} {one O} c@(can O)
    rewrite helper₀ {b O} {one O} c
          | helper₀ {b} {one} can = refl
helper₁ {b I} {one I} c@(can I)
    rewrite helper₀ {b I} {one I} c
          | helper₀ {b} {one} can = refl

Can-to∘from : ∀ {b : Bin} → Can b → to (from b) ≡ b
Can-to∘from <>O = refl
Can-to∘from <>I = refl
Can-to∘from (_O {b} {one} can) rewrite helper₀ {b} {one} can | Can-to∘from can = refl
Can-to∘from (_I {b} {one} can) rewrite helper₁ {b} {one} can | Can-to∘from can = refl