Programming Language Foundations in Agda: Quantifiers

Quantifiers.agda

module Quantifiers where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; cong-app)
open Eq.≡-Reasoning
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (+-suc)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_; proj₁; proj₂; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)

-- https://gist.github.com/pedrominicz/bce9bcfc44f55c04ee5e0b6d903f5809
open import Isomorphism using (_≃_; extensionality; ∀-extensionality)

∀-distrib-× : ∀ {A : Set} {B C : A → Set}
    → (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
∀-distrib-× {A} {B} {C} =
    record
        { to      = to
        ; from    = from
        ; from∘to = λ { _ → refl }
        ; to∘from = λ { _ → refl }
        }
    where
    to : (∀ (x : A) → B x × C x) → (∀ (x : A) → B x) × (∀ (x : A) → C x)
    to a→b×c = (helper₁ , helper₂)
        where
        helper₁ : ∀ (x : A) → B x
        helper₁ a = proj₁ (a→b×c a)

        helper₂ : ∀ (x : A) → C x
        helper₂ a = proj₂ (a→b×c a)

    from : (∀ (x : A) → B x) × (∀ (x : A) → C x) → (∀ (x : A) → B x × C x)
    from (a→b , a→c) = λ a → (a→b a , a→c a)

⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set}
    → (∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
⊎∀-implies-∀⊎ (inj₁ a→b) = λ a → inj₁ (a→b a)
⊎∀-implies-∀⊎ (inj₂ a→c) = λ a → inj₂ (a→c a)

data Tri : Set where
    aa : Tri
    bb : Tri
    cc : Tri

∀-× : ∀ {P : Tri → Set} → (∀ (x : Tri) → P x) ≃ P aa × P bb × P cc
∀-× {P} =
    record
        { to      = to
        ; from    = from
        ; from∘to = λ _ → ∀-extensionality (λ { aa → refl ; bb → refl ; cc → refl })
        ; to∘from = λ _ → refl
        }
    where
    to : (∀ (x : Tri) → P x) → P aa × P bb × P cc
    to p = (p aa , p bb , p cc)

    from : P aa × P bb × P cc → ∀ (x : Tri) → P x
    from (a , b , c) aa = a
    from (a , b , c) bb = b
    from (a , b , c) cc = c

data Σ (A : Set) (B : A → Set) : Set where
    ⟨_,_⟩ : (a : A) → B a → Σ A B

Σ-syntax = Σ
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
infix 2 Σ-syntax

∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B

∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B

∃-elim : ∀ {A : Set} {B : A → Set} {C : Set}
    → (∀ x → B x → C) → ∃[ x ] B x → C
∃-elim f ⟨ x , Bx ⟩ = f x Bx

∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set}
    → (∀ x → B x → C) ≃ (∃[ x ] B x → C)
∀∃-currying {A} {B} {C} =
    record
        { to      = to
        ; from    = from
        ; from∘to = λ _ → refl
        ; to∘from = λ _ → extensionality (λ { ⟨ _ , _ ⟩ → refl })
        }
    where
    to : (∀ x → B x → C) → ∃[ x ] B x → C
    to = ∃-elim

    from : (∃[ x ] B x → C) → ∀ x → B x → C
    from f x Bx = f ⟨ x , Bx ⟩

∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set}
    → ∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
∃-distrib-⊎ {A} {B} {C} =
    record
        { to      = to
        ; from    = from
        ; from∘to = λ { ⟨ x , inj₁ Bx ⟩ → refl ; ⟨ x , inj₂ Cx ⟩ → refl }
        ; to∘from = λ { (inj₁ ⟨ x , Bx ⟩) → refl ; (inj₂ ⟨ x , Cx ⟩) → refl }
        }
    where
    to : ∃[ x ] (B x ⊎ C x) → (∃[ x ] B x) ⊎ (∃[ x ] C x)
    to ⟨ x , inj₁ Bx ⟩ = inj₁ ⟨ x , Bx ⟩
    to ⟨ x , inj₂ Cx ⟩ = inj₂ ⟨ x , Cx ⟩

    from : (∃[ x ] B x) ⊎ (∃[ x ] C x) → ∃[ x ] (B x ⊎ C x)
    from (inj₁ ⟨ x , Bx ⟩) = ⟨ x , inj₁ Bx ⟩
    from (inj₂ ⟨ x , Cx ⟩) = ⟨ x , inj₂ Cx ⟩

∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set}
    → ∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
∃×-implies-×∃ ⟨ x , (Bx , Cx) ⟩ = (⟨ x , Bx ⟩ , ⟨ x , Cx ⟩)

{-
-- ×∃-implies-∃× doesn't hold as there is no guarantee that x ≡ y.
×∃-implies-∃× : ∀ {A : Set} {B C : A → Set}
    → (∃[ x ] B x) × (∃[ x ] C x) → ∃[ x ] (B x × C x)
×∃-implies-∃× (⟨ x , Bx ⟩ , ⟨ y , Cy ⟩) = _
-}

∃-⊎ : ∀ {P : Tri → Set} → (∃[ x ] P x) ≃ P aa ⊎ P bb ⊎ P cc
∃-⊎ {P} =
    record
        { to      = to
        ; from    = from
        ; from∘to = from∘to
        ; to∘from = to∘from
        }
    where
    to : (∃[ x ] P x) → P aa ⊎ P bb ⊎ P cc
    to ⟨ aa , Paa ⟩ = inj₁ Paa
    to ⟨ bb , Pbb ⟩ = inj₂ (inj₁ Pbb)
    to ⟨ cc , Pcc ⟩ = inj₂ (inj₂ Pcc)

    from : P aa ⊎ P bb ⊎ P cc → (∃[ x ] P x)
    from (inj₁ Paa)        = ⟨ aa , Paa ⟩
    from (inj₂ (inj₁ Pbb)) = ⟨ bb , Pbb ⟩
    from (inj₂ (inj₂ Pcc)) = ⟨ cc , Pcc ⟩

    from∘to : (x : ∃-syntax P) → from (to x) ≡ x
    from∘to ⟨ aa , Paa ⟩ = refl
    from∘to ⟨ bb , Pbb ⟩ = refl
    from∘to ⟨ cc , Pcc ⟩ = refl

    to∘from : (x : P aa ⊎ P bb ⊎ P cc) → to (from x) ≡ x
    to∘from (inj₁ Paa)        = refl
    to∘from (inj₂ (inj₁ Pbb)) = refl
    to∘from (inj₂ (inj₂ Pcc)) = refl

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-∃ : ∀ {n : ℕ} → even n → ∃[ m ] (m * 2 ≡ n)
odd-∃ : ∀ {n : ℕ} → odd n → ∃[ m ] (1 + m * 2 ≡ n)

even-∃ even-zero = ⟨ zero , refl ⟩
even-∃ (even-suc o) with odd-∃ o
...                    | ⟨ m , refl ⟩ = ⟨ suc m , refl ⟩

odd-∃ (odd-suc e) with even-∃ e
...                  | ⟨ m , refl ⟩ = ⟨ m , refl ⟩

∃-even : ∀ {n : ℕ} → ∃[ m ] (m * 2 ≡ n) → even n
∃-odd : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) → odd n

∃-even ⟨ zero  , refl ⟩ = even-zero
∃-even ⟨ suc m , refl ⟩ = even-suc (∃-odd ⟨ m , refl ⟩)

∃-odd ⟨ m , refl ⟩ = odd-suc (∃-even ⟨ m , refl ⟩)

∃-+-≤ : ∀ {n m : ℕ} → n ≤ m → ∃[ x ] (n + x ≡ m)
∃-+-≤ {zero} {m} z≤m = ⟨ m , refl ⟩
∃-+-≤ (s≤s n≤m) with ∃-+-≤ n≤m
...                | ⟨ m , refl ⟩ = ⟨ m , refl ⟩

≤-+-∃ : ∀ {n m : ℕ} → ∃[ x ] (n + x ≡ m) → n ≤ m
≤-+-∃ {zero}  ⟨ x , refl ⟩ = z≤n
≤-+-∃ {suc n} ⟨ x , refl ⟩ = s≤s (≤-+-∃ {n} ⟨ x , refl ⟩)

¬∃≃∀¬ : ∀ {A : Set} {B : A → Set}
    → (¬ ∃[ x ] B x) ≃ (∀ x → ¬ B x)
¬∃≃∀¬ {A} {B} =
    record
        { to      = to
        ; from    = from
        ; from∘to = λ _ → extensionality (λ { ⟨ _ , _ ⟩ → refl })
        ; to∘from = λ _ → refl
        }
    where
    to : ¬ ∃[ x ] B x → ∀ x → ¬ B x
    to ¬∃ x Bx = ¬∃ ⟨ x , Bx ⟩

    from : (∀ x → ¬ B x) → ¬ ∃[ x ] B x
    from ∀¬ ⟨ x , Bx ⟩ = ∀¬ x Bx

∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
    → ∃[ x ] (¬ B x) → ¬ (∀ x → B x)
∃¬-implies-¬∀ ⟨ x , ¬Bx ⟩ = λ B → ¬Bx (B x)

{-
-- ¬∀-implies-∃¬ does not hold because its unknown which x implies ¬ B x.
¬∀-implies-∃¬ : ∀ {A : Set} {B : A → Set}
    → ¬ (∀ x → B x) → ∃[ x ] (¬ B x)
¬∀-implies-∃¬ ¬∀ = ⟨ _ , _ ⟩
-}

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

-- https://gist.github.com/pedrominicz/1e85c4ab834a01e990f3e7bc3129e9a0
open import Relations using (One; Can; <>O; <>I; _O; _I; Can-to; to-O)

from-inc : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
from-inc <>                                                     = refl
from-inc (b O) rewrite from-inc b                               = refl
from-inc (b I) rewrite from-inc b | +-suc (from b) (from b + 0) = refl

Bin-isomorphism : ℕ ≃ ∃[ b ] (Can b)
Bin-isomorphism = record
    { to      = to'
    ; from    = from'
    ; from∘to = from∘to
    ; to∘from = to∘from
    }
    where
    to' : ℕ → ∃[ b ] (Can b)
    to' n = ⟨ to n , Can-to n ⟩

    from' : ∃[ b ] (Can b) → ℕ
    from' ⟨ b , _ ⟩ = from b

    from∘to : ∀ (x : ℕ) → from' (to' x) ≡ x
    from∘to zero                                        = refl
    from∘to (suc n) rewrite from-inc (to n) | from∘to n = refl

    to∘from : ∀ (x : ∃[ b ] (Can b)) → to' (from' x) ≡ x
    to∘from ⟨ <> O  , <>O    ⟩ = refl
    to∘from ⟨ <> I  , <>I    ⟩ = refl
    to∘from ⟨ (b O) , (can O) ⟩ rewrite to∘from ⟨ b , can ⟩ = ?
    to∘from ⟨ (b I) , (can I) ⟩ rewrite to∘from ⟨ b , can ⟩ = ?