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

finished Quantifiers (again)

Browse source
This commit is contained in:
wadler 2018-03-18 19:13:27 -03:00
parent 63f65333e3
commit cd37b8a2ce
1 changed files with 95 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

167
src/Quantifiers.lagda
View file

@ -61,21 +61,21 @@ is a term of type `A` then we may conclude that `B M` holds.
\end{code} \end{code}
As with `→-elim`, the rule corresponds to function application. As with `→-elim`, the rule corresponds to function application.
Function types arise as a special case of dependent function types, Functions arise as a special case of dependent functions,
where the range does not depend on a variable drawn from the domain. where the range does not depend on a variable drawn from the domain.
When a function is viewed as evidence of implication, both its When a function is viewed as evidence of implication, both its
argument and result are viewed as evidence, whereas when a dependent argument and result are viewed as evidence, whereas when a dependent
function is viewed as evidence of a universal, its argument is viewed 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 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 proposition that depends on the argument. This difference is largely
a matter of interpretation, since in Agda data types and types of a matter of interpretation, since in Agda values of a type and
evidence are indistinguishable. evidence of a proposition are indistinguishable.
Dependent function types are sometimes referred to as dependent products, Dependent function types are sometimes referred to as dependent products,
because if `A` is a finite type with values `{ x₁ , ⋯ , xᵢ }`, and if 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, each of the types `B x₁ , ⋯ , B xᵢ` has `m₁ , ⋯ , mᵢ` distinct members,
then `∀ (x : A) → B x` has `m₁ × ⋯ × mᵢ` members. Because of this then `∀ (x : A) → B x` has `m₁ * ⋯ * mᵢ` members.
association, sometimes the notation `∀ (x : A) → B x` Indeed, sometimes the notation `∀ (x : A) → B x`
is replaced by a notation such as `Π[ 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 where `Π` stands for product. However, we will stick with the name
dependent function, because (as we will see) dependent product is ambiguous. dependent function, because (as we will see) dependent product is ambiguous.
@ -104,28 +104,41 @@ Does the converse hold? If so, prove; if not, explain why.
Given a variable `x` of type `A` and a proposition `B x` which Given a variable `x` of type `A` and a proposition `B x` which
contains `x` as a free variable, the existentially quantified contains `x` as a free variable, the existentially quantified
proposition `∃ (λ (x : A) → B x)` holds if for some term `M` of type proposition `Σ[ x ∈ A ] B x` holds if for some term `M` of type
`A` the proposition `B M` holds. Here `B M` stands for `A` the proposition `B M` holds. Here `B M` stands for
the proposition `B x` with each free occurrence of `x` replaced by the proposition `B x` with each free occurrence of `x` replaced by
`M`. The variable `x` appears free in `B x` but bound in `M`. The variable `x` appears free in `B x` but bound in
`∃ (λ (x : A) → B x)`. `Σ[ x ∈ A ] B x`.
We formalise existential quantification by declaring a suitable We formalise existential quantification by declaring a suitable
inductive type. inductive type.
\begin{code} \begin{code}
data ∃ {A : Set} (B : A → Set) : Set where data Σ (A : Set) (B : A → Set) : Set where
_,_ : (x : A) → B x → ∃ B _,_ : (x : A) → B x → Σ A B
\end{code} \end{code}
Evidence that `∃ (λ (x : A) → B x)` holds is of the form 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 `(M , N)` where `M` is a term of type `A`, and `N` is evidence
that `B M` holds. that `B M` holds.
Equivalently, we could also declare existentials as a record type. Equivalently, we could also declare existentials as a record type.
\begin{code} \begin{code}
record ∃′ {A : Set} (B : A → Set) : Set where record Σ′ (A : Set) (B : A → Set) : Set where
field field
proj₁ : A proj₁′ : A
proj₂ : B proj₁ proj₂′ : B proj₁′
\end{code} \end{code}
Here record construction Here record construction
@ -140,65 +153,73 @@ corresponds to the term
where `M` is a term of type `A` and `N` is a term of type `B M`. where `M` is a term of type `A` and `N` is a term of type `B M`.
Given evidence that `∃ (λ (x : A) → B x)` holds, and Products arise a special case of existentials, where the second
given evidence that `∀ (x : A) → B x → C` holds, where `C` does component does not depend on a variable drawn from the first
not contain `x` as a free variable, we may conclude that `C` holds. 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} \begin{code}
∃-elim : ∀ {A : Set} {B : A → Set} {C : Set} → ∃ : ∀ {A : Set} (B : A → Set) → Set
(∃ (λ (x : A) → B x)) → (∀ (x : A) → B x → C) → C ∃ {A} B = Σ A B
∃-elim (M , N) P = P M N
∃-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} \end{code}
In other words, if we know for every `x` of type `A` that `B x` 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, 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 then we may conclude that `C` holds. This is because we may
instantiate that proof that `∀ (x : A) → B x → C` to any value instantiate that proof that `∀ x → B x → C` to any value `x` of type
`M` of type `A` and any `N` of type `B M`, and exactly such values `A` and any `y` of type `B x`, and exactly such values are provided by
are provided by the evidence for `∃ (λ (x : A) → B x)`. the evidence for `∃[ x ] B x`.
Products arise a special case of existentials, where the second Indeed, the converse also holds, and the two together form an isomorphism.
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 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 data types and
types of evidence 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. Because of this
association, sometimes the notation `∃ (λ (x : A) → B x)`
is replaced by a notation such as `Σ[ x ∈ A ] (B x)`,
where `Σ` 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, because universals also have
a claim to the name dependent product, and because existentials
have a claim to the name dependent sum.
Agda makes it possible to define our own syntactic abbreviations.
\begin{code} \begin{code}
∃-syntax = ∃ ∀∃-currying : ∀ {A : Set} {B : A → Set} {C : Set} → (∀ x → B x → C) ≃ (∃[ x ] B x → C)
syntax ∃-syntax (λ x → B) = ∃[ x ] B ∀∃-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} \end{code}
This allows us to write `∃[ x ] (B x)` in place of `∃ (λ x → B x)`. The result can be viewed as a generalisation of currying, and the code to
We could also define a syntax that makes the argument explicit. establish the isomorphism is identical.
\begin{code}
Σ-syntax = ∃
syntax Σ-syntax {A} (λ x → B) = Σ[ x ∈ A ] B
\end{code}
Both forms of syntax are provided by the Agda standard library.
We will usually use the first, as it is more compact.
As an example, recall the definitions of `even` and `odd` from
Chapter [Relations](Relations). ## Existential examples
Recall the definitions of `even` and `odd` from Chapter [Relations](Relations).
\begin{code} \begin{code}
data even : ℕ → Set data even : ℕ → Set
data odd : ℕ → Set data odd : ℕ → Set
@ -215,13 +236,15 @@ 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 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 other number, and odd if and only if it is one more than twice
some other number. some other number. In other words, we will show
First, we need a lemma, which allows us to > `even n` *iff* `∃[ m ] ( 2 * m ≡ n)`
simplify twice the successor of `m` to two > `odd n` *iff* `∃[ m ] (1 + 2 * m ≡ n)`
more than twice `m`.
First, we need a lemma, which allows us to simplify twice the
successor of `m` to two more than twice `m`.
\begin{code} \begin{code}
lemma : ∀ (m : ℕ) → 2 * suc m ≡ suc (suc (2 * m)) lemma : ∀ (m : ℕ) → 2 * suc m ≡ 2 + 2 * m
lemma m = lemma m =
begin begin
2 * suc m 2 * suc m
@ -232,7 +255,7 @@ lemma m =
≡⟨ cong suc (+-suc m (m + zero)) ⟩ ≡⟨ cong suc (+-suc m (m + zero)) ⟩
suc (suc (m + (m + zero))) suc (suc (m + (m + zero)))
≡⟨⟩ ≡⟨⟩
suc (suc (2 * m)) 2 + 2 * m
∎ ∎
\end{code} \end{code}
The lemma is straightforward, and uses the lemma The lemma is straightforward, and uses the lemma
@ -367,7 +390,7 @@ Does the converse hold? If so, prove; if not, explain why.
Definitions similar to those in this chapter can be found in the standard library. Definitions similar to those in this chapter can be found in the standard library.
\begin{code} \begin{code}
import Data.Product using (∃;_,_) import Data.Product using (Σ; _,_; ∃; Σ-syntax; ∃-syntax)
\end{code} \end{code}