Propositional logic in Agda

Samuel Mimram

1 Getting started

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

1.1 Getting everything ready

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

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

1.2 Installing Agda on your own computer

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.

1.2.1 Linux

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

1.2.2 MacOS

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.

1.2.3 Windows

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

1.2.4 Atom

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

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.

1.3 Shortcuts

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

1.4 Symbols

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-/.

2 Our first proof

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

×-comm : (A B : Set)  (A × B)  (B × A)
×-comm A B p = ?

Then

  1. Use C-c C-l to load the file.
  2. Use C-c C-, to obtain the type of the hole.
  3. Use C-c C-c then p to observe the argument.
  4. Use C-c C-r to refine the hole.
  5. 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.

3 Implication

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 = a

3.1 First projection

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

K : {A B : Set}  A  B  A

3.2 Application

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

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

3.3 Flip

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

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

3.4 Transitivity / composition

Give 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)

3.5 S

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  C

4 Conjunction

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 .

4.1 Projections

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

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

and a proof proj2 of \((A\land B)\Rightarrow B\).

4.2 Diagonal

Give a proof of \(A\Rightarrow A\land A\).

4.3 Commutativity

Show that conjunction is commutative: \((A\land B)\Rightarrow(B\land A)\).

4.4 Currying

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

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).

4.5 Optional: distributivity

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.

5 Disjunction

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 ∨ B

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.

5.1 Elimination rule

Show the elimination rule for disjunction:

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

5.2 Commutativity

Show that disjunction is commutative.

5.3 Distributivity

Show that conjunction distributes over disjunction.

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

6 Negation

6.1 Falsity

We define falsity as

data: Set where

which is an inductive type with no constructor.

Show the elimination rule

⊥-elim : {A : Set}  A

6.2 Negation

Define negation as a function

¬ : Set  Set

6.3 Contradiction

Show the principle of contradiction:

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

6.4 Non-contradiction

Show the principle of non-contradiction:

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

6.5 Double negation introduction

Show the rule of introduction of double negation:

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

6.6 Double negation elimination on \(\bot\)

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

⊥-nne : ¬ (¬ ⊥) 

6.7 Elimination of negation

Show the principle of elimination of negation:

¬-elim : ¬ A  A  B

6.8 Non-falsifiability of the law of excluded middle

Show that the law of excluded middle is not falsifiable:

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

6.9 Russell’s paradox

Show the following logical counterpart of Russell’s paradox:

rp : {A : Set}  (A  ¬ A)  (¬ A  A) 

7 Truth

7.1 Definition

Define truth as an inductive type.

7.2 ⊤-strengthening

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

ti : {A : Set}  ( A)  A

7.3 De Morgan

Show the de Morgan laws

dmnt : ¬ ⊤ 

and

dmtn : ¬ ⊤

8 Classical logic

8.1 Equivalence between excluded middle and double negation elimination

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)  A

Show that lem implies nne:

nne-lem : nne  lem

Show the converse implication:

lem-nne : lem  nne

It can be useful to first show:

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

8.2 Pierce law

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

pierce : Set₁
pierce = (A B : Set)  ¬ (¬ (((A  B)  A)  A))