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 agda`

in 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 setup
```

The 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:

- VSCode with the dedicated Agda mode
- Atom with the dedicated Agda mode
- vim with the dedicated 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 |

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
: (A B : Set) → (A × B) → (B × A)
×-comm = ? ×-comm A B p
```

Then

- Use
`C-c C-l`

to load the file. - Use
`C-c C-,`

to obtain the type of the hole. - Use
`C-c C-c`

then`p`

to observe the argument. - Use
`C-c C-r`

to refine the hole. - Enter the answers in the two holes and use
`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,

```
: {A : Set} → A → A
id = a id a
```

Give a proof of \(A\Rightarrow B\Rightarrow A\):

`: {A B : Set} → A → B → A K `

Give a proof of \((A\Rightarrow B)\Rightarrow A\Rightarrow B\):

`: {A B : Set} → (A → B) → A → B app `

Give a proof of \((A\Rightarrow B\Rightarrow C)\Rightarrow B\Rightarrow A\Rightarrow C\)

`: {A B C : Set} → (A → B → C) → B → A → C flip `

Give a proof of \((A\Rightarrow B)\Rightarrow(B\Rightarrow C)\Rightarrow(A\Rightarrow C)\):

`: {A B C : Set} → (A → B) → (B → C) → (A → C) comp `

Give a proof of \((A\Rightarrow B\Rightarrow C)\Rightarrow(A\Rightarrow B)\Rightarrow A\Rightarrow C\):

`: {A B C : Set} → (A → B → C) → (A → B) → A → C S `

The *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\):

`: {A B : Set} → (A ∧ B) → A proj1 `

and 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 -> 'c`

are in correspondence with those of type

` 'a -> 'b -> 'c`

Show that we have \((A\land B\Rightarrow C)\Rightarrow(A\Rightarrow B\Rightarrow C)\):

`: {A B C : Set} → (A ∧ B → C) → (A → B → C) curry1 `

and the converse implication

`: {A B C : Set} → (A → B → C) → (A ∧ B → C) curry2 `

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

```
: (A B : Set) → Set
equiv = (A → B) ∧ (B → A) equiv A B
```

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) ∧ (B → A) A ↔ B
```

where `↔︎`

is typed `\<->`

. With this
notation, currying can now be expressed as

`: {A B C : Set} → (A ∧ B → C) ↔ (A → B → C) currying `

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
: A → A ∨ B
left : B → A ∨ B right
```

It 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:

`: {A B C : Set} → (A ∨ B) → (A → C) → (B → C) → C or-elim `

Show that disjunction is commutative.

Show that conjunction distributes over disjunction.

`: {A B C : Set} → (A ∧ (B ∨ C)) → (A ∧ B) ∨ (A ∧ C) dist `

We define *falsity* as

`data ⊥ : Set where`

which is an inductive type with no constructor.

Show the elimination rule

`: {A : Set} → ⊥ → A ⊥-elim `

Define *negation* as a function

`: Set → Set ¬ `

Show the principle of contradiction:

`: {A B : Set} → (A → B) → (¬ B → ¬ A) contr `

Show the principle of non-contradiction:

`: {A : Set} → ¬ (A ∧ ¬ A) non-contr `

Show the rule of introduction of double negation:

`: {A : Set} → A → ¬ (¬ A) nni `

Show that the principle of elimination of double negation is valid on \(\bot\):

`: ¬ (¬ ⊥) → ⊥ ⊥-nne `

Show the principle of elimination of negation:

`: {A B : Set} → ¬ A → A → B ¬-elim `

Show the De Morgan laws

`: {A B : Set} → ¬ A ∧ ¬ B → ¬ (A ∨ B) dm∧ `

and

`: {A B : Set} → ¬ A ∨ ¬ B → ¬ (A ∧ B) dm∨ `

Can you manage to prove the converse implications?

Show that the law of excluded middle is not falsifiable:

`: {A : Set} → ¬ (¬ (A ∨ (¬ A))) nnlem `

Show the following logical counterpart of Russell’s paradox:

`: {A : Set} → (A → ¬ A) → ((¬ A) → A) → ⊥ rp `

(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:

`: {A : Set} → (⊤ → A) → A ti `

Show the de Morgan laws

`: ¬ ⊤ → ⊥ dmnt `

and

`: ⊥ → ¬ ⊤ dmtn `

We define the excluded middle principle by

```
: Set₁
lem = (A : Set) → A ∨ (¬ A) lem
```

and double negation elimination by

```
: Set₁
nne = (A : Set) → ¬ (¬ A) → A nne
```

Show that lem implies nne:

`: nne → lem nne-lem `

Show the converse implication:

`: lem → nne lem-nne `

It can be useful to first show:

`: (A : Set) → (A ∨ ¬ A) → ¬ (¬ A) → A lem-nne' `

Show that the two above principles are equivalent to the *Pierce
law*:

```
: Set₁
pierce = {A B : Set} → ((A → B) → A) → A pierce
```

Suppose fixed a set `U`

, which will act as the universe
where variables range over. This can be achieved with

`postulate U : Set`

A 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

```
: {P : U → U → Set} →
∀-comm ((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

`: {P : U → U → Set} → ∃ (λ x → ∃ (λ y → P x y)) → ∃ (λ y → ∃ (λ x → P x y)) ∃-comm `

Show the formula

\[\exists x.\forall y.P(x,y)\Rightarrow \forall y.\exists x.P(x,y)\]

Show the following formulas

- \((\forall x.P(x))\lor(\forall x.Q(x))\Rightarrow \forall x.(P(x)\lor Q(x))\)
- \((\forall x.P(x)\land Q(x))\Leftrightarrow ((\forall x.P(x))\land(\forall x.Q(x)))\)
- \((\exists x.\lnot P(x))\Rightarrow\lnot(\forall x.P(x))\)
- \((\forall x.\lnot P(x))\Rightarrow\lnot(\exists x.P(x))\)