Starting from today we are going to use Agda. In case you have a problem, you are encouraged to read the official documentation.
This section is useful in order to install Agda on your personal computer, skip it if you are using the PCs of the TD room.
If you have a Linux distribution such as Ubuntu or Debian simply type
sudo apt-get install emacs agdain order to install Agda and Emacs.
Install brew by following these instructions (brew is a package manager for MacOS) and type
brew install agda emacs
agda-mode setupThe easiest way is to use Windows subsystem for Linux (aka WSL) and follow the above installation instructions for Linux.
The recommended editor is Emacs, which is already installed and configured in the TD rooms.
Some other editors however also have support for Agda:
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 |
Note: if some e appears when you type
C-c C-., you should run ibus-setup and disable
the C-. shortcut here (it is used in order to type
emoji…).
Agda heavily resorts to UTF-8 notations. The Emacs mode has some great support for it, allowing to enter symbols generally as you would do in LaTeX. Some useful ones are
| ∧ | \and |
⊤ | \top |
→ | \to |
| ∨ | \or |
⊥ | \bot |
¬ | \neg |
| ∀ | \all |
Π | \Pi |
λ | \Gl |
| ∃ | \ex |
Σ | \Sigma |
≡ | \Equiv |
| ℕ | \bN |
× | \times |
≤ | \le |
| ∈ | \in |
⊎ | \uplus |
∷ | \:: |
| ∎ | \qed |
₁ | \_1 |
⇒ | \=> |
| ⟨ | \< |
⟩ | \> |
Many other symbols can be found here.
Try to do by yourself the first proof of the course. Create a file
named TD5.agda and type (or copy) the following (recall
that “×” is entered with \times and “→” with
\to):
open import Data.Product
×-comm : (A B : Set) → (A × B) → (B × A)
×-comm A B p = ?Then
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.
Modify the proof so that the arguments A and
B are implicit.
We will now do some proofs in propositional logic. We recall that,
under the Curry-Howard correspondence the implication \(\Rightarrow\) corresponds to the arrow → of
Agda. For instance, if we want to prove \(A\Rightarrow A\), we will construct a term
of type A → A. For instance,
id : {A : Set} → A → A
id a = aGive a proof of \(A\Rightarrow B\Rightarrow A\):
K : {A B : Set} → A → B → AGive a proof of \((A\Rightarrow B)\Rightarrow A\Rightarrow B\):
app : {A B : Set} → (A → B) → A → BGive a proof of \((A\Rightarrow B\Rightarrow C)\Rightarrow B\Rightarrow A\Rightarrow C\)
flip : {A B C : Set} → (A → B → C) → B → A → CGive a proof of \((A\Rightarrow B)\Rightarrow(B\Rightarrow C)\Rightarrow(A\Rightarrow C)\):
comp : {A B C : Set} → (A → B) → (B → C) → (A → C)Give a proof of \((A\Rightarrow B\Rightarrow C)\Rightarrow(A\Rightarrow B)\Rightarrow A\Rightarrow C\):
S : {A B C : Set} → (A → B → C) → (A → B) → A → CThe conjunction is defined in the module
Data.Product which you can use with
open import Data.Product renaming (_×_ to _∧_)By default, following the Curry-Howard correspondence, the
conjunction \(\land\) is noted as a
product × on types in Agda. However, since we focus on logic here, we
use the renaming command in order to change the notation to
the usual ∧.
Give a proof of \((A\land B)\Rightarrow A\):
proj1 : {A B : Set} → (A ∧ B) → Aand a proof proj2 of \((A\land
B)\Rightarrow B\).
Give a proof of \(A\Rightarrow A\land A\).
Show that conjunction is commutative: \((A\land B)\Rightarrow(B\land A)\).
Most functional programming languages support Currying which is a principle according to which a function taking a pair of arguments can be transformed into one with two arguments and vice versa. For instance, in OCaml the functions of type
'a * 'b -> 'care in correspondence with those of type
'a -> 'b -> 'cShow that we have \((A\land B\Rightarrow C)\Rightarrow(A\Rightarrow B\Rightarrow C)\):
curry1 : {A B C : Set} → (A ∧ B → C) → (A → B → C)and the converse implication
curry2 : {A B C : Set} → (A → B → C) → (A ∧ B → C)All connectives are defined in Agda. For instance, following the usual definition
\[ A \Leftrightarrow B \qquad=\qquad (A\Rightarrow B)\land(B\Rightarrow A) \]
we can define equivalence in Agda by
equiv : (A B : Set) → Set
equiv A B = (A → B) ∧ (B → A)Do you understand this notation? (if not, ask). Or better, since we like UTF-8 symbols and infix notations:
_↔_ : (A B : Set) → Set
A ↔ B = (A → B) ∧ (B → A)where ↔︎ is typed \<->. With this
notation, currying can now be expressed as
currying : {A B C : Set} → (A ∧ B → C) ↔ (A → B → C)prove it (you can use previous proofs).
Show that conjunction on the target distributes over implication: \((A\Rightarrow(B\land C))\Leftrightarrow((A\Rightarrow B)\land(A\Rightarrow C))\).
Disjunction is defined in Agda in the module
Data.Sum. However, in order to see how it works, we define
it by hand (and use more usual notations):
data _∨_ (A B : Set) : Set where
left : A → A ∨ B
right : B → A ∨ BIt is an inductive type, which takes two parameters (A
and B of type Set) and returns a
Set. It has two constructors left and
right which respectively take an element of type
A and B as argument.
Show the elimination rule for disjunction:
or-elim : {A B C : Set} → (A ∨ B) → (A → C) → (B → C) → CShow that disjunction is commutative.
Show that conjunction distributes over disjunction.
dist : {A B C : Set} → (A ∧ (B ∨ C)) → (A ∧ B) ∨ (A ∧ C)We define falsity as
data ⊥ : Set wherewhich is an inductive type with no constructor.
Show the elimination rule
⊥-elim : {A : Set} → ⊥ → ADefine negation as a function
¬ : Set → SetShow the principle of contradiction:
contr : {A B : Set} → (A → B) → (¬ B → ¬ A)Show the principle of non-contradiction:
non-contr : {A : Set} → ¬ (A ∧ ¬ A)Show the rule of introduction of double negation:
nni : {A : Set} → A → ¬ (¬ A)Show that the principle of elimination of double negation is valid on \(\bot\):
⊥-nne : ¬ (¬ ⊥) → ⊥Show the principle of elimination of negation:
¬-elim : {A B : Set} → ¬ A → A → BShow the De Morgan laws
dm∧ : {A B : Set} → ¬ A ∧ ¬ B → ¬ (A ∨ B)and
dm∨ : {A B : Set} → ¬ A ∨ ¬ B → ¬ (A ∧ B)Can you manage to prove the converse implications?
Show that the law of excluded middle is not falsifiable:
nnlem : {A : Set} → ¬ (¬ (A ∨ (¬ A)))Show the following logical counterpart of Russell’s paradox:
rp : {A : Set} → (A → ¬ A) → ((¬ A) → A) → ⊥(Hint: there is a solution which does not require any previously defined function).
Define truth ⊤ as an inductive type.
Show that the hypothesis \(\top\) is always superfluous:
ti : {A : Set} → (⊤ → A) → AShow the de Morgan laws
dmnt : ¬ ⊤ → ⊥and
dmtn : ⊥ → ¬ ⊤We define the excluded middle principle by
lem : Set₁
lem = (A : Set) → A ∨ (¬ A)and double negation elimination by
nne : Set₁
nne = (A : Set) → ¬ (¬ A) → AShow that lem implies nne:
nne-lem : nne → lemShow the converse implication:
lem-nne : lem → nneIt can be useful to first show:
lem-nne' : (A : Set) → (A ∨ ¬ A) → ¬ (¬ A) → AShow that the two above principles are equivalent to the Pierce law:
pierce : Set₁
pierce = {A B : Set} → ((A → B) → A) → ASuppose fixed a set U, which will act as the universe
where variables range over. This can be achieved with
postulate U : SetA predicate \(P(x)\) will be encoded
as a function P of type U → Set which, given
an element \(x\) of U
returns a truth value. The formula \(\forall
x. P(x)\) can then be encoded as the type of (dependent)
functions
(x : U) → (P x)and the formula \(\exists x. P(x)\) will be encoded as
∃ (λ x → P x)(we will not detail what this notation means exactly for now, but a
witness is a pair consisting of an element t of
U, and an element of P t).
Given a predicate \(P(x,y)\), which depends on two variables, show the formula \[\forall x.\forall y.P(x,y)\Rightarrow \forall y.\forall x.P(x,y)\] by defining
∀-comm : {P : U → U → Set} →
((x : U) → (y : U) → P x y) → ((y : U) → (x : U) → P x y)Similarly, show that existential quantifications commute, i.e. \[\exists x.\exists y.P(x,y)\Rightarrow \exists y.\exists x.P(x,y)\] by defining
∃-comm : {P : U → U → Set} → ∃ (λ x → ∃ (λ y → P x y)) → ∃ (λ y → ∃ (λ x → P x y))Show the formula
\[\exists x.\forall y.P(x,y)\Rightarrow \forall y.\exists x.P(x,y)\]
Show the following formulas