title | permalink |
---|---|
Assignment2: TSPL Assignment 2 |
/TSPL/2023/Assignment2/ |
module Assignment2 where
You must do all the exercises labelled "(recommended)".
Exercises labelled "(stretch)" are there to provide an extra challenge. You don't need to do all of these, but should attempt at least a few.
Exercises labelled "(practice)" are included for those who want extra practice.
Submit your homework using Gradescope. Go to the course page under Learn.
Select Assessment
, then select Assignment Submission
.
Please ensure your files execute correctly under Agda!
Please remember the University requirement as regards all assessed work. Details about this can be found at:
https://web.inf.ed.ac.uk/infweb/admin/policies/academic-misconduct
Furthermore, you are required to take reasonable measures to protect your assessed work from unauthorised access. For example, if you put any such work on a public repository then you must set access permissions appropriately (generally permitting access only to yourself, or your group in the case of group practicals).
module Connectives where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ)
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; _≲_; extensionality; _⇔_)
open plfa.part1.Isomorphism.≃-Reasoning
open import plfa.part1.Connectives
hiding (⊎-weak-×; ⊎×-implies-×⊎)
Show that A ⇔ B
as defined earlier
is isomorphic to (A → B) × (B → A)
.
-- Your code goes here
Show sum is commutative up to isomorphism.
-- Your code goes here
Show sum is associative up to isomorphism.
-- Your code goes here
Show empty is the left identity of sums up to isomorphism.
-- Your code goes here
Show empty is the right identity of sums up to isomorphism.
-- Your code goes here
Show that the following property holds:
postulate
⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)
This is called a weak distributive law. Give the corresponding distributive law, and explain how it relates to the weak version.
-- Your code goes here
Show that a disjunct of conjuncts implies a conjunct of disjuncts:
postulate
⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)
Does the converse hold? If so, prove; if not, give a counterexample.
-- Your code goes here
module Negation where
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import plfa.part1.Isomorphism using (_≃_; extensionality)
open import plfa.part1.Connectives
open import plfa.part1.Negation hiding (Stable)
Using negation, show that
strict inequality
is irreflexive, that is, n < n
holds for no n
.
-- Your code goes here
Show that strict inequality satisfies
trichotomy,
that is, for any naturals m
and n
exactly one of the following holds:
m < n
m ≡ n
m > n
Here "exactly one" means that not only one of the three must hold, but that when one holds the negation of the other two must also hold.
-- Your code goes here
Show that conjunction, disjunction, and negation are related by a version of De Morgan's Law.
¬ (A ⊎ B) ≃ (¬ A) × (¬ B)
This result is an easy consequence of something we've proved previously.
-- Your code goes here
Do we also have the following?
¬ (A × B) ≃ (¬ A) ⊎ (¬ B)
If so, prove; if not, can you give a relation weaker than isomorphism that relates the two sides?
Consider the following principles:
- Excluded Middle:
A ⊎ ¬ A
, for allA
- Double Negation Elimination:
¬ ¬ A → A
, for allA
- Peirce's Law:
((A → B) → A) → A
, for allA
andB
. - Implication as disjunction:
(A → B) → ¬ A ⊎ B
, for allA
andB
. - De Morgan:
¬ (¬ A × ¬ B) → A ⊎ B
, for allA
andB
.
Show that each of these implies all the others.
-- Your code goes here
Say that a formula is stable if double negation elimination holds for it:
Stable : Set → Set
Stable A = ¬ ¬ A → A
Show that any negated formula is stable, and that the conjunction of two stable formulas is stable.
-- Your code goes here
module Quantifiers where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Relation.Nullary using (¬_)
open import Function using (_∘_)
open import plfa.part1.Isomorphism using (_≃_; extensionality; ∀-extensionality)
open import plfa.part1.Connectives
hiding (Tri)
open import plfa.part1.Quantifiers
hiding (∀-distrib-×; ⊎∀-implies-∀⊎; ∃-distrib-⊎; ∃×-implies-×∃; ∃¬-implies-¬∀; Tri)
Show that universals distribute over conjunction:
postulate
∀-distrib-× : ∀ {A : Set} {B C : A → Set} →
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
Compare this with the result (→-distrib-×
) in
Chapter Connectives.
Hint: you will need to use ∀-extensionality
.
Show that a disjunction of universals implies a universal of disjunctions:
postulate
⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
Does the converse hold? If so, prove; if not, explain why.
Consider the following type.
data Tri : Set where
aa : Tri
bb : Tri
cc : Tri
Let B
be a type indexed by Tri
, that is B : Tri → Set
.
Show that ∀ (x : Tri) → B x
is isomorphic to B aa × B bb × B cc
.
Hint: you will need to use ∀-extensionality
.
Show that existentials distribute over disjunction:
postulate
∃-distrib-⊎ : ∀ {A : Set} {B C : A → Set} →
∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
Show that an existential of conjunctions implies a conjunction of existentials:
postulate
∃×-implies-×∃ : ∀ {A : Set} {B C : A → Set} →
∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
Does the converse hold? If so, prove; if not, explain why.
Let Tri
and B
be as in Exercise ∀-×
.
Show that ∃[ x ] B x
is isomorphic to B aa ⊎ B bb ⊎ B cc
.
How do the proofs become more difficult if we replace m * 2
and 1 + m * 2
by 2 * m
and 2 * m + 1
? Rewrite the proofs of ∃-even
and ∃-odd
when
restated in this way.
-- Your code goes here
Show that y ≤ z
holds if and only if there exists a x
such that
x + y ≡ z
.
-- Your code goes here
Show that existential of a negation implies negation of a universal:
postulate
∃¬-implies-¬∀ : ∀ {A : Set} {B : A → Set}
→ ∃[ x ] (¬ B x)
--------------
→ ¬ (∀ x → B x)
Does the converse hold? If so, prove; if not, explain why.
Recall that Exercises
Bin,
Bin-laws, and
Bin-predicates
define a datatype Bin
of bitstrings representing natural numbers,
and asks you to define the following functions and predicates:
to : ℕ → Bin
from : Bin → ℕ
Can : Bin → Set
And to establish the following properties:
from (to n) ≡ n
----------
Can (to n)
Can b
---------------
to (from b) ≡ b
Using the above, establish that there is an isomorphism between ℕ
and
∃[ b ] Can b
.
We recommend proving the following lemmas which show that, for a given
binary number b
, there is only one proof of One b
and similarly
for Can b
.
≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
≡Can : ∀ {b : Bin} (cb cb′ : Can b) → cb ≡ cb′
Many of the alternatives for proving to∘from
turn out to be tricky.
However, the proof can be straightforward if you use the following lemma,
which is a corollary of ≡Can
.
proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
-- Your code goes here
module Decidable where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)
open import Relation.Nullary.Negation using ()
renaming (contradiction to ¬¬-intro)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import plfa.part1.Relations using (_<_; z<s; s<s)
open import plfa.part1.Isomorphism using (_⇔_)
open import plfa.part1.Decidable
hiding (_<?_; _≡ℕ?_; ∧-×; ∨-⊎; not-¬; _iff_; _⇔-dec_; iff-⇔)
Analogous to the function above, define a function to decide strict inequality:
postulate
_<?_ : ∀ (m n : ℕ) → Dec (m < n)
-- Your code goes here
Define a function to decide whether two naturals are equal:
postulate
_≡ℕ?_ : ∀ (m n : ℕ) → Dec (m ≡ n)
-- Your code goes here
Show that erasure relates corresponding boolean and decidable operations:
postulate
∧-× : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∧ ⌊ y ⌋ ≡ ⌊ x ×-dec y ⌋
∨-⊎ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ ∨ ⌊ y ⌋ ≡ ⌊ x ⊎-dec y ⌋
not-¬ : ∀ {A : Set} (x : Dec A) → not ⌊ x ⌋ ≡ ⌊ ¬? x ⌋
Give analogues of the _⇔_
operation from
Chapter Isomorphism,
operation on booleans and decidables, and also show the corresponding erasure:
postulate
_iff_ : Bool → Bool → Bool
_⇔-dec_ : ∀ {A B : Set} → Dec A → Dec B → Dec (A ⇔ B)
iff-⇔ : ∀ {A B : Set} (x : Dec A) (y : Dec B) → ⌊ x ⌋ iff ⌊ y ⌋ ≡ ⌊ x ⇔-dec y ⌋
-- Your code goes here
Give analogues of True
, toWitness
, and fromWitness
which work
with negated properties. Call these False
, toWitnessFalse
, and
fromWitnessFalse
.
Recall that Exercises
Bin,
Bin-laws, and
Bin-predicates
define a datatype Bin
of bitstrings representing natural numbers,
and asks you to define the following predicates:
One : Bin → Set
Can : Bin → Set
Show that both of the above are decidable.
One? : ∀ (b : Bin) → Dec (One b)
Can? : ∀ (b : Bin) → Dec (Can b)