[Nottingham Internship] Agda

3 minute read

Agda is a dependently typed functional programming language: I’ll try to make use of it to formalize $𝜔$-groupoids.

Watch out!: On macOS, when installing Agda with homebrew:

 brew install agda

if you have problems with emacs and the standard library (with errors such as failed to find source of module Data.Nat for instance), try this:

 mkdir -p ~/.agda
 echo /usr/local/lib/agda/standard-library.agda-lib >> ~/.agda/libraries
 echo standard-library >> ~/.agda/defaults

it took me a while to figure that out…

For example, here is my version of the Pigeonhole Principle in Agda:

open import Data.Nat
open import Data.Nat.Base
open import Relation.Nullary
open import Data.Vec
open import Data.Product
open import Data.Empty

open import Relation.Binary.PropositionalEquality

-- inspired by https://github.com/youqad/Coq_Project/blob/master/pigeonhole.v

module pigeonhole {X : Set} where

  data not-repeats :  {n}  Vec X n  Set where
    base-not-repeats : not-repeats []
    rec-not-repeats :  {x n}  {l : Vec X n}  not-repeats l  ¬ (x  l)  not-repeats (x  l)

  repeats :  {n}  Vec X n  Set
  repeats l = ¬ not-repeats l

  __ :  {n m}  Vec X n  Vec X m  Set
  l  l' =  {x}  x  l  x  l'

  -delete :  {n}  (x : X)  (l : Vec X (suc n))  x  l
              Σ[ l'  Vec X n ] ( {y}  y  x  y  l  y  l')
  -delete x (.x  []) here = [] , lemma {x}
      lemma : {x y : X}  y  x  y  x  []  y  []
      lemma yx here = -elim (yx refl)
      lemma yx (there ())
  -delete x (x  []) (there ())
  -delete x (.x  x  l) here = (x  l) , lemma {x}
      lemma : {x y : X}  y  x  y  x  x  l  y  x  l
      lemma yx here = -elim (yx refl)
      lemma yx (there yxx₂∷l) = yxx₂∷l
  -delete x (x  x  l) (there xl) = let l' , p = -delete x (x  l) xl
                                         in (x  l') , lemma {p}
                                             lemma : {p :  {y'}  y'  x  y'  (x  l)  y'  proj (-delete x (x  l) xl)}
                                                       {y : X}
                                                       y  x  y  x  x  l
                                                       y  x  proj (-delete x (x  l) xl)
                                             lemma yx here = here
                                             lemma {p} yx (there yx₁∷x₂∷l) = there (p yx yx₁∷x₂∷l)

  pigeonhole :  {n m} (l : Vec X n) (l : Vec X m)  l  l  m < n  repeats l
  pigeonhole [] l l₁↪l ()
  pigeonhole (x  l) [] xl₁↪l m<n _ with (xl₁↪l {x} here)
  ... | ()
  pigeonhole {suc n} {suc m} l@(x  l') l@(_  _) xl₁↪l suc-m<suc-n
             (rec-not-repeats not-repeats-l' xl') with (xl₁↪l {x} here)
  ... | xl with (-delete x l xl)
  ...           | (l' , p) = -elim ((pigeonhole l' l' l'l' (m<n suc-m<suc-n)) not-repeats-l') -- p : (∀ {y} → y ≢ x → y ∈ l₂ → y ∈ l₂')
                                l'l' :  {x'}  x'  l'  x'  l'
                                l'l' {x'} x'l' = let x'l = (xl₁↪l (there x'l')) -- x' ∈ l₂ ≡ l₂' ∪ x
                                                      in p (not-in-not-equal x'l' xl') x'l
                                                          not-in-not-equal :  {k} {y x' : X} {l : Vec X k}  (y  l)  ¬ (x'  l)  y  x'
                                                          not-in-not-equal yl x'l yx rewrite yx = -elim (x'l yl)

                                m<n :  {m' n'}  suc m' < suc n'  m' < n'
                                m<n (ss suc-m<suc-n) = suc-m<suc-n

Leave a comment