michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

update Lists, Decidable and reorganise files

Browse source
This commit is contained in:
wadler 2018-03-22 18:46:29 -03:00
parent b943785e6b
commit fb3592239d
7 changed files with 31 additions and 1211 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

817
src/Connectives-old.lagda
View file

@ -1,817 +0,0 @@
---
title : "Connectives: Conjunction, Disjunction, and Implication"
layout : page
permalink : /Connectives
---
This chapter introduces the basic logical connectives, by observing
a correspondence between connectives of logic and data types,
a principal known as *Propositions as Types*.
+ *conjunction* is *product*
+ *disjunction* is *sum*
+ *true* is *unit type*
+ *false* is *empty type*
+ *implication* is *function space*
## Imports
\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open Isomorphism.≃-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties.Simple using (+-suc)
open import Function using (_∘_)
\end{code}
We assume [extensionality][extensionality].
\begin{code}
postulate
extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
\end{code}
[extensionality]: Equality/index.html#extensionality
## Conjunction is product
Given two propositions `A` and `B`, the conjunction `A × B` holds
if both `A` holds and `B` holds. We formalise this idea by
declaring a suitable inductive type.
\begin{code}
data _×_ : Set → Set → Set where
_,_ : ∀ {A B : Set} → A → B → A × B
\end{code}
Evidence that `A × B` holds is of the form
`(M , N)`, where `M` is evidence that `A` holds and
`N` is evidence that `B` holds. By convention, we
parenthesise pairs, even though `M , N` is also
accepted by Agda.
Given evidence that `A × B` holds, we can conclude that either
`A` holds or `B` holds.
\begin{code}
proj₁ : ∀ {A B : Set} → A × B → A
proj₁ (x , y) = x
proj₂ : ∀ {A B : Set} → A × B → B
proj₂ (x , y) = y
\end{code}
If `L` is evidence that `A × B` holds, then `fst L` is evidence
that `A` holds, and `proj₂ L` is evidence that `B` holds.
Equivalently, we could also declare conjunction as a record type.
\begin{code}
record _×′_ (A B : Set) : Set where
field
proj₁′ : A
proj₂′ : B
open _×′_
\end{code}
Here record construction
record
{ proj₁′ = M
; proj₂′ = N
}
corresponds to the term
( M , N )
where `M` is a term of type `A` and `N` is a term of type `B`.
When `(_,_)` appears on the right-hand side of an equation we
refer to it as a *constructor*, and when it appears on the
left-hand side we refer to it as a *destructor*. We also refer
to `proj₁` and `proj₂` as destructors, since they play a similar role.
Other terminology refers to constructor as *introducing* a conjunction,
and to a destructor as *eliminating* a conjunction.
Indeed, `proj₁` and `proj₂` are sometimes given the names
`×-elim₁` and `×-elim₂`.
Applying each destructor and reassembling the results with the
constructor is the identity over products.
\begin{code}
η-× : ∀ {A B : Set} (w : A × B) → (proj₁ w , proj₂ w) ≡ w
η-× (x , y) = refl
\end{code}
The pattern matching on the left-hand side is essential, since
replacing `w` by `(x , y)` allows both sides of the equation to
simplify to the same term.
We set the precedence of conjunction so that it binds less
tightly than anything save disjunction, and of the pairing
operator so that it binds less tightly than any arithmetic
operator.
\begin{code}
infixr 2 _×_
infixr 4 _,_
\end{code}
Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)` and
`(m * n , p)` parses as `((m * n) , p)`.
Given two types `A` and `B`, we refer to `A x B` as the
*product* of `A` and `B`. In set theory, it is also sometimes
called the *cartesian product*, and in computing it corresponds
to a *record* type. Among other reasons for
calling it the product, note that if type `A` has `m`
distinct members, and type `B` has `n` distinct members,
then the type `A × B` has `m * n` distinct members.
For instance, consider a type `Bool` with two members, and
a type `Tri` with three members.
\begin{code}
data Bool : Set where
true : Bool
false : Bool
data Tri : Set where
aa : Tri
bb : Tri
cc : Tri
\end{code}
Then the type `Bool × Tri` has six members:
(true , aa) (true , bb) (true , cc)
(false , aa) (false , bb) (false , cc)
For example, the following function enumerates all
possible arguments of type `Bool × Tri`:
\begin{code}
×-count : Bool × Tri → ℕ
×-count (true , aa) = 1
×-count (true , bb) = 2
×-count (true , cc) = 3
×-count (false , aa) = 4
×-count (false , bb) = 5
×-count (false , cc) = 6
\end{code}
Product on types also shares a property with product on numbers in
that there is a sense in which it is commutative and associative. In
particular, product is commutative and associative *up to
isomorphism*.
For commutativity, the `to` function swaps a pair, taking `(x , y)` to
`(y , x)`, and the `from` function does the same (up to renaming).
Instantiating the patterns correctly in `from∘to` and `to∘from` is essential.
Replacing the definition of `from∘to` by `λ w → refl` will not work;
and similarly for `to∘from`, which does the same (up to renaming).
\begin{code}
×-comm : ∀ {A B : Set} → (A × B) ≃ (B × A)
×-comm =
record
{ to = λ{ (x , y) → (y , x)}
; from = λ{ (y , x) → (x , y)}
; from∘to = λ{ (x , y) → refl }
; to∘from = λ{ (y , x) → refl }
}
\end{code}
Being *commutative* is different from being *commutative up to
isomorphism*. Compare the two statements:
m * n ≡ n * m
A × B ≃ B × A
In the first case, we might have that `m` is `2` and `n` is `3`, and
both `m * n` and `n * m` are equal to `6`. In the second case, we
might have that `A` is `Bool` and `B` is `Tri`, and `Bool × Tri` is
*not* the same as `Tri × Bool`. But there is an isomorphism
between the two types. For
instance, `(true , aa)`, which is a member of the former, corresponds
to `(aa , true)`, which is a member of the latter.
For associativity, the `to` function reassociates two uses of pairing,
taking `((x , y) , z)` to `(x , (y , z))`, and the `from` function does
the inverse. Again, the evidence of left and right inverse requires
matching against a suitable pattern to enable simplification.
\begin{code}
×-assoc : ∀ {A B C : Set} → ((A × B) × C) ≃ (A × (B × C))
×-assoc =
record
{ to = λ{ ((x , y) , z) → (x , (y , z)) }
; from = λ{ (x , (y , z)) → ((x , y) , z) }
; from∘to = λ{ ((x , y) , z) → refl }
; to∘from = λ{ (x , (y , z)) → refl }
}
\end{code}
Being *associative* is not the same as being *associative
up to isomorphism*. Compare the two statements:
(m * n) * p ≡ m * (n * p)
(A × B) × C ≃ A × (B × C)
For example, the type `(ℕ × Bool) × Tri` is *not* the same as `ℕ ×
(Bool × Tri)`. But there is an isomorphism between the two types. For
instance `((1 , true) , aa)`, which is a member of the former,
corresponds to `(1 , (true , aa))`, which is a member of the latter.
## Truth is unit
Truth `⊤` always holds. We formalise this idea by
declaring a suitable inductive type.
\begin{code}
data ⊤ : Set where
tt : ⊤
\end{code}
Evidence that `⊤` holds is of the form `tt`.
Given evidence that `⊤` holds, there is nothing more of interest we
can conclude. Since truth always holds, knowing that it holds tells
us nothing new.
The nullary case of `η-×` is `η-⊤`, which asserts that any
term of type `⊤` must be equal to `tt`.
\begin{code}
η-⊤ : ∀ (w : ⊤) → tt ≡ w
η-⊤ tt = refl
\end{code}
The pattern matching on the left-hand side is essential. Replacing
`w` by `tt` allows both sides of the equation to simplify to the
same term.
We refer to `⊤` as the *unit* type. And, indeed,
type `⊤` has exactly once member, `tt`. For example, the following
function enumerates all possible arguments of type `⊤`:
\begin{code}
⊤-count : ⊤ → ℕ
⊤-count tt = 1
\end{code}
For numbers, one is the identity of multiplication. Correspondingly,
unit is the identity of product *up to isomorphism*. For left
identity, the `to` function takes `(tt , x)` to `x`, and the `from`
function does the inverse. The evidence of left inverse requires
matching against a suitable pattern to enable simplification.
\begin{code}
⊤-identityˡ : ∀ {A : Set} → (⊤ × A) ≃ A
⊤-identityˡ =
record
{ to = λ{ (tt , x) → x }
; from = λ{ x → (tt , x) }
; from∘to = λ{ (tt , x) → refl }
; to∘from = λ{ x → refl }
}
\end{code}
Having an *identity* is different from having an identity
*up to isomorphism*. Compare the two statements:
1 * m ≡ m
⊤ × A ≃ A
In the first case, we might have that `m` is `2`, and both
`1 * m` and `m` are equal to `2`. In the second
case, we might have that `A` is `Bool`, and `⊤ × Bool` is *not* the
same as `Bool`. But there is an isomorphism between the two types.
For instance, `(tt, true)`, which is a member of the former,
corresponds to `true`, which is a member of the latter.
Right identity follows from commutativity of product and left identity.
\begin{code}
⊤-identityʳ : ∀ {A : Set} → (A × ⊤) ≃ A
⊤-identityʳ {A} =
≃-begin
(A × ⊤)
≃⟨ ×-comm ⟩
(⊤ × A)
≃⟨ ⊤-identityˡ ⟩
A
≃-∎
\end{code}
Here we have used a chain of isomorphisms,
analogous to that used for equality.
## Disjunction is sum
Given two propositions `A` and `B`, the disjunction `A ⊎ B` holds
if either `A` holds or `B` holds. We formalise this idea by
declaring a suitable inductive type.
\begin{code}
data _⊎_ : Set → Set → Set where
inj₁ : ∀ {A B : Set} → A → A ⊎ B
inj₂ : ∀ {A B : Set} → B → A ⊎ B
\end{code}
Evidence that `A ⊎ B` holds is either of the form `inj₁ M`, where `M`
is evidence that `A` holds, or `inj₂ N`, where `N` is evidence that
`B` holds.
Given evidence that `A → C` and `B → C` both hold, then given
evidence that `A ⊎ B` holds we can conclude that `C` holds.
\begin{code}
⊎-elim : ∀ {A B C : Set} → (A → C) → (B → C) → (A ⊎ B → C)
⊎-elim f g (inj₁ x) = f x
⊎-elim f g (inj₂ y) = g y
\end{code}
Pattern matching against `inj₁` and `inj₂` is typical of how we exploit
evidence that a disjunction holds.
When `inj₁` and `inj₂` appear on the right-hand side of an equation we
refer to them as *constructors*, and when they appears on the
left-hand side we refer to them as *destructors*. We also refer
to `⊎-elim` as a destructor, since it plays a similar role.
Other terminology refers to constructors as *introducing* a disjunction,
and to a destructors as *eliminating* a disjunction.
Applying the destructor to each of the constructors is the identity.
\begin{code}
η-⊎ : ∀ {A B : Set} (w : A ⊎ B) → ⊎-elim inj₁ inj₂ w ≡ w
η-⊎ (inj₁ x) = refl
η-⊎ (inj₂ y) = refl
\end{code}
More generally, we can also throw in an arbitrary function from a disjunction.
\begin{code}
uniq-⊎ : ∀ {A B C : Set} (h : A ⊎ B → C) (w : A ⊎ B) →
⊎-elim (h ∘ inj₁) (h ∘ inj₂) w ≡ h w
uniq-⊎ h (inj₁ x) = refl
uniq-⊎ h (inj₂ y) = refl
\end{code}
The pattern matching on the left-hand side is essential. Replacing
`w` by `inj₁ x` allows both sides of the equation to simplify to the
same term, and similarly for `inj₂ y`.
We set the precedence of disjunction so that it binds less tightly
than any other declared operator.
\begin{code}
infix 1 _⊎_
\end{code}
Thus, `A × C ⊎ B × C` parses as `(A × C) ⊎ (B × C)`.
Given two types `A` and `B`, we refer to `A ⊎ B` as the
*sum* of `A` and `B`. In set theory, it is also sometimes
called the *disjoint union*, and in computing it corresponds
to a *variant record* type. Among other reasons for
calling it the sum, note that if type `A` has `m`
distinct members, and type `B` has `n` distinct members,
then the type `A ⊎ B` has `m + n` distinct members.
For instance, consider a type `Bool` with two members, and
a type `Tri` with three members, as defined earlier.
Then the type `Bool ⊎ Tri` has five
members:
(inj₁ true) (inj₂ aa)
(inj₁ false) (inj₂ bb)
(inj₂ cc)
For example, the following function enumerates all
possible arguments of type `Bool ⊎ Tri`:
\begin{code}
⊎-count : Bool ⊎ Tri → ℕ
⊎-count (inj₁ true) = 1
⊎-count (inj₁ false) = 2
⊎-count (inj₂ aa) = 3
⊎-count (inj₂ bb) = 4
⊎-count (inj₂ cc) = 5
\end{code}
Sum on types also shares a property with sum on numbers in that it is
commutative and associative *up to isomorphism*.
For commutativity, the `to` function swaps the two constructors,
taking `inj₁ x` to `inj₂ x`, and `inj₂ y` to `inj₁ y`; and the `from`
function does the same (up to renaming). Replacing the definition of
`from∘to` by `λ w → refl` will not work; and similarly for `to∘from`, which
does the same (up to renaming).
\begin{code}
⊎-comm : ∀ {A B : Set} → (A ⊎ B) ≃ (B ⊎ A)
⊎-comm = record
{ to = λ{ (inj₁ x) → (inj₂ x)
; (inj₂ y) → (inj₁ y)
}
; from = λ{ (inj₁ y) → (inj₂ y)
; (inj₂ x) → (inj₁ x)
}
; from∘to = λ{ (inj₁ x) → refl
; (inj₂ y) → refl
}
; to∘from = λ{ (inj₁ y) → refl
; (inj₂ x) → refl
}
}
\end{code}
Being *commutative* is different from being *commutative up to
isomorphism*. Compare the two statements:
m + n ≡ n + m
A ⊎ B ≃ B ⊎ A
In the first case, we might have that `m` is `2` and `n` is `3`, and
both `m + n` and `n + m` are equal to `5`. In the second case, we
might have that `A` is `Bool` and `B` is `Tri`, and `Bool ⊎ Tri` is
*not* the same as `Tri ⊎ Bool`. But there is an isomorphism between
the two types. For instance, `inj₁ true`, which is a member of the
former, corresponds to `inj₂ true`, which is a member of the latter.
For associativity, the `to` function reassociates, and the `from` function does
the inverse. Again, the evidence of left and right inverse requires
matching against a suitable pattern to enable simplification.
\begin{code}
⊎-assoc : ∀ {A B C : Set} → ((A ⊎ B) ⊎ C) ≃ (A ⊎ (B ⊎ C))
⊎-assoc = record
{ to = λ{ (inj₁ (inj₁ x)) → (inj₁ x)
; (inj₁ (inj₂ y)) → (inj₂ (inj₁ y))
; (inj₂ z) → (inj₂ (inj₂ z))
}
; from = λ{ (inj₁ x) → (inj₁ (inj₁ x))
; (inj₂ (inj₁ y)) → (inj₁ (inj₂ y))
; (inj₂ (inj₂ z)) → (inj₂ z)
}
; from∘to = λ{ (inj₁ (inj₁ x)) → refl
; (inj₁ (inj₂ y)) → refl
; (inj₂ z) → refl
}
; to∘from = λ{ (inj₁ x) → refl
; (inj₂ (inj₁ y)) → refl
; (inj₂ (inj₂ z)) → refl
}
}
\end{code}
Again, being *associative* is not the same as being *associative
up to isomorphism*. For example, the type `(ℕ + Bool) + Tri`
is *not* the same as `ℕ + (Bool + Tri)`. But there is an
isomorphism between the two types. For instance `inj₂ (inj₁ true)`,
which is a member of the former, corresponds to `inj₁ (inj₂ true)`,
which is a member of the latter.
## False is empty
False `⊥` never holds. We formalise this idea by declaring
a suitable inductive type.
\begin{code}
data ⊥ : Set where
-- no clauses!
\end{code}
There is no possible evidence that `⊥` holds.
Given evidence that `⊥` holds, we might conclude anything! Since
false never holds, knowing that it holds tells us we are in a
paradoxical situation. This is a basic principle of logic,
known in medieval times by the latin phrase *ex falso*,
and known to children through phrases such as
"if pigs had wings, then I'd be the Queen of Sheba".
We formalise it as follows.
\begin{code}
⊥-elim : ∀ {A : Set} → ⊥ → A
⊥-elim ()
\end{code}
This is our first use of the *absurd pattern* `()`.
Here since `⊥` is a type with no members, we indicate that it is
*never* possible to match against a value of this type by using
the pattern `()`.
The nullary case of `uniq-⊎` is `uniq-⊥`, which asserts that `⊥-elim`
is equal to any arbitrary function from `⊥`.
\begin{code}
uniq-⊥ : ∀ {C : Set} (h : ⊥ → C) (w : ⊥) → ⊥-elim w ≡ h w
uniq-⊥ h ()
\end{code}
The pattern matching on the left-hand side is essential. Using
the absurd pattern asserts there are no possible values for `w`,
so the equation holds trivially.
We refer to `⊥` as *empty* type. And, indeed,
type `⊥` has no members. For example, the following function
enumerates all possible arguments of type `⊥`:
\begin{code}
⊥-count : ⊥ → ℕ
⊥-count ()
\end{code}
Here again the absurd pattern `()` indicates that no value can match
type `⊥`.
For numbers, zero is the identity of addition. Correspondingly,
empty is the identity of sums *up to isomorphism*.
For left identity, the `to` function observes that `inj₁ ()` can never arise,
and takes `inj₂ x` to `x`, and the `from` function
does the inverse. The evidence of left inverse requires matching against
a suitable pattern to enable simplification.
\begin{code}
⊥-identityˡ : ∀ {A : Set} → (⊥ ⊎ A) ≃ A
⊥-identityˡ =
record
{ to = λ{ (inj₁ ())
; (inj₂ x) → x
}
; from = λ{ x → inj₂ x
}
; from∘to = λ{ (inj₁ ())
; (inj₂ x) → refl
}
; to∘from = λ{ x → refl
}
}
\end{code}
Having an *identity* is different from having an identity
*up to isomorphism*. Compare the two statements:
0 + m ≡ m
⊥ ⊎ A ≃ A
In the first case, we might have that `m` is `2`, and both `0 + m` and
`m` are equal to `2`. In the second case, we might have that `A` is
`Bool`, and `⊥ ⊎ Bool` is *not* the same as `Bool`. But there is an
isomorphism between the two types. For instance, `inj₂ true`, which is
a member of the former, corresponds to `true`, which is a member of
the latter.
Right identity follows from commutativity of sum and left identity.
\begin{code}
⊥-identityʳ : ∀ {A : Set} → (A ⊎ ⊥) ≃ A
⊥-identityʳ {A} =
≃-begin
(A ⊎ ⊥)
≃⟨ ⊎-comm ⟩
(⊥ ⊎ A)
≃⟨ ⊥-identityˡ ⟩
A
≃-∎
\end{code}
## Implication is function {#implication}
Given two propositions `A` and `B`, the implication `A → B` holds if
whenever `A` holds then `B` must also hold. We formalise implication using
the function type, which has appeared throughout this book.
Evidence that `A → B` holds is of the form
λ (x : A) → N x
where `N x` is a term of type `B` containing as a free variable `x` of type `A`.
Given a term `L` providing evidence that `A → B` holds, and a term `M`
providing evidence that `A` holds, the term `L M` provides evidence that
`B` holds. In other words, evidence that `A → B` holds is a function that
converts evidence that `A` holds into evidence that `B` holds.
Put another way, if we know that `A → B` and `A` both hold,
then we may conclude that `B` holds.
\begin{code}
→-elim : ∀ {A B : Set} → (A → B) → A → B
→-elim L M = L M
\end{code}
In medieval times, this rule was known by the name *modus ponens*.
It corresponds to function application.
Defining a function, with an named definition or a lambda expression,
is referred to as *introducing* a function,
while applying a function is referred to as *eliminating* the function.
Elimination followed by introduction is the identity.
\begin{code}
η-→ : ∀ {A B : Set} (f : A → B) → (λ (x : A) → f x) ≡ f
η-→ {A} {B} f = extensionality η-helper
where
η-helper : (x : A) → (λ (x : A) → f x) x ≡ f x
η-helper x = refl
\end{code}
The proof depends on extensionality.
<!--
If we introduce an implication and then immediately eliminate it, we can
always simplify the resulting term. Thus
λ{ x → N } M
simplifies to `N[x := M]`, where `N[x := M]` stands for the term `N` with each
free occurrence of `x` replaced by `M`.
-->
Implication binds less tightly than any other operator. Thus, `A ⊎ B →
B ⊎ A` parses as `(A ⊎ B) → (B ⊎ A)`.
Given two types `A` and `B`, we refer to `A → B` as the *function*
space from `A` to `B`. It is also sometimes called the *exponential*,
with `B` raised to the `A` power. Among other reasons for calling
it the exponential, note that if type `A` has `m` distinct
members, and type `B` has `n` distinct members, then the type
`A → B` has `n ^ m` distinct members. For instance, consider a
type `Bool` with two members and a type `Tri` with three members,
as defined earlier. The the type `Bool → Tri` has nine (that is,
three squared) members:
λ{true → aa; false → aa} λ{true → aa; false → bb} λ{true → aa; false → cc}
λ{true → bb; false → aa} λ{true → bb; false → bb} λ{true → bb; false → cc}
λ{true → cc; false → aa} λ{true → cc; false → bb} λ{true → cc; false → cc}
For example, the following function enumerates all possible
arguments of the type `Bool → Tri`:
\begin{code}
→-count : (Bool → Tri) → ℕ
→-count f with f true | f false
... | aa | aa = 1
... | aa | bb = 2
... | aa | cc = 3
... | bb | aa = 4
... | bb | bb = 5
... | bb | cc = 6
... | cc | aa = 7
... | cc | bb = 8
... | cc | cc = 9
\end{code}
Exponential on types also share a property with exponential on
numbers in that many of the standard identities for numbers carry
over to the types.
Corresponding to the law
(p ^ n) ^ m = p ^ (n * m)
we have the isomorphism
A → (B → C) ≃ (A × B) → C
Both types can be viewed as functions that given evidence that `A` holds
and evidence that `B` holds can return evidence that `C` holds.
This isomorphism sometimes goes by the name *currying*.
The proof of the right inverse requires extensionality.
\begin{code}
currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)
currying =
record
{ to = λ{ f → λ{ (x , y) → f x y }}
; from = λ{ g → λ{ x → λ{ y → g (x , y) }}}
; from∘to = λ{ f → refl }
; to∘from = λ{ g → extensionality λ{ (x , y) → refl }}
}
\end{code}
Currying tells us that instead of a function that takes a pair of arguments,
we can have a function that takes the first argument and returns a function that
expects the second argument. Thus, for instance, our way of writing addition:
_+_ : ℕ → ℕ → ℕ
is isomorphic to a function that accepts a pair of arguments:
_+′_ : (ℕ × ℕ) → ℕ
Agda is optimised for currying, so `2 + 3` abbreviates `_+_ 2 3`.
In a language optimised for pairing, we would take `2 +′ 3` as
an abbreviation for `_+′_ (2 , 3)`.
Corresponding to the law
p ^ (n + m) = (p ^ n) * (p ^ m)
we have the isomorphism
(A ⊎ B) → C ≃ (A → C) × (B → C)
That is, the assertion that if either `A` holds or `B` holds then `C` holds
is the same as the assertion that if `A` holds then `C` holds and if
`B` holds then `C` holds. The proof of the left inverse requires extensionality.
\begin{code}
→-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))
→-distrib-⊎ =
record
{ to = λ{ f → ( (λ{ x → f (inj₁ x) }) , (λ{ y → f (inj₂ y) }) ) }
; from = λ{ (g , h) → λ{ (inj₁ x) → g x ; (inj₂ y) → h y } }
; from∘to = λ{ f → extensionality λ{ (inj₁ x) → refl ; (inj₂ y) → refl } }
; to∘from = λ{ (g , h) → refl }
}
\end{code}
Corresponding to the law
(p * n) ^ m = (p ^ m) * (n ^ m)
we have the isomorphism
A → B × C ≃ (A → B) × (A → C)
That is, the assertion that if either `A` holds then `B` holds and `C` holds
is the same as the assertion that if `A` holds then `B` holds and if
`A` holds then `C` holds. The proof of left inverse requires both extensionality
and the rule `η-×` for products.
\begin{code}
→-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)
→-distrib-× =
record
{ to = λ{ f → ( (λ{ x → proj₁ (f x) }) , (λ{ y → proj₂ (f y)}) ) }
; from = λ{ (g , h) → λ{ x → (g x , h x) } }
; from∘to = λ{ f → extensionality λ{ x → η-× (f x) } }
; to∘from = λ{ (g , h) → refl }
}
\end{code}
## Distribution
Products distributes over sum, up to isomorphism. The code to validate
this fact is similar in structure to our previous results.
\begin{code}
×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ =
record
{ to = λ{ ((inj₁ x) , z) → (inj₁ (x , z))
; ((inj₂ y) , z) → (inj₂ (y , z))
}
; from = λ{ (inj₁ (x , z)) → ((inj₁ x) , z)
; (inj₂ (y , z)) → ((inj₂ y) , z)
}
; from∘to = λ{ ((inj₁ x) , z) → refl
; ((inj₂ y) , z) → refl
}
; to∘from = λ{ (inj₁ (x , z)) → refl
; (inj₂ (y , z)) → refl
}
}
\end{code}
Sums do not distribute over products up to isomorphism, but it is an embedding.
\begin{code}
⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)
⊎-distrib-× =
record
{ to = λ{ (inj₁ (x , y)) → (inj₁ x , inj₁ y)
; (inj₂ z) → (inj₂ z , inj₂ z)
}
; from = λ{ (inj₁ x , inj₁ y) → (inj₁ (x , y))
; (inj₁ x , inj₂ z) → (inj₂ z)
; (inj₂ z , _ ) → (inj₂ z)
}
; from∘to = λ{ (inj₁ (x , y)) → refl
; (inj₂ z) → refl
}
}
\end{code}
Note that there is a choice in how we write the `from` function.
As given, it takes `(inj₂ z , inj₂ z′)` to `(inj₂ z)`, but it is
easy to write a variant that instead returns `(inj₂ z′)`. We have
an embedding rather than an isomorphism because the
`from` function must discard either `z` or `z′` in this case.
In the usual approach to logic, both of the distribution laws
are given as equivalences, where each side implies the other:
A & (B ∨ C) ⇔ (A & B) ∨ (A & C)
A ∨ (B & C) ⇔ (A ∨ B) & (A ∨ C)
But when we consider the two laws in terms of evidence, where `_&_`
corresponds to `_×_` and `_∨_` corresponds to `_⊎_`, then the first
gives rise to an isomorphism, while the second only gives rise to an
embedding, revealing a sense in which one of these laws is "more
true" than the other.
### Exercise (`×⊎-implies-⊎×`)
Show that a conjunct of disjuncts implies a disjunct of conjuncts.
\begin{code}
×⊎-Implies-⊎× = ∀ {A B C D : Set} → (A ⊎ B) × (C ⊎ D) → (A × C) ⊎ (B × D)
\end{code}
Does the converse hold? If so, prove; if not, explain why.
### Exercise (`⇔-refl`, `⇔-sym`, `⇔-trans`)
Define equivalence of propositions (also known as "if and only if") as follows.
\begin{code}
record _⇔_ (A B : Set) : Set where
field
to : A → B
from : B → A
\end{code}
Show that equivalence is reflexive, symmetric, and transitive.
### Exercise (`⇔-iso`)
Show that `A ⇔ B` is isomorphic to `(A → B) × (B → A)`.
## Standard library
Definitions similar to those in this chapter can be found in the standard library.
\begin{code}
import Data.Product using (_×_; _,_; proj₁; proj₂)
import Data.Unit using (⊤; tt)
import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_] to ⊎-elim)
import Data.Empty using (⊥; ⊥-elim)
\end{code}
## Unicode
This chapter uses the following unicode.
× U+00D7 MULTIPLICATION SIGN (\x)
⊎ U+228E MULTISET UNION (\u+)
⊤ U+22A4 DOWN TACK (\top)
⊥ U+22A5 UP TACK (\bot)
η U+03B7 GREEK SMALL LETTER ETA (\eta)
₁ U+2081 SUBSCRIPT ONE (\_1)
₂ U+2082 SUBSCRIPT TWO (\_2)
⇔ U+21D4 LEFT RIGHT DOUBLE ARROW (\<=>)

394
src/Quantifiers-old.lagda
View file

@ -1,394 +0,0 @@
---
title : "Quantifiers: Universals and Existentials"
layout : page
permalink : /Quantifiers
---
This chapter introduces universal and existential quantification.
## Imports
\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open Isomorphism.≃-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties.Simple using (+-suc)
open import Relation.Nullary using (¬_)
open import Function using (_∘_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
\end{code}
We assume [extensionality][extensionality].
\begin{code}
postulate
extensionality : ∀ {A B : Set} {f g : A → B} → (∀ (x : A) → f x ≡ g x) → f ≡ g
\end{code}
[extensionality]: Equality/index.html#extensionality
## Universals
Given a variable `x` of type `A` and a proposition `B x` which
contains `x` as a free variable, the universally quantified
proposition `∀ (x : A) → B x` holds if for every term `M` of type
`A` the proposition `B M` holds. Here `B M` stands for
the proposition `B x` with each free occurrence of `x` replaced by
`M`. The variable `x` appears free in `B x` but bound in
`∀ (x : A) → B x`. We formalise universal quantification using the
dependent function type, which has appeared throughout this book.
Evidence that `∀ (x : A) → B x` holds is of the form
λ (x : A) → N
where `N` is a term of type `B x`, and `N x` and `B x` both contain
a free variable `x` of type `A`. Given a term `L` providing evidence
that `∀ (x : A) → B x` holds, and a term `M` of type `A`, the term `L
M` provides evidence that `B M` holds. In other words, evidence that
`∀ (x : A) → B x` holds is a function that converts a term `M` of type
`A` into evidence that `B M` holds.
Put another way, if we know that `∀ (x : A) → B x` holds and that `M`
is a term of type `A` then we may conclude that `B M` holds.
\begin{code}
∀-elim : ∀ {A : Set} {B : A → Set} → (∀ (x : A) → B x) → (M : A) → B M
∀-elim L M = L M
\end{code}
As with `→-elim`, the rule corresponds to function application.
Functions arise as a special case of dependent functions,
where the range does not depend on a variable drawn from the domain.
When a function is viewed as evidence of implication, both its
argument and result are viewed as evidence, whereas when a dependent
function is viewed as evidence of a universal, its argument is viewed
as an element of a data type and its result is viewed as evidence of
a proposition that depends on the argument. This difference is largely
a matter of interpretation, since in Agda values of a type and
evidence of a proposition are indistinguishable.
Dependent function types are sometimes referred to as dependent products,
because if `A` is a finite type with values `x₁ , ⋯ , xᵢ`, and if
each of the types `B x₁ , ⋯ , B xᵢ` has `m₁ , ⋯ , mᵢ` distinct members,
then `∀ (x : A) → B x` has `m₁ * ⋯ * mᵢ` members.
Indeed, sometimes the notation `∀ (x : A) → B x`
is replaced by a notation such as `Π[ x ∈ A ] (B x)`,
where `Π` stands for product. However, we will stick with the name
dependent function, because (as we will see) dependent product is ambiguous.
### Exercise (`∀-distrib-×`)
Show that universals distribute over conjunction.
\begin{code}
∀-Distrib-× = ∀ {A : Set} {B C : A → Set} →
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
\end{code}
Compare this with the result (`→-distrib-×`) in Chapter [Connectives](Connectives).
### Exercise (`⊎∀-implies-∀⊎`)
Show that a disjunction of universals implies a universal of disjunctions.
\begin{code}
⊎∀-Implies-∀⊎ = ∀ {A : Set} { B C : A → Set } →
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
\end{code}
Does the converse hold? If so, prove; if not, explain why.
## Existentials
Given a variable `x` of type `A` and a proposition `B x` which
contains `x` as a free variable, the existentially quantified
proposition `Σ[ x ∈ A ] B x` holds if for some term `M` of type
`A` the proposition `B M` holds. Here `B M` stands for
the proposition `B x` with each free occurrence of `x` replaced by
`M`. The variable `x` appears free in `B x` but bound in
`Σ[ x ∈ A ] B x`.
We formalise existential quantification by declaring a suitable
inductive type.
\begin{code}
data Σ (A : Set) (B : A → Set) : Set where
_,_ : (x : A) → B x → Σ A B
\end{code}
We define a convenient syntax for existentials as follows.
\begin{code}
infix 2 Σ-syntax
Σ-syntax = Σ
syntax Σ-syntax A (λ x → B) = Σ[ x ∈ A ] B
\end{code}
This is our first use of a syntax declaration, which specifies that
the term on the left may be written with the syntax on the right.
The special syntax is available only when the identifier
`Σ-syntax` is imported.
Evidence that `Σ[ x ∈ A ] B x` holds is of the form
`(M , N)` where `M` is a term of type `A`, and `N` is evidence
that `B M` holds.
Equivalently, we could also declare existentials as a record type.
\begin{code}
record Σ′ (A : Set) (B : A → Set) : Set where
field
proj₁′ : A
proj₂′ : B proj₁′
\end{code}
Here record construction
record
{ proj₁′ = M
; proj₂′ = N
}
corresponds to the term
( M , N )
where `M` is a term of type `A` and `N` is a term of type `B M`.
Products arise a special case of existentials, where the second
component does not depend on a variable drawn from the first
component. When a product is viewed as evidence of a conjunction,
both of its components are viewed as evidence, whereas when it is
viewed as evidence of an existential, the first component is viewed as
an element of a datatype and the second component is viewed as
evidence of a proposition that depends on the first component. This
difference is largely a matter of interpretation, since in Agda values
of a type and evidence of a proposition are indistinguishable.
Existentials are sometimes referred to as dependent sums,
because if `A` is a finite type with values `x₁ , ⋯ , xᵢ`, and if
each of the types `B x₁ , ⋯ B xᵢ` has `m₁ , ⋯ , mᵢ` distinct members,
then `Σ[ x ∈ A] B x` has `m₁ + ⋯ + mᵢ` members, which explains the
choice of notation for existentials, since `Σ` stands for sum.
Existentials are sometimes referred to as dependent products, since
products arise as a special case. However, that choice of names is
doubly confusing, since universal also have a claim to the name dependent
product and since existential also have a claim to the name dependent sum.
A common notation for existentials is `∃` (analogous to `∀` for universals).
We follow the convention of the Agda standard library, and reserve this
notation for the case where the domain of the bound variable is left implicit.
\begin{code}
∃ : ∀ {A : Set} (B : A → Set) → Set
∃ {A} B = Σ A B
∃-syntax = ∃
syntax ∃-syntax (λ x → B) = ∃[ x ] B
\end{code}
The special syntax is available only when the identifier `∃-syntax` is imported.
We will tend to use this syntax, since it is shorter and more familiar.
Given evidence that `∀ x → B x → C` holds, where `C` does not contain
`x` as a free variable, and given evidence that `∃[ x ] B x` holds, we
may conclude that `C` holds.
\begin{code}
∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} → (∀ x → B x → C) → ∃[ x ] B x → C
∃-elim f (x , y) = f x y
\end{code}
In other words, if we know for every `x` of type `A` that `B x`
implies `C`, and we know for some `x` of type `A` that `B x` holds,
then we may conclude that `C` holds. This is because we may
instantiate that proof that `∀ x → B x → C` to any value `x` of type
`A` and any `y` of type `B x`, and exactly such values are provided by
the evidence for `∃[ x ] B x`.
Indeed, the converse also holds, and the two together form an isomorphism.
\begin{code}
∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set} → (∀ x → B x → C) ≃ (∃[ x ] B x → C)
∀∃-currying =
record
{ to = λ{ f → λ{ (x , y) → f x y }}
; from = λ{ g → λ{ x → λ{ y → g (x , y) }}}
; from∘to = λ{ f → refl }
; to∘from = λ{ g → extensionality λ{ (x , y) → refl }}
}
\end{code}
The result can be viewed as a generalisation of currying. Indeed, the code to
establish the isomorphism is identical to what we wrote when discussing
[implication][implication].
[implication]: Connectives/index.html#implication
### Exercise (`∃-distrib-⊎`)
Show that universals distribute over conjunction.
\begin{code}
∃-Distrib-⊎ = ∀ {A : Set} {B C : A → Set} →
∃[ x ] (B x ⊎ C x) ≃ (∃[ x ] B x) ⊎ (∃[ x ] C x)
\end{code}
### Exercise (`∃×-implies-×∃`)
Show that an existential of conjunctions implies a conjunction of existentials.
\begin{code}
∃×-Implies-×∃ = ∀ {A : Set} { B C : A → Set } →
∃[ x ] (B x × C x) → (∃[ x ] B x) × (∃[ x ] C x)
\end{code}
Does the converse hold? If so, prove; if not, explain why.
## An existential example
Recall the definitions of `even` and `odd` from Chapter [Relations](Relations).
\begin{code}
data even : ℕ → Set
data odd : ℕ → Set
data even where
even-zero : even zero
even-suc : ∀ {n : ℕ} → odd n → even (suc n)
data odd where
odd-suc : ∀ {n : ℕ} → even n → odd (suc n)
\end{code}
A number is even if it is zero or the successor of an odd number, and
odd if it the successor of an even number.
We will show that a number is even if and only if it is twice some
other number, and odd if and only if it is one more than twice
some other number. In other words, we will show
even n iff ∃[ m ] ( m * 2 ≡ n)
odd n iff ∃[ m ] (1 + m * 2 ≡ n)
By convention, one tends to write constant factors first and to put
the constant term in a sum last. Here we've reversed each of those
conventions, because doing so eases the proof.
Here is the proof in the forward direction.
\begin{code}
even-∃ : ∀ {n : ℕ} → even n → ∃[ m ] ( m * 2 ≡ n)
odd-∃ : ∀ {n : ℕ} → odd n → ∃[ m ] (1 + m * 2 ≡ n)
even-∃ even-zero = zero , refl
even-∃ (even-suc o) with odd-∃ o
... | m , refl = suc m , refl
odd-∃ (odd-suc e) with even-∃ e
... | m , refl = m , refl
\end{code}
We define two mutually recursive functions. Given
evidence that `n` is even or odd, we return a
number `m` and evidence that `m * 2 ≡ n` or `1 + m * 2 ≡ n`.
We induct over the evidence that `n` is even or odd.
- If the number is even because it is zero, then we return a pair
consisting of zero and the (trivial) proof that twice zero is zero.
- If the number is even because it is one more than an odd number,
then we apply the induction hypothesis to give a number `m` and
evidence that `1 + m * 2 ≡ n`. We return a pair consisting of `suc m`
and evidence that `suc m * 2` ≡ suc n`, which is immediate after
substituting for `n`.
- If the number is odd because it is the successor of an even number,
then we apply the induction hypothesis to give a number `m` and
evidence that `m * 2 ≡ n`. We return a pair consisting of `suc m` and
evidence that `1 + 2 * m = suc n`, which is immediate after
substituting for `n`.
This completes the proof in the forward direction.
Here is the proof in the reverse direction.
\begin{code}
∃-even : ∀ {n : ℕ} → ∃[ m ] ( m * 2 ≡ n) → even n
∃-odd : ∀ {n : ℕ} → ∃[ m ] (1 + m * 2 ≡ n) → odd n
∃-even ( zero , refl) = even-zero
∃-even (suc m , refl) = even-suc (∃-odd (m , refl))
∃-odd ( m , refl) = odd-suc (∃-even (m , refl))
\end{code}
Given a number that is twice some other number we must show it is
even, and a number that is one more than twice some other number we
must show it is odd. We induct over the evidence of the existential,
and in the even case consider the two possibilities for the number
that is doubled.
- In the even case for `zero`, we must show `2 * zero` is even, which
follows by `even-zero`.
- In the even case for `suc n`, we must show `2 * suc m` is even. The
inductive hypothesis tells us that `1 + 2 * m` is odd, from which the
desired result follows by `even-suc`.
- In the odd case, we must show `1 + m * 2` is odd. The inductive
hypothesis tell us that `m * 2` is even, from which the desired result
follows by `odd-suc`.
This completes the proof in the backward direction.
### Exercise (`∃-even′, ∃-odd′`)
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.
## Existentials, Universals, and Negation
Negation of an existential is isomorphic to universal
of a negation. Considering that existentials are generalised
disjunction and universals are generalised conjunction, this
result is analogous to the one which tells us that negation
of a disjunction is isomorphic to a conjunction of negations.
\begin{code}
¬∃∀ : ∀ {A : Set} {B : A → Set} → (¬ ∃[ x ] B x) ≃ ∀ x → ¬ B x
¬∃∀ =
record
{ to = λ{ ¬∃xy x y → ¬∃xy (x , y) }
; from = λ{ ∀¬xy (x , y) → ∀¬xy x y }
; from∘to = λ{ ¬∃xy → extensionality λ{ (x , y) → refl } }
; to∘from = λ{ ∀¬xy → refl }
}
\end{code}
In the `to` direction, we are given a value `¬∃xy` of type
`¬ ∃[ x ] B x`, and need to show that given a value
`x` that `¬ B x` follows, in other words, from
a value `y` of type `B x` we can derive false. Combining
`x` and `y` gives us a value `(x , y)` of type `∃[ x ] B x`,
and applying `¬∃xy` to that yields a contradiction.
In the `from` direction, we are given a value `∀¬xy` of type
`∀ x → ¬ B x`, and need to show that from a value `(x , y)`
of type `∃[ x ] B x` we can derive false. Applying `∀¬xy`
to `x` gives a value of type `¬ B x`, and applying that to `y` yields
a contradiction.
The two inverse proofs are straightforward, where one direction
requires extensionality.
### Exercise (`∃¬-Implies-¬∀`)
Show `∃[ x ] ¬ B x → ¬ (∀ x → B x)`.
Does the converse hold? If so, prove; if not, explain why.
## Standard Prelude
Definitions similar to those in this chapter can be found in the standard library.
\begin{code}
import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
\end{code}
## Unicode
This chapter uses the following unicode.
∃ U+2203 THERE EXISTS (\ex, \exists)

0
src/ListsAns.lagda → src/answers/ListsAns.lagda
View file

0
src/NegationAns.lagda → src/answers/NegationAns.lagda
View file

0
src/PropertiesAns.lagda → src/answers/PropertiesAns.lagda
View file

0
src/RelationsAns.lagda → src/answers/RelationsAns.lagda
View file

31
src/extra/Nat.agda Normal file
View file

@ -0,0 +1,31 @@
module Nat where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}
_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)
_ : 2 + 3 ≡ 5
_ =
begin
2 + 3
≡⟨⟩
suc (1 + 3)
≡⟨⟩
suc (suc (0 + 3))
≡⟨⟩
suc (suc 3)
≡⟨⟩
5
∎