Starting from today we are going to use Agda. In case you have a problem, you are encouraged to read the official documentation.

My previous script was buggy, please run again the magic command

`wget -O - http://inf551.mimram.fr/install.sh | /bin/sh`

This section is useful in order to install Agda on your personal computer, skip it if you are working in the TD rooms.

On your own computer, please *do not run the above script*, it is not supposed to work there.

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. If you want to install Atom, go on this page, download the `.deb`

archive and run

`sudo dpkg -i atom-amd64.deb`

(where `atom-amd64.deb`

is the file you just downloaded, which is supposed to be in the current directory). After that, install the plugins `agda-mode`

and `language-agda`

and, in the settings of `agda-mode`

, change the path of the Agda executable to

`/usr/bin/agda -i /usr/share/agda-stdlib`

Install brew by following these instructions (brew is a package manager for MacOS) and type

```
brew install agda emacs
agda-mode setup
```

Additionally, you can install Atom.

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. If you are using Atom and it complains that it cannot find Agda whereas it should, please follow these steps (on Windows 10):

- Go to the system’s
*Language settings* - Select
*Administrative language settings* - Click
*Change system locale…* - Check
*Beta: Use Unicode UTF-8 for worldwide language support*

In order to configure Atom (on whichever platform), you should

- go into the menu
*Edit > Preferences > Install*, - search for “
`agda`

”, and - install both
`agda-mode`

and`language-agda`

.

In the preferences, under the *Editor* tab, it is also recommended to activate the *Scroll Past End* checkbox. If Atom has trouble with finding Agda, you might have to change its path in the `agda-mode`

settings.

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.

If you are using Atom and `\`

is not working, you should use `alt-/`

.

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`

):

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,

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

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

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

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

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

The *conjunction* is defined in the module `Data.Product`

which you can use with

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

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

are in correspondence with those of type

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

and the converse implication

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

Do you understand this notation? (if not, ask). Or better, since we like UTF-8 symbols and infix notations:

where `↔`

is typed `\<->`

. With this notation, currying can now be expressed as

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))\). You might need to generalize the type of your projections `proj1`

and `proj2`

.

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

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:

Show that disjunction is commutative.

Show that conjunction distributes over disjunction.

We define *falsity* as

which is an inductive type with no constructor.

Show the elimination rule

Define *negation* as a function

Show the principle of contradiction:

Show the principle of non-contradiction:

Show the rule of introduction of double negation:

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

Show the principle of elimination of negation:

Show that the law of excluded middle is not falsifiable:

Show the following logical counterpart of Russell’s paradox:

Define truth `⊤`

as an inductive type.

Show that the hypothesis \(\top\) is always superfluous:

Show the de Morgan laws

and

We define the excluded middle principle by

and double negation elimination by

Show that lem implies nne:

Show the converse implication:

It can be useful to first show:

Show that the two above principle are equivalent with the *Pierce law*: