[Nottingham Internship] Agda

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}
    where
      lemma : {x y : X} → y ≢ x → y ∈ x ∷ [] → y ∈ []
      lemma y≢x here = ⊥-elim (y≢x refl)
      lemma y≢x (there ())
  ∈-delete x (x₁ ∷ []) (there ())
  ∈-delete x (.x ∷ x₂ ∷ l) here = (x₂ ∷ l) , lemma₂ {x}
    where
      lemma₂ : {x y : X} → y ≢ x → y ∈ x ∷ x₂ ∷ l → y ∈ x₂ ∷ l
      lemma₂ y≢x here = ⊥-elim (y≢x refl)
      lemma₂ y≢x (there y∈x∷x₂∷l) = y∈x∷x₂∷l
  ∈-delete x (x₁ ∷ x₂ ∷ l) (there x∈l) = let l' , p = ∈-delete x (x₂ ∷ l) x∈l
                                         in (x₁ ∷ l') , lemma₃ {p}
                                           where
                                             lemma₃ : {p : ∀ {y'} → y' ≢ x → y' ∈ (x₂ ∷ l) → y' ∈ proj₁ (∈-delete x (x₂ ∷ l) x∈l)}
                                                      → {y : X}
                                                      → y ≢ x → y ∈ x₁ ∷ x₂ ∷ l
                                                      → y ∈ x₁ ∷ proj₁ (∈-delete x (x₂ ∷ l) x∈l)
                                             lemma₃ y≢x here = here
                                             lemma₃ {p} y≢x (there y∈x₁∷x₂∷l) = there (p y≢x y∈x₁∷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₁) [] x∷l₁↪l₂ m<n _ with (x∷l₁↪l₂ {x} here)
  ... | ()
  pigeonhole {suc n} {suc m} l₁@(x ∷ l₁') l₂@(_ ∷ _) x∷l₁↪l₂ suc-m<suc-n
             (rec-not-repeats not-repeats-l₁' x∉l₁') with (x∷l₁↪l₂ {x} here)
  ... | x∈l₂ with (∈-delete x l₂ x∈l₂)
  ...           | (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₂')
                              where
                                l₁'↪l₂' : ∀ {x'} → x' ∈ l₁' → x' ∈ l₂'
                                l₁'↪l₂' {x'} x'∈l₁' = let x'∈l₂ = (x∷l₁↪l₂ (there x'∈l₁')) -- x' ∈ l₂ ≡ l₂' ∪ x
                                                      in p (not-in-not-equal x'∈l₁' x∉l₁') x'∈l₂
                                                        where
                                                          not-in-not-equal : ∀ {k} {y x' : X} {l : Vec X k} → (y ∈ l) → ¬ (x' ∈ l) → y ≢ x'
                                                          not-in-not-equal y∈l x'∉l y≡x rewrite y≡x = ⊥-elim (x'∉l y∈l)

                                m<n : ∀ {m' n'} → suc m' < suc n' → m' < n'
                                m<n (s≤s suc-m<suc-n₁) = suc-m<suc-n₁