In the labs we are going to use Agda. In case you have a problem, feel free to - ask me, - have a look at this page recalling the basics of Agda, - read the official documentation.
All the labs are following each other: - you should work in the same directory for all labs - you should work regularly
The labs are graded: - the best and most simple is that you create a
private github repository for that and add me
(smimram) to it - otherwise, please send me regularly you
Agda files by mail
If you have a Linux distribution such as Ubuntu or Debian simply type
sudo apt-get install agdain order to install Agda.
If you have a permission denied problem with Ubuntu, you
have probably hit a known
bug in the package for the standard library
(agda-stdlib version 1.7.3-1). Make sure that we are
talking about the incriminated package by typing
apt-cache policy agda-stdliband check that the installed version is 1.7.3-1. If this
is the case, you can to the following in order to circumvent it. Type as
root:
cd /usr/share/agda-stdlib
echo "name: standard-library-1.7.1" > standard-library.agda-lib
echo "flags: -WnoUnsupportedIndexedMatch" >> standard-library.agda-lib
mkdir _build
chmod 777 _buildOn MacOS, you can install Agda via Homebrew with
brew install agdaBeware, you should also follow the instructions displayed in the end in order to properly install the standard library.
On Windows, you should use Windows subsystem for Linux (aka WSL) and refer to the above documentation for Linux.
The following editors support Agda:
agda-mode)If you are using VSCode you might need to type UTF-8 symbols as
*times instead of \times.
We recall that the most useful shortcuts are
| Shortcut | Effect |
|---|---|
C-c C-l |
typecheck and highlight the current file |
C-c C-, |
get information about the hole under the cursor |
C-c C-. |
show both the type of the current hole and of the proposed filling |
C-c C-space |
give a solution |
C-c C-c |
case analysis on a variable (≈ an elimination rule) |
C-c C-r |
refine the hole (≈ an introduction rule) |
C-c C-a |
automatic fill |
| middle click | definition of the term |
You first need to download our ``minimal standard library’’ which is in the file Prelude.agda and put it in the same directory as the one you will work in during the labs.
Have a look at this file.
Open a new file name Introduction.agda and type the
following (recall that “×” is entered with \times and “→”
with \to):
open import Prelude
comm× : {A B : Type} → A × B → B × A
comm× (a , b) = b , aThen
C-c C-l to load the file.C-c C-, to obtain the type of the hole.C-c C-c then p to observe the
argument.C-c C-r to refine the hole.C-c C-space.In this example, you could have directly defined the λ-term, but in general you will see that it is necessary to use the holes, so start getting used to those!
Show that product is commutative, i.e. provide a proof of
comm× : {A B : Type} → A × B → B × AShow that the function you have just defined is involutive:
comm×-involutive : {A B : Type} (a : A) (b : B) → comm× (comm× (a , b)) ≡ (a , b)We recall that the constructor for equality is called
refl.
Show that product is associative:
assoc× : {A B C : Type} → (A × B) × C → A × (B × C)Show that coproduct is commutative:
comm⊎ : {A B : Type} → A ⊎ B → B ⊎ AWe recall that the two canonical injections into the coproduct are
noted inl and inr, i.e. coproduct is defined as the
inductive type
data _⊎_ (A : Type) (B : Type) : Type where
inl : A → A ⊎ B
inr : B → A ⊎ BDefine a function comm⊎-involutive showing that the
function comm⊎ is involutive.
Show that product distributes over coproducts:
dist⊎ : {A B C : Type} → A × (B ⊎ C) → (A × B) ⊎ (A × C)Define equivalence with
_↔_ : (A B : Type) → Type
A ↔ B = (A → B) × (B → A)Show that we have the following equivalence:
currying : {A B C : Type} → (A × B → C) ↔ (A → B → C)We recall that you can capture the optional arguments by taking
arguments of the form {A}. It will be useful two define two
local functions, we recall that this can be done with the
where keyword.
We recall that natural numbers are defined in the standard library as
data ℕ : Type where
zero : ℕ
suc : ℕ → ℕDefine addition:
_+_ : ℕ → ℕ → ℕ(you should perform a recurrence on the first argument).
Define predecessor:
pred : ℕ → ℕShow that zero is neutral on the left for addition
unitl+ : (n : ℕ) → zero + n ≡ nShow that equality is a congruence:
cong : {A B : Type} (f : A → B) {x y : A} → x ≡ y → f x ≡ f yHint: we recall that equality is defined as the inductive type
data _≡_ {A : Type} (x : A) : (y : A) → Type where
refl : x ≡ xso that you can reason on equality proofs with pattern matching.
Show that zero is neutral on the right for addition:
assoc+ : (m n o : ℕ) → (m + n) + o ≡ m + (n + o)Show that equality is symmetric:
sym : {A : Type} {x y : A} → x ≡ y → y ≡ xShow that equality is transitive:
trans : {A : Type} {x y z : A} → x ≡ y → y ≡ z → x ≡ zShow the following useful lemma:
+suc : (m n : ℕ) → m + (suc n) ≡ suc (m + n)Show that addition is commutative:
comm+ : (m n : ℕ) → m + n ≡ n + mShow that predecessor is left inverse for successor:
pred-suc : (n : ℕ) → pred (suc n) ≡ nShow that successor is left inverse for predecessor on non-zero numbers:
suc-pred : (n : ℕ) → ¬ (n ≡ zero) → suc (pred n) ≡ nWe recall that ¬ A is defined as A → ⊥ and
that the recurrence principle for ⊥ is called
⊥-rec (it states that if we can prove false then anything
can be deduced).
Show that 0 is different from any succesor:
zero-suc : (n : ℕ) → ¬ (zero ≡ suc n)Show that successor is injective:
suc-inj : {m n : ℕ} → suc m ≡ suc n → m ≡ nShow that equality is decidable on natural numbers:
nat-eq-dec : (m n : ℕ) → (m ≡ n) ⊎ ¬ (m ≡ n)Define division by 2 on natural numbers:
div2 : (n : ℕ) → Σ ℕ (λ q → q + q ≡ n ⊎ suc (q + q) ≡ n)Show that equality is substitutive:
subst : {A : Type} (P : A → Type) {x y : A} → x ≡ y → P x → P yDefine the predicate of being even as
data Even : ℕ → Type where
evenZero : Even zero
evenSuc : {n : ℕ} → Even n → Even (suc (suc n))and show that doubling a natural number produces an even number:
double-even : (n : ℕ) → Even (n + n)