{
"cells": [
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"hide_input": true,
"id": 121,
"summary": true
},
"source": [
"Summary
code.id, code.fst, code.impl, code.lab01.ex01, code.lab01.ex01, code.and, code.lab01.ex04, code.lab01.ex05, code.or, code.lab01.ex5, code.lab01.ex5, code.lab01.distr, code.lab01.distr, code.true-false, code.neg, code.lab01.ex02, code.lab01.ex02, code.lab01.ex03, code.lab01.ex03, code.lab01.ex07, code.lab01.ex07, code.lab01.ex07, code.lab01.ex07, code.conn, code.lab01.ex03, code.lab01.ex03, code.lab01.irref, code.lab01.irref, code.lab01.weak-peirce, code.lab01.weak-peirce, code.lab01.LEM-eq, code.lab01.LEM-eq, code.lab01.weak-LEM, code.lab01.weak-LEM\n"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/id.agda",
"holes": [],
"moduleName": "code.id",
"preambleLength": 0
},
"source": [
"**LICENCE:**\n",
"This tutorial contains adaptations of material from [Programming Language Foundations in Agda](https://plfa.github.io/) by Phil Wadler and Wen Kokke. It is licensed under Creative Commons Attribution 4.0 International.\n",
"\n",
"**SYNTAX:**\n",
"You can enter `→` by writing `->` and pressing TAB; pressing TAB again goes back to `->`. Similar useful combinations are:\n",
"\n",
"| base form | alternate form |\n",
"|:---------:|:--------------:|\n",
"| -> | → |\n",
"| \\ | λ |\n",
"| neg | ¬ |\n",
"| top | ⊤ |\n",
"| bot | ⊥ |\n",
"| /\\ | ∧ |\n",
"| \\\\/ | ∨ |\n",
"| < | ⟨ |\n",
"| > | ⟩ |\n",
"| forall | ∀ |\n",
"| exists | ∃ |\n",
"| Pi | Π |\n",
"| Sigma | Σ |\n",
"\n",
"\n",
"\n",
"\n",
"\n",
"\n",
"\n",
"# Curry-Howard isomorphism\n",
"\n",
"| Logic | Programming | |\n",
"|----------|-------------|-----|\n",
"| theorems | types | $A$ |\n",
"| proofs | programs (terms) | $a$ |\n",
"| proof simplification | program execution | run $a$ |\n",
"| proof development | programming | write $a$ |\n",
"| proof checking | type checking | given $a, A$, does $a : A$ hold? |\n",
"| validity | type inhabitation | given $A$, find $a$ s.t. $a : A$ |\n",
"| ? | type reconstruction | given $a$, find $A$ s.t. $a : A$ |\n",
"\n",
"\n",
"\n",
"# Polymorphism and implicit arguments\n",
"\n",
"````\n",
"module code.id where\n",
"````\n",
"\n",
"The polymorphic identity function in Agda is written as follows:\n",
"\n",
"```\n",
"id : (A : Set) → A → A\n",
"id A x = x\n",
"```\n",
"\n",
"(Compare this with the equivalent Haskell definition:\n",
"```haskell\n",
"id :: A -> A\n",
"id x = x\n",
"```\n",
"Incidentally, note the crucial difference that the typing operator in Agda is `:` instead of `::`.)\n",
"\n",
"Therefore, in Agda `id ℕ` is the identity on the natural numbers,\n",
"`id (ℕ → ℕ)` is the identity on functions of natural numbers,\n",
"and so on.\n",
"It turns out that 1) specifying the argument `A` is boring\n",
"and 2) in most cases Agda can infer it from the context.\n",
"For these two reasons, Agda allows us to say that some argument is implicit `{A : Set}`, as we demonstrate below.\n",
"\n",
"````\n",
"id : {A : Set} → A → A\n",
"id x = x\n",
"````"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"**UNDER THE HOOD:** A code cell must start with a line in the format\n",
"\n",
"```agda\n",
"module A.B.C where\n",
"```\n",
"\n",
"Upon evaluation, the file `A/B/C.agda` is created on disk from the cell's contents\n",
"and fed to the Agda interpreter.\n",
"For this reason, it is important to evaluate a cell to ensure that its changes are reflected on disk and can be used from other cells.\n",
"\n",
"**SPACING:**\n",
"Agda allows us to be very flexible in the variable names,\n",
"which can be strings such as `x`, `idλ`, `a→b`, `&&true`, or even arbitrary unicode symbols `💔`, provided there is no space in-between.\n",
"As a consequence, spaces in Agda have a syntactic meaning as separators,\n",
"and we need to be very generous with them."
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/Workspace/teaching/Teaching/2018-2019/summer semester/LDI (logika dla informatyków)/lab/agda/code/id.agda",
"holes": [],
"moduleName": "code.id",
"preambleLength": 0
},
"source": [
"## Exercise\n",
"\n",
"Write polymorphic functions `fst` and `snd` that takes two arguments of types `A` and `B`,\n",
"and return the first, resp., second argument."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
2,
2,
3,
3,
5,
5,
6,
6
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/fst.agda",
"holes": [
2,
2,
3,
3,
5,
5,
6,
6
],
"id": 54,
"moduleName": "code.fst",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.fst where\n",
"\n",
"fst : {A B : Set} → ?\n",
"fst = ?\n",
"\n",
"snd : {A B : Set} → ?\n",
"snd = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/impl.agda",
"holes": [],
"moduleName": "code.impl",
"preambleLength": 0
},
"source": [
"# Intuitionistic propositional logic in Agda\n",
"\n",
"## Implication\n",
"\n",
"````\n",
"module code.impl where\n",
"````\n",
"\n",
"Intuitionistic implication is implemented as *function space*\n",
"$$A \\to B.$$\n",
"This concept has no counterpart in classical logic.\n",
"The function space operator `→` is an Agda primitive.\n",
"The idea is that a proof of $A \\to B$\n",
"is a (terminating) *program* $t : A \\to B$\n",
"that, given a proof $a : A$ of $A$,\n",
"always terminates and produces a proof $t\\; a : B$ of $B$.\n",
"The $\\to$-eliminaton rule is implemented by *function application*.\n",
"\n",
"````\n",
"apply : {A B : Set} → (A → B) → A → B\n",
"apply a→b = λ a → a→b a\n",
"````\n",
"\n",
"Equivalent spellings:\n",
"`apply a→b a = a→b a`,\n",
"` apply a→b = a→b`,\n",
"`apply = id` (why?).\n",
"The last case shows why do not need to explicitly use `apply`.\n",
"\n",
""
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise**\n",
"\n",
"Prove in Agda following tautologies of intuitionistic propositional logic:\n",
"1. Argument commutativity: $(A \\to B \\to C) \\to B \\to A \\to C$.\n",
"2. Distributivity: $(A \\to B \\to C) \\to (A \\to B) \\to A \\to C$.\n",
"3. Diamond $(A \\to B) \\to (A \\to C) \\to (B \\to C \\to D) \\to A \\to D$.\n",
"4. Projection: $A \\to A \\to A$. How many proof of this fact are there?\n",
"\n",
"Note that the operator \"$\\to$\" is right-associative:\n",
"For example, the last expression above is parenthesized as\n",
"$$ A \\to (A \\to A).$$\n",
"We will only write parentheses when they are needed.\n",
"\n",
"Also note that, since intuitionistic implication in general behaves differently from classical implication,\n",
"the intuitionistic tautologies above hold for reasons which are different from why the same formulas are also classical tautologies (and thus must be reproven in the inuitionistic setting)."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
3,
3,
6,
6,
9,
9,
12,
12
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex01.agda",
"holes": [
3,
3,
6,
6,
9,
9,
12,
12
],
"moduleName": "code.lab01.ex01",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex01 where\n",
"\n",
"→-comm : {A B C : Set} → (A → B → C) → B → A → C\n",
"→-comm f b a = ?\n",
"\n",
"→-distr : {A B C : Set} → (A → B → C) → (A → B) → A → C\n",
"→-distr f g x = ?\n",
"\n",
"→-diamond : {A B C D : Set} → (A → B) → (A → C) → (B → C → D) → A → D\n",
"→-diamond f g h x = ?\n",
"\n",
"→-proj : {A : Set} → A → A → A\n",
"→-proj = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/and.agda",
"holes": [],
"moduleName": "code.and",
"preambleLength": 0
},
"source": [
"## Conjunction\n",
"\n",
"````\n",
"module code.and where\n",
"````\n",
"\n",
"In intuitionistic logic, a proof of $A \\wedge B$ is a pair $\\langle a, b \\rangle$,\n",
"where $a$ is a proof of $A$ and $b$ is a proof of $B$.\n",
"(From this point of view, intuitionistic conjunction behaves similarly to classical conjunction,\n",
"because also in classical logic both conjuncts must be provable for their conjunction to be provable.)\n",
"This intuition translates immediately into the following *product* datatype:\n",
"\n",
"````\n",
"data _∧_ (A : Set) (B : Set) : Set where\n",
" ⟨_,_⟩ : A → B → A ∧ B\n",
"````\n",
"\n",
"The datatype `_∧_` is parametrised by two types, `A` and `B`,\n",
"and it is written `A ∧ B` or, using prefix notation, `_∧_ A B`.\n",
"It has only one constructor `⟨_,_⟩`, corresponding to the ∧-introduction rule:\n",
"Given elements `a : A` and `b : B`, `⟨ a , b ⟩` has type `A ∧ B` (notice the mandatory spaces!).\n",
"The term above can also be written in prefix notation as `⟨_,_⟩ A B`.\n",
"We can then define the two projection functions, which correspond to the two ∧-elimination rules:\n",
"\n",
"````\n",
"fst : {A B : Set} → A ∧ B → A\n",
"fst ⟨ a , _ ⟩ = a\n",
"\n",
"snd : {A B : Set} → A ∧ B → B\n",
"snd ⟨ _ , b ⟩ = b\n",
"````\n",
"\n",
"It is sometimes convenient to write longer conjunctions such as `A ∧ B ∧ C`,\n",
"to which end we need to define that the operator `_∧_` is *right associative*.\n",
"\n",
"````\n",
"infixr 2 _∧_\n",
"````\n",
"\n",
"We will also give it a numerical priority, `2` in this case,\n",
"in order to avoid ambiguity later then introducing more operators.\n",
"\n",
"Once again, `_∧_ ` is not an Agda primitive, but it can be defined with Agda's datatype creation facility."
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise**\n",
"\n",
"Formalise and prove the following:\n",
"1. Curry/uncurry: $A → B → C$ is the same as $A \\wedge B → C$.\n",
"2. Conjunction is commutative: $A \\wedge B$ is the same as $B \\wedge A$.\n",
"3. Conjunction is associative: $A \\wedge B \\wedge C$ is the same as $(A \\wedge B) \\wedge C$.\n",
"4. Implication distributes over conjunction: $A \\to B \\wedge C$ is the same as $(A \\to B) \\wedge (A \\to C)$.\n",
"\n",
"Do the last three properties follow from curry/uncurry?"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
4,
4,
7,
7,
9,
9,
10,
10,
12,
12,
13,
13,
15,
15,
16,
16,
18,
18,
19,
19,
21,
21,
22,
22
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex04.agda",
"holes": [
4,
4,
7,
7,
9,
9,
10,
10,
12,
12,
13,
13,
15,
15,
16,
16,
18,
18,
19,
19,
21,
21,
22,
22
],
"moduleName": "code.lab01.ex04",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex04 where\n",
"open import code.and\n",
"\n",
"uncurry : {A B C : Set} → (A → B → C) → A ∧ B → C\n",
"uncurry = ?\n",
"\n",
"curry : {A B C : Set} → (A ∧ B → C) → A → B → C\n",
"curry = ?\n",
"\n",
"∧-comm : ?\n",
"∧-comm = ?\n",
"\n",
"∧-assoc-1 : ?\n",
"∧-assoc-1 = ?\n",
"\n",
"∧-assoc-2 : ?\n",
"∧-assoc-2 = ?\n",
"\n",
"→∧-distr-1 : ?\n",
"→∧-distr-1 = ?\n",
"\n",
"→∧-distr-2 : ?\n",
"→∧-distr-2 = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/or.agda",
"holes": [],
"moduleName": "code.or",
"preambleLength": 0
},
"source": [
"## Disjunction\n",
"\n",
"````\n",
"module code.or where\n",
"````\n",
"\n",
"In intuitionistic logic a proof of a disjunction is a proof of either the first disjunct or of the second.\n",
"More precisely, a proof of $A_1 \\vee A_2$ is a pair $(k, t_k)$,\n",
"where $k \\in \\{1, 2\\}$ specifies that we are proving $A_k$\n",
"and $t_k : A_k$ is a proof thereof.\n",
"The two options can be implemented with two different constructors,\n",
"called right and left *injection*.\n",
"\n",
"````\n",
"data _∨_ (A : Set) (B : Set) : Set where\n",
" left : A → A ∨ B\n",
" right : B → A ∨ B\n",
"````\n",
"\n",
"The two constructors `left` and `right` above\n",
"correspond to the two ∨-introduction rules.\n",
"\n",
"Notice that this is very different from classical logic\n",
"(where it is \"easier\" to prove a disjunction),\n",
"because a classical proof does not need to prove any single disjunct.\n",
"\n",
"We give disjunction lower priority than conjunction\n",
"so we can omit parenthesis from `(A ∧ B) ∨ C` and write `A ∧ B ∨ C` instead.\n",
"\n",
"````\n",
"infixr 1 _∨_ \n",
"````\n",
"\n",
"The ∨-elimination rule is provided by case analysis,\n",
"which is implemented by performing pattern matching on the constructor.\n",
"\n",
"\n",
"````\n",
"case : {A B C : Set} → (A → C) → (B → C) → A ∨ B → C\n",
"case f g (left x) = f x\n",
"case f g (right x) = g x\n",
"````"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise**\n",
"\n",
"Formalise and prove the following:\n",
"1. Disjunction is commutative: $A \\vee B$ is the same as $B \\vee A$.\n",
"2. Disjunction is associative: $A \\vee B \\vee C$ is the same as $(A \\vee B) \\vee C$.\n",
"3. $A \\vee B \\to C$ is the same as $(A \\to C) \\wedge (B \\to C)$."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
4,
4,
5,
5,
7,
7,
8,
8,
10,
10,
11,
11,
13,
13,
14,
14
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex5.agda",
"holes": [
4,
4,
5,
5,
7,
7,
8,
8,
10,
10,
11,
11,
13,
13,
14,
14
],
"id": 105,
"moduleName": "code.lab01.ex5",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex5 where\n",
"open import code.and\n",
"open import code.or\n",
"\n",
"∨-comm : {A B : Set} → ?\n",
"∨-comm = ?\n",
"\n",
"∨-assoc : {A B C : Set} → ?\n",
"∨-assoc = ?\n",
"\n",
"∨∧→-1 : {A B C : Set} → ?\n",
"∨∧→-1 = ?\n",
"\n",
"∨∧→-2 : {A B C : Set} → ?\n",
"∨∧→-2 = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise** (`∧` and `∨`)\n",
"\n",
"Prove the following tautologies:\n",
"1. $A \\wedge (B \\vee C) \\leftrightarrow A \\wedge B \\vee A \\wedge C$.\n",
"2. $A \\vee B \\wedge C \\leftrightarrow (A \\vee B) \\wedge (A \\vee C)$."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
5,
5,
8,
8,
11,
11,
14,
14
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/distr.agda",
"holes": [
5,
5,
8,
8,
11,
11,
14,
14
],
"moduleName": "code.lab01.distr",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.distr where\n",
"open import code.and\n",
"open import code.or\n",
"\n",
"∧∨-distr-1 : {A B C : Set} → A ∧ (B ∨ C) → A ∧ B ∨ A ∧ C\n",
"∧∨-distr-1 = ?\n",
"\n",
"∧∨-distr-2 : {A B C : Set} → A ∧ B ∨ A ∧ C → A ∧ (B ∨ C)\n",
"∧∨-distr-2 = ?\n",
"\n",
"∨∧-distr-1 : {A B C : Set} → A ∨ B ∧ C → (A ∨ B) ∧ (A ∨ C)\n",
"∨∧-distr-1 = ?\n",
"\n",
"∨∧-distr-2 : {A B C : Set} → (A ∨ B) ∧ (A ∨ C) → A ∨ B ∧ C\n",
"∨∧-distr-2 = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/true-false.agda",
"holes": [],
"moduleName": "code.true-false",
"preambleLength": 0
},
"source": [
"## Truth values\n",
"\n",
"````\n",
"module code.true-false where\n",
"````\n",
"\n",
"The two truth values `⊤` and `⊥` are implemented via Agda's data type mechanism.\n",
"Notice that neither `⊤` nor `⊥` are Agda primitives.\n",
"However, Agda's datatype creation facilities allow us to define those datatypes in such a way that they behave as we expect.\n",
"\n",
"### True: `⊤`\n",
"\n",
"The type `⊤` has precisely one inhabitant, called `tt` (its only constructor).\n",
"\n",
"````\n",
"data ⊤ : Set where\n",
" tt : ⊤\n",
"````\n",
"\n",
"The ⊤-introduction rule says that we can prove that anything implies `⊤`.\n",
"\n",
"````\n",
"A→⊤ : {A : Set} → A → ⊤\n",
"A→⊤ _ = tt\n",
"````\n",
"\n",
"There is no ⊤-elimination rule.\n",
"\n",
"### False: `⊥`\n",
"\n",
"The type `⊥` has dual property to `⊤`.\n",
"The type `⊥` has no inhabitants at all, and thus we do not provide any constructor in its definition.\n",
"\n",
"````\n",
"data ⊥ : Set where\n",
"````\n",
"\n",
"The ⊥-elimination rule says that anything can be proved from `⊥`.\n",
"The absurd pattern `()` below is how we tell Agda that there cannot be any argument to `⊥-elim`, and thus it says that no defining equation is needed.\n",
"\n",
"````\n",
"⊥-elim : {A : Set} → ⊥ → A\n",
"⊥-elim ()\n",
"````\n",
"\n",
"There is no ⊥-introducion rule.\n",
"This makes the world a better place (why?)."
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/neg.agda",
"holes": [],
"moduleName": "code.neg",
"preambleLength": 0
},
"source": [
"## Negation\n",
"\n",
"````\n",
"module code.neg where\n",
"open import code.true-false public\n",
"````\n",
"\n",
"Negation is not a primitive in intuitionistic logic.\n",
"In intuitionistic logic $\\neg A$ means that, if we had a proof of $A$, then we could derive a contradiction $\\bot$:\n",
"$$ \\neg A \\;\\equiv\\; A \\to \\bot.$$\n",
"And this is how negation is defined in Agda.\n",
"\n",
"````\n",
"¬_ : Set → Set\n",
"¬ A = A → ⊥\n",
"````\n",
"\n",
"Thus, `¬ A` is a shorthand for (i.e., evaluates to) `A → ⊥`.\n",
"Notice that for the first time we are defining a function that maps types to types, i.e., a so called *type-level function*.\n",
"This is made possible by the fact that in a dependently typed language\n",
"types are first-class citizens and can be manipulated as any other data.\n",
"\n",
"We give negation higher priority than `∧` and `∨`,\n",
"so we can just write `¬ A ∧ B` instead of `(¬ A) ∧ B.\n",
"\n",
"````\n",
"infix 3 ¬_ \n",
"````"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise** (`¬¬`)\n",
"\n",
"The logic of Agda is intuitionistic. In particular, in Agda the following double negation law does *not* hold:\n",
"$$ A \\leftrightarrow \\neg \\neg A. $$\n",
"Which one of the two directions holds in intuitionistic logic?\n",
"- Formalise this and prove it in Agda.\n",
"- Does the proof (i.e., program) resemble something we have already seen?\n",
"\n",
"*Hint:* The type $\\neg \\neg A$ expands to\n",
"$$(A \\to \\bot) \\to \\bot.$$"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
6,
6
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex02.agda",
"holes": [
6,
6
],
"moduleName": "code.lab01.ex02",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex02 where\n",
"open import code.neg\n",
"\n",
"-- recall that ¬ ¬ A = (A → ⊥) → ⊥\n",
"\n",
"¬¬-intro : {A : Set} → A → ¬ ¬ A\n",
"¬¬-intro x f = ?\n",
"\n",
"-- the occurrence of \"?\" above is called a hole;\n",
"-- Agda will compile and remind us that there are open goals corresponding to holes to be solved"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise** (`¬ B → ¬ A`)\n",
"\n",
"The *contrapositive* of an implication $A \\to B$ is $\\neg B \\to \\neg A$.\n",
"In classical logic an implication and its contrapositive are logically equivalent, i.e., the following is a tautology:\n",
"$$(A \\to B) \\leftrightarrow (\\neg B \\to \\neg A).$$\n",
"Use Agda to prove which, if any, of the two directions above holds in intuitionistic logic."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
4,
4,
5,
5
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex03.agda",
"holes": [
4,
4,
5,
5
],
"moduleName": "code.lab01.ex03",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex03 where\n",
"open import code.neg\n",
"\n",
"-- your solution here\n",
"contrapositive : ?\n",
"contrapositive = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise** (De Morgan laws)\n",
"\n",
"Are the following laws valid in intuitionistic logic?\n",
"If so, write a proof in Agda.\n",
"\\begin{align}\n",
" (1) \\qquad \\neg (A \\vee B) \\leftrightarrow \\neg A \\wedge \\neg B. \\\\\n",
" (2) \\qquad \\neg A \\vee \\neg B \\to \\neg (A \\wedge B). \\\\\n",
" (3) \\qquad \\neg (A \\wedge B) \\to \\neg A \\vee \\neg B.\n",
"\\end{align}"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
6,
6,
9,
9,
12,
12,
15,
15
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex07.agda",
"holes": [
6,
6,
9,
9,
12,
12,
15,
15
],
"moduleName": "code.lab01.ex07",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex07 where\n",
"open import code.and\n",
"open import code.or\n",
"open import code.neg\n",
"\n",
"de_morgan1-1 : {A B : Set} → ¬ (A ∨ B) → ¬ A ∧ ¬ B\n",
"de_morgan1-1 = ?\n",
"\n",
"de_morgan1-2 : {A B : Set} → ¬ A ∧ ¬ B → ¬ (A ∨ B)\n",
"de_morgan1-2 = ?\n",
"\n",
"de_morgan2 : {A B : Set} → ¬ A ∨ ¬ B → ¬ (A ∧ B)\n",
"de_morgan2 = ?\n",
"\n",
"de_morgan3 : {A B : Set} → ¬ (A ∧ B) → ¬ A ∨ ¬ B\n",
"de_morgan3 = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"### **Exercise** (`¬ A ∨ B`)\n",
"\n",
"\n",
"\n",
"In classical logic, $A \\to B$ is defined to be $\\neg A \\vee B$.\n",
"Which of the following two directions hold in intuitionistic logic? Prove it in Agda.\n",
"$$(A \\to B) \\leftrightarrow (\\neg A \\vee B).$$\n",
"\n",
""
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex07.agda",
"holes": [],
"moduleName": "code.lab01.ex07",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex07 where\n",
"open import code.true-false\n",
"open import code.neg\n",
"open import code.or\n",
"\n",
"-- your solution here"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"# Challenges"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/conn.agda",
"holes": [],
"moduleName": "code.conn",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.conn where\n",
"open import code.or public\n",
"open import code.neg public \n",
"open import code.and public \n",
"open import code.true-false public"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"## **Exercise** (Triple negation)\n",
"\n",
"While $\\neg \\neg A \\to A$ does not hold in intuitionistic logic, prove that the following *triple negation* law holds\n",
"\n",
"$$\\neg \\neg \\neg A \\to \\neg A.$$\n",
"\n",
"*Hint:* Expand the definition of \"$\\neg$\". You should get a function of two arguments and output $\\bot$."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
4,
4
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/ex03.agda",
"holes": [
4,
4
],
"moduleName": "code.lab01.ex03",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.ex03 where\n",
"open import code.conn\n",
"\n",
"¬¬¬-rule : {A : Set} → ¬ ¬ ¬ A → ¬ A\n",
"¬¬¬-rule = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"## **Exercise** (Irrefutability)\n",
"\n",
"\n",
"\n",
"Show that the following classical tautologies $P$ are intuitionistically *irrefutable*, in the sense that $\\neg \\neg P$ is an intuitionistic tautology:\n",
"\n",
"1. Law of excluded middle: $\\neg \\neg (A \\vee \\neg A)$.\n",
" *Hint: Expand the definition of $\\neg$. You will need: `left`, `right`, and $\\lambda$-abstraction.*\n",
"2. Implication as disjunction: $\\neg \\neg ((A \\to B) \\to \\neg A \\vee B)$.\n",
"3. De Morgan: $\\neg \\neg (\\neg (A \\wedge B) \\to \\neg A \\vee \\neg B)$."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
4,
4,
5,
5,
7,
7,
8,
8,
10,
10,
11,
11
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/irref.agda",
"holes": [
4,
4,
5,
5,
7,
7,
8,
8,
10,
10,
11,
11
],
"moduleName": "code.lab01.irref",
"preambleLength": 0
},
"outputs": [],
"source": [
"{-# OPTIONS --allow-unsolved-metas #-}\n",
"module code.lab01.irref where\n",
"open import code.conn\n",
"\n",
"excluded-middle-irref : ?\n",
"excluded-middle-irref = ?\n",
"\n",
"impl-irref : ?\n",
"impl-irref = ?\n",
"\n",
"deMorgan-irref : ?\n",
"deMorgan-irref = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"## **Exercise** (Weak Peirce's law)\n",
"\n",
"Prove the following weakening of Peirce's law:\n",
"$$((((A \\to B) \\to A) \\to A) \\to B) \\to B.$$"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
3,
3
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/weak-peirce.agda",
"holes": [
3,
3
],
"moduleName": "code.lab01.weak-peirce",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.weak-peirce where\n",
"\n",
"wp : {A B : Set} → ((((A → B) → A) → A) → B) → B\n",
"wp = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": []
},
"source": [
"## **Exercise**\n",
"\n",
"In the previous exercises we have seen that the following principles are not intuitionistic tautologies:\n",
"1. Law of excluded middle: $A \\vee \\neg A$.\n",
"2. Elimination of double negation: $\\neg \\neg A \\to A$.\n",
"3. Implication as disjunction: $(A \\to B) \\to \\neg A \\vee B$.\n",
"4. The Negated De Morgan's law: $\\neg (\\neg A \\wedge \\neg B) \\to A \\vee B$.\n",
"5. Peirce's Law: $((A \\to B) \\to A) \\to A$.\n",
"\n",
"Show that all principles above are logically equivalent in intuitionistic logic.\n",
"Each propositional variable $A, B$ is universally quantified in each principle.\n",
"\n",
"*Hint:* Prove the following sequence of implications:\n",
"- $1 \\to 2$.\n",
"- $2 \\to 3$: Use irrefutability of $(A → B) \\to \\neg A \\vee B$, proved earlier:\n",
"$ \\neg \\neg ((A \\to B) \\to \\neg A \\vee B).$\n",
"- $3 \\to 1$.\n",
"- $1 \\to 4$: Use the excluded middle for $A$ and for $B$.\n",
"- $4 \\to 1$: Use $\\neg (\\neg A \\wedge \\neg B) \\to A \\vee B$ with $B \\equiv \\neg A$.\n",
"- $1 \\to 5$.\n",
"- $5 \\to 1$: Use Peirce's law $((A' \\to B') \\to A') \\to A'$ with\n",
"$A' \\equiv A \\vee \\neg A$ and $B' \\equiv \\bot.$"
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
4,
4,
5,
5,
7,
7,
8,
8,
10,
10,
11,
11,
13,
13,
14,
14,
16,
16,
17,
17,
19,
19,
20,
20,
22,
22,
23,
23
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/LEM-eq.agda",
"holes": [
4,
4,
5,
5,
7,
7,
8,
8,
10,
10,
11,
11,
13,
13,
14,
14,
16,
16,
17,
17,
19,
19,
20,
20,
22,
22,
23,
23
],
"moduleName": "code.lab01.LEM-eq",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.LEM-eq where\n",
"open import code.conn public\n",
"open import code.lab01.irref public\n",
"\n",
"1→2 : ?\n",
"1→2 = ?\n",
"\n",
"2→3 : ?\n",
"2→3 = ?\n",
"\n",
"3→1 : ?\n",
"3→1 = ?\n",
"\n",
"1→4 : ?\n",
"1→4 = ?\n",
"\n",
"4→1 : ?\n",
"4→1 = ?\n",
"\n",
"1→5 : ?\n",
"1→5 = ?\n",
"\n",
"5→1 : ?\n",
"5→1 = ?"
]
},
{
"cell_type": "markdown",
"metadata": {
"code_hole_highlighter": [],
"codehighlighter": [],
"hide_input": false
},
"source": [
"## **Exercise**\n",
"\n",
"Show that the following two principles are intuitionistically equivalent:\n",
"1. De Morgan's Law: $\\neg (A \\wedge B) \\to \\neg A \\vee \\neg B$.\n",
"2. The *weak principle of excluded middle*: $\\neg A \\vee \\neg \\neg A$.\n",
"This is interesting, because the weak principle of excluded middle is strictly weaker than the principle of excluded middle, but it is still not an intuitonistic tautology."
]
},
{
"cell_type": "code",
"execution_count": null,
"metadata": {
"code_hole_highlighter": [
2,
2,
3,
3,
5,
5,
6,
6
],
"codehighlighter": [],
"fileName": "/Users/lorenzo/Dropbox/workspace/teaching/2019-2020/LDI (logika dla informatyków)/labs/agda/code/lab01/weak-LEM.agda",
"holes": [
2,
2,
3,
3,
5,
5,
6,
6
],
"moduleName": "code.lab01.weak-LEM",
"preambleLength": 0
},
"outputs": [],
"source": [
"module code.lab01.weak-LEM where\n",
"\n",
"1→2 : ?\n",
"1→2 = ?\n",
"\n",
"2→1 : ?\n",
"2→1 = ?"
]
}
],
"metadata": {
"kernelspec": {
"display_name": "agda",
"language": "agda",
"name": "agda"
},
"language_info": {
"file_extension": ".agda",
"mimetype": "text/agda",
"name": "agda"
},
"latex_envs": {
"LaTeX_envs_menu_present": true,
"autoclose": false,
"autocomplete": true,
"bibliofile": "biblio.bib",
"cite_by": "apalike",
"current_citInitial": 1,
"eqLabelWithNumbers": true,
"eqNumInitial": 1,
"hotkeys": {
"equation": "Ctrl-E",
"itemize": "Ctrl-I"
},
"labels_anchors": false,
"latex_user_defs": false,
"report_style_numbering": false,
"user_envs_cfg": false
},
"nbTranslate": {
"displayLangs": [
"*"
],
"hotkey": "alt-t",
"langInMainMenu": true,
"sourceLang": "en",
"targetLang": "fr",
"useGoogleTranslate": true
},
"toc": {
"base_numbering": 1,
"nav_menu": {},
"number_sections": true,
"sideBar": true,
"skip_h1_title": false,
"title_cell": "Table of Contents",
"title_sidebar": "Contents",
"toc_cell": false,
"toc_position": {
"height": "calc(100% - 180px)",
"left": "10px",
"top": "150px",
"width": "315px"
},
"toc_section_display": true,
"toc_window_display": true
}
},
"nbformat": 4,
"nbformat_minor": 2
}