Tutorial

Tutorials.Wednesday

Tutorials.Wednesday
{-# OPTIONS --allow-unsolved-metas #-}

open import Tutorials.Monday
open import Tutorials.Tuesday
open List using (List; []; _∷_; _++_)
open Vec using (Vec; []; _∷_; _!_)
open Fin using (Fin; zero; suc)
module Tutorials.Wednesday where

-----------
-- Interfaces, isomorphisms
-----------

module Isomorphism where
  -- Why can we import _,_ from both modules without resulting in a nameclash?
  open Simple using (_⊎_; _×_; _,_; inl; inr)
  open Product using (Σ-syntax; Σ-⊎; Σ-×; Π-×; Π-→; _,_)

  infix 2 _≅_
  record _≅_ (A B : Set) : Set where
    constructor Mk≅
    field
      to      : A  B
      from    : B  A
      from∘to :  a  from (to a)  a
      to∘from :  b  to (from b)  b

  open _≅_

  -- We can use copattern matching to construct a record by defining how to construct each of its fields
  Σ-⊎-≅ : Σ-⊎ A B  A  B
  Σ-⊎-≅ = {!!}

  Σ-×-≅ : Σ-× A B  A × B
  Σ-×-≅ = {!!}

  Π-→-≅ : Π-→ A B  (A  B)
  to Π-→-≅ = {!!}
  from Π-→-≅ = {!!}
  -- Needs η laws for functions (∀ x → f x) ≡ f
  from∘to Π-→-≅ = {!!}
  to∘from Π-→-≅ = {!!}

  -- The following isomorphism needs of function extensionality
  -- Function extensionality claims that if two functions give the same output on the same input, then they are equal
  -- This does not hold internally in Agda and we therefore need to postulate it as an axiom
  postulate
    extensionality : {P : A  Set} {f g : (a : A)  P a}  (∀ x  f x  g x)  f  g

  Π-×-≅ : Π-× A B  A × B
  Π-×-≅ = {!!}

  curry : Π-→ A (Π-→ B C)  Π-→ (Σ-× A B) C
  curry f (a , b) = f a b

  uncurry : Π-→ (Σ-× A B) C  Π-→ A (Π-→ B C)
  uncurry f a b = f (a , b)

  curry-uncurry : Π-→ A (Π-→ B C)  Π-→ (Σ-× A B) C
  curry-uncurry = {!!}

  Fin-≤-≅ : Fin m  Σ[ n   ] n < m
  Fin-≤-≅ = {!!}

  _iso-∘_ : B  C  A  B  A  C
  x iso-∘ y = {!!}

-----------
-- Decidability
-----------

module Dec where
  open Product using (_×_; _,_; fst; snd)
  open Simple using (¬_)

  data Dec (A : Set) : Set where
    yes :   A  Dec A
    no  : ¬ A  Dec A

  DecEq : Set  Set
  DecEq A = (x y : A)  Dec (x  y)

  map : (A  B)  (¬ A  B)  Dec A  B
  map f g (yes x) = f x
  map f g (no x) = g x

  infix 5 _×-dec_
  _×-dec_ : Dec A  Dec B  Dec (A × B)
  yes x ×-dec yes y = yes (x , y)
  yes x ×-dec no ¬y = no (¬y  snd)
  no ¬x ×-dec B? = no (¬x  fst)

  _ℕ-≟_ : (n m : )  Dec (n  m)
  n ℕ-≟ m = {!!}

  suc-injective : {i j : Fin n}  _≡_ {A = Fin (suc n)} (suc i) (suc j)  i  j
  suc-injective refl = refl

  _Fin-≟_ : (i j : Fin n)  Dec (i  j)
  zero Fin-≟ zero = yes refl
  zero Fin-≟ suc j = no λ ()
  suc i Fin-≟ zero = no λ ()
  suc i Fin-≟ suc j = map
    (yes  cong suc)
    (no   neq  neq  suc-injective))
    (i Fin-≟ j)

  ∷-injective : {x y : A} {xs ys : List A}  _≡_ {A = List A} (x  xs) (y  ys)  x  y × xs  ys
  ∷-injective refl = refl , refl

  List-≟ : (_A-≟_ : (x y : A)  Dec (x  y))  (xs ys : List A)  Dec (xs  ys)
  List-≟ _A-≟_ [] [] = yes refl
  List-≟ _A-≟_ [] (y  ys) = no λ ()
  List-≟ _A-≟_ (x  xs) [] = no λ ()
  List-≟ _A-≟_ (x  xs) (y  ys) = map
    (yes  Isomorphism.curry (cong₂ _∷_))
    (no   neq  neq  ∷-injective))
    (x A-≟ y ×-dec List-≟ _A-≟_ xs ys)

-----------
-- Interfaces
-----------

-- We define what it is to be a monoid on a carrier set C
record Monoid (C : Set) : Set where
  constructor MkMonoid
  field
    ε   : C
    _∙_ : C  C  C
    -- Including the algebraic laws
    idˡ : (x : C)  ε  x  x
    idʳ : (x : C)  x  ε  x
    assoc : (x y z : C)  (x  y)  z  x  (y  z)

module MonoidSolver (Symbol : Set) (symbol-≟ : Dec.DecEq Symbol) where
  -- The syntax for an expression tree of symbolic monoidal operations
  infixl 20 _‵∙_
  infix 25 ‵_
  data Expr : Set where
    ‵ε   : Expr
    ‵_   : Symbol  Expr
    _‵∙_ : Expr  Expr  Expr

  -- And define equations on monoids
  infix 10 _‵≡_
  record Eqn : Set where
    constructor _‵≡_
    field
      lhs : Expr
      rhs : Expr

  -- The canonical normal form for expression trees
  NormalForm : Set
  NormalForm = List Symbol

  normalise : Expr  NormalForm
  normalise ‵ε = []
  normalise ( x) = x  []
  normalise (xs ‵∙ ys) = normalise xs ++ normalise ys

  module Eval (M : Monoid C) where
    open Monoid M

    -- An environment maps symbols to values in the carrier set
    Env : Set
    Env = Symbol  C

    -- Evaluate the syntax in a given environment
    ⟦_⟧ : Expr  Env  C
     ‵ε  Γ = ε
      x  Γ = Γ x
     x ‵∙ y  Γ =  x  Γ   y  Γ

    -- Evaluate the normal form in a given environment
    ⟦_⟧⇓ : NormalForm  Env  C
     [] ⟧⇓ Γ = ε
     x  xs ⟧⇓ Γ = Γ x   xs ⟧⇓ Γ

    -- The evaluation of normal forms distributes over list concatenation
    ++-homo :  Γ (xs ys : NormalForm)   xs ++ ys ⟧⇓ Γ   xs ⟧⇓ Γ   ys ⟧⇓ Γ
    ++-homo Γ [] ys = sym (idˡ _)
    ++-homo Γ (x  xs) ys = begin
      Γ x   xs ++ ys ⟧⇓ Γ
        ≡⟨ cong (_ ∙_) (++-homo Γ xs ys) 
      Γ x  ( xs ⟧⇓ Γ   ys ⟧⇓ Γ)
        ≡⟨ sym (assoc _ _ _) 
      (Γ x   xs ⟧⇓ Γ)   ys ⟧⇓ Γ
        

    -- Normalising and then evaluating the normal form is equal to evaluating the original expression
    correct :  Γ (expr : Expr)   normalise expr ⟧⇓ Γ   expr  Γ
    correct Γ ‵ε = refl
    correct Γ ( x) = idʳ _
    correct Γ (le ‵∙ re) = begin
       normalise le      ++  normalise re ⟧⇓ Γ ≡⟨ ++-homo Γ (normalise le) (normalise re) 
       normalise le ⟧⇓ Γ   normalise re ⟧⇓ Γ ≡⟨ cong₂ _∙_ (correct Γ le) (correct Γ re) 
       le             Γ   re             Γ 

    -- We describe what it is to be a solution to an equation
    -- If both sides normalise to the same symbols in the same order,
    -- we claim that the monoid laws make the equations hold in any environment
    Solution : Eqn  Set
    Solution (lhs ‵≡ rhs) =
      Dec.map
        -- Both sides normalise to a common list of symbols, we must now show that the equation holds under any environment
         _   (Γ : Env)   lhs  Γ   rhs  Γ)
        -- Both sides do *not* normalise to a common list of symbols, we claim only the trivial
         _  )
        (Dec.List-≟ symbol-≟ (normalise lhs) (normalise rhs))

    -- Now that we have described what a solution is, we show that we can provide one
    solve : (eqn : Eqn)  Solution eqn
    -- Pattern matching using with makes the goal type compute
    solve (lhs ‵≡ rhs) with Dec.List-≟ symbol-≟ (normalise lhs) (normalise rhs)
    solve (lhs ‵≡ rhs) | Dec.no _ = tt
    solve (lhs ‵≡ rhs) | Dec.yes lhs⇓≡rhs⇓ = λ Γ  begin
       lhs  Γ            ≡⟨ sym (correct Γ lhs) 
       normalise lhs ⟧⇓ Γ ≡⟨ cong      ⟧⇓ Γ) lhs⇓≡rhs⇓ 
       normalise rhs ⟧⇓ Γ ≡⟨ correct Γ rhs 
       rhs  Γ            

open MonoidSolver

-- An example instance of a monoid: natural numbers with addition
NAT-MONOID : Monoid 
Monoid.ε NAT-MONOID = zero
Monoid._∙_ NAT-MONOID = _+_
Monoid.idˡ NAT-MONOID = +-idˡ
Monoid.idʳ NAT-MONOID = +-idʳ
Monoid.assoc NAT-MONOID = +-assoc

-- An example usage of the monoid solver
-- We first need to "quote" the goal, i.e. describe it in terms of the expression language / syntax
-- NAT-MONOID describes how to interpret the syntax back and evaluate the expression into a value of the carrier set
eqn₁-auto : (x y z : )  (0 + x) + y + (y + z)  x + (0 + y + 0) + (y + z + 0)
eqn₁-auto x y z =
  let
    ‵x = zero
    ‵y = suc zero
    ‵z = suc (suc zero)
    lhs = (‵ε ‵∙  ‵x) ‵∙  ‵y ‵∙ ( ‵y ‵∙  ‵z)
    rhs =  ‵x ‵∙ (‵ε ‵∙  ‵y ‵∙ ‵ε) ‵∙ ( ‵y ‵∙  ‵z ‵∙ ‵ε)
  in
  Eval.solve (Fin 3) Dec._Fin-≟_ NAT-MONOID (lhs ‵≡ rhs) λ where
    zero  x
    (suc zero)  y
    (suc (suc zero))  z