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 online editor.

If you have a Linux distribution such as Ubuntu or Debian simply type

`sudo apt-get install agda emacs agda-mode`

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

Install the latest version found here (this is `Agda2.6.0.1.v1.msi`

at the time of this writing). After that, you still need to install the standard library by hand: it can be downloaded from here, and you should copy the contents of the `src`

directory of the archive to the `library`

directory of the Agda installed by the previous installer.

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.

Try to do by yourself the first proof of the course. Begin by typing (or copying) 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 `

TODO…..

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 `

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

TODO…