Programming Language Foundations in Agda: Equality

Equality.agda

module Equality where

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

{-# BUILTIN EQUALITY _≡_ #-}

infix 4 _≡_

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

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

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

cong₂ : ∀ {A B C : Set} (f : A → B → C) {x y : A} {u v : B} → x ≡ y → u ≡ v → f x u ≡ f y v
cong₂ f refl refl = refl

cong-app : ∀ {A B : Set} {f g : A → B} → f ≡ g → ∀ (x : A) → f x ≡ f x
cong-app refl x = refl

subst : ∀ {A : Set} {x y : A} (P : A → Set) → x ≡ y → P x → P y
subst P refl px = px

module ≡-Reasoning {A : Set} where

    infix  1 begin_
    infixr 2 _≡⟨⟩_ _≡⟨_⟩_
    infix  3 _∎

    begin_ : ∀ {x y : A} → x ≡ y → x ≡ y
    begin_ x≡y = x≡y

    _≡⟨⟩_ : ∀ (x : A) {y : A} → x ≡ y → x ≡ y
    x ≡⟨⟩ x≡y = x≡y

    _≡⟨_⟩_ : ∀ (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
    x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z

    _∎ : ∀ (x : A) → x ≡ x
    x ∎ = refl

open ≡-Reasoning

trans' : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans' {A} {x} {y} {z} x≡y y≡z =
    begin
        x
    ≡⟨ x≡y ⟩
        y
    ≡⟨ y≡z ⟩
        z
    ∎

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

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

postulate
    +-identity : ∀ (m : ℕ) → m + zero ≡ m
    +-suc : ∀ (m n : ℕ) → m + suc n ≡ suc (m + n)

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-comm m zero =
    begin
        m + zero
    ≡⟨ +-identity m ⟩
        m
    ≡⟨⟩
        zero + m
    ∎
+-comm m (suc n) =
    begin
        m + suc n
    ≡⟨ +-suc m n ⟩
        suc (m + n)
    ≡⟨ cong suc (+-comm m n) ⟩
        suc (n + m)
    ≡⟨⟩
        suc n + m
    ∎

infix 4 _≤_

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

module ≤-Reasoning {A : Set} where

    infix  1 start_
    infixr 2 _≤⟨⟩_ _≤⟨_⟩_
    infix  3 _qed

    start_ : ∀ {x y : ℕ} → x ≤ y → x ≤ y
    start_ x≤y = x≤y

    _≤⟨⟩_ : ∀ (x : ℕ) {y : ℕ} → x ≤ y → x ≤ y
    x ≤⟨⟩ x≤y = x≤y

    _≤⟨_⟩_ : ∀ (x : ℕ) {y z : ℕ} → x ≤ y → y ≤ z → x ≤ z
    x       ≤⟨ z≤n       ⟩ y≤z       = z≤n
    (suc x) ≤⟨ (s≤s x≤y) ⟩ (s≤s y≤z) = s≤s ( x ≤⟨ x≤y ⟩ y≤z )

    _qed : ∀ (x : ℕ) → x ≤ x
    zero    qed = z≤n
    (suc x) qed = s≤s ( x qed )

open ≤-Reasoning

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

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

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

even-comm : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm m n ev rewrite +-comm m n = ev

even-comm' : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm' m n ev with m + n    | +-comm m n
...                  | .(n + m) | refl       = ev

even-comm'' : ∀ (m n : ℕ) → even (m + n) → even (n + m)
even-comm'' m n = subst even (+-comm m n)

_≐_ : ∀ {A : Set} (x y : A) → Set₁
_≐_ {A} x y = ∀ (P : A → Set) → P x → P y

refl-≐ : ∀ {A : Set} {x : A} → x ≐ x
refl-≐ P Px = Px

trans-≐ : ∀ {A : Set} {x y z : A} → x ≐ y → y ≐ z → x ≐ z
trans-≐ xy yz P Px = yz P (xy P Px)

sym-≐ : ∀ {A : Set} {x y : A} → x ≐ y → y ≐ x
sym-≐ {A} {x} {y} xy P = Qy
    where
    Q : A → Set
    Q z = P z → P x
    Qx : Q x
    Qx = refl-≐ P
    Qy : Q y
    Qy = xy Q Qx

open import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)

data _≡'_ {ℓ : Level} {A : Set ℓ} (x : A) : A → Set ℓ where
    refl' : x ≡' x

sym' : ∀ {ℓ : Level} {A : Set ℓ} {x y : A} → x ≡' y → y ≡' x
sym' refl' = refl'

_≐'_ : ∀ {ℓ : Level} {A : Set ℓ} (x y : A) → Set (lsuc ℓ)
_≐'_ {ℓ} {A} x y = ∀ (P : A → Set ℓ) → P x → P y