Starting from today we are going to use Agda. In case you have a problem, you are encouraged to read the official documentation.
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.
If you cannot manage to install Agda on your machine, ask for help. In the meantime, you can work via ssh on the machines from the computer room in the Turing building:
ssh -J samuel.mimram@login.dix.polytechnique.fr samuel.mimram@ablette.dix.polytechnique.fr(obviously, you need to replace samuel.mimram by you own
login above, twice).
The following editors support Agda:
agda-mode)
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 |
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.
Note: if you are using VS Code, the \ should be
replaced by *
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: you should change (A B : Set)
to {A B : Set} and remove the arguments A and
B in the last line.
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 diag of \(A\Rightarrow A\land A\).
Show that conjunction is commutative in a proof ∧-comm:
\((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 in a
proof →distrib: \[
(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 (or-comm).
Show that conjunction distributes over disjunction
(and-or-distrib).
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