making sure everything is committed
This commit is contained in:
wadler
parent
9f58620f8d
commit
858e191639
5 changed files with 142 additions and 64 deletions
|
|
@ -20,6 +20,7 @@ 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 (contraposition)
|
||||
renaming (contradiction to ¬¬-intro)
|
||||
open import Data.Unit using (⊤; tt)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.List using (List; []; _∷_; foldr; map)
|
||||
|
|
@ -128,7 +129,6 @@ no possible evidence that `T b` holds if `b` is false.
|
|||
|
||||
Another way to put this is that `T b` is inhabited exactly when `b ≡ true`
|
||||
is inhabited.
|
||||
|
||||
In the forward direction, we need to do a case analysis on the boolean `b`.
|
||||
\begin{code}
|
||||
T→≡ : ∀ (b : Bool) → T b → b ≡ true
|
||||
|
|
@ -276,14 +276,14 @@ trouble normalising evidence of negation.)
|
|||
|
||||
## Decidables from booleans, and booleans from decidables
|
||||
|
||||
Curious readers might wonder if we could reuse the definition of `m ≤ᵇ
|
||||
n`, together with the proofs that it is equivalent to `m ≤ n`, to show
|
||||
Curious readers might wonder if we could reuse the definition of
|
||||
`m ≤ᵇ n`, together with the proofs that it is equivalent to `m ≤ n`, to show
|
||||
decidability. Indeed we can do so as follows.
|
||||
\begin{code}
|
||||
_≤?′_ : ∀ (m n : ℕ) → Dec (m ≤ n)
|
||||
m ≤?′ n with m ≤ᵇ n | ≤ᵇ→≤ m n | ≤→≤ᵇ {m} {n}
|
||||
... | true | p | _ = yes (p tt)
|
||||
... | false | _ | ¬p = no ¬p
|
||||
... | true | p | _ = yes (p tt)
|
||||
... | false | _ | ¬p = no ¬p
|
||||
\end{code}
|
||||
If `m ≤ᵇ n` is true then `≤ᵇ→≤` yields a proof that `m ≤ n` holds,
|
||||
while if it is false then `≤→≤ᵇ` takes a proof the `m ≤ n` holds into a contradiction.
|
||||
|
|
@ -304,7 +304,7 @@ then Agda would make two complaints, one for each clause
|
|||
T (m ≤ᵇ n) !=< ⊥ of type Set
|
||||
when checking that the expression ≤→≤ᵇ {m} {n} has type ¬ m ≤ n
|
||||
|
||||
Putting the expressions into the with clause permits Agda to exploit
|
||||
Putting the expressions into the `with` clause permits Agda to exploit
|
||||
the fact that `T (m ≤ᵇ n)` is `⊤` when `m ≤ᵇ n` is true, and that
|
||||
`T (m ≤ᵇ n)` is `⊥` when `m ≤ᵇ n` is false.
|
||||
|
||||
|
|
@ -401,6 +401,11 @@ true ∨ _ = true
|
|||
_ ∨ true = true
|
||||
false ∨ false = false
|
||||
\end{code}
|
||||
In Emacs, the left-hand side of the second equation displays in grey,
|
||||
indicating that the order of the equations determines which of the
|
||||
first or the second can match. However, regardless of which matches
|
||||
the answer is the same.
|
||||
|
||||
Correspondingly, given two decidable propositions, we can
|
||||
decide their disjunction.
|
||||
\begin{code}
|
||||
|
|
@ -417,6 +422,12 @@ If either holds, we inject the evidence to yield
|
|||
evidence of the disjunct. If the negation of both hold,
|
||||
assuming either disjunct will lead to a contradiction.
|
||||
|
||||
Again in Emacs, the left-hand side of the second equation displays in grey,
|
||||
indicating that the order of the equations determines which of the
|
||||
first or the second can match. This time the answer is different depending
|
||||
on which matches; if both disjuncts hold we pick the first,
|
||||
but it would be equally valid to pick the second.
|
||||
|
||||
The negation of a boolean is false if its argument is true,
|
||||
and vice versa.
|
||||
\begin{code}
|
||||
|
|
@ -427,9 +438,9 @@ not false = true
|
|||
Correspondingly, given a decidable proposition, we
|
||||
can decide its negation.
|
||||
\begin{code}
|
||||
not? : {A : Set} → Dec A → Dec (¬ A)
|
||||
not? (yes x) = no λ{ ¬x → ¬x x }
|
||||
not? (no ¬x) = yes ¬x
|
||||
¬? : {A : Set} → Dec A → Dec (¬ A)
|
||||
¬? (yes x) = no (¬¬-intro x)
|
||||
¬? (no ¬x) = yes ¬x
|
||||
\end{code}
|
||||
We simply swap yes and no. In the first equation,
|
||||
the right-hand side asserts that the negation of `¬ A` holds,
|
||||
|
|
@ -449,6 +460,10 @@ whenever the first is true then the second is true.
|
|||
Hence, the implication of two booleans is true if
|
||||
the second is true or the first is false,
|
||||
and false if the first is true and the second is false.
|
||||
In Emacs, the left-hand side of the second equation displays in grey,
|
||||
indicating that the order of the equations determines which of the
|
||||
first or the second can match. However, regardless of which matches
|
||||
the answer is the same.
|
||||
|
||||
Correspondingly, given two decidable propositions,
|
||||
we can decide if the first implies the second.
|
||||
|
|
@ -472,6 +487,12 @@ we apply the evidence of the implication `f` to the evidence of the
|
|||
first `x`, yielding a contradiction with the evidence `¬y` of
|
||||
the negation of the second.
|
||||
|
||||
Again in Emacs, the left-hand side of the second equation displays in grey,
|
||||
indicating that the order of the equations determines which of the
|
||||
first or the second can match. This time the answer is different depending
|
||||
on which matches; but either is equally valid.
|
||||
|
||||
|
||||
## Decidability of All
|
||||
|
||||
Recall that in Chapter [Lists](Lists#All) we defined a predicate `All P`
|
||||
|
|
@ -500,17 +521,17 @@ a function of type `A → Set`, taking a value `x` of type `A` into evidence
|
|||
if we have a function that for a given `x` can decide `P x`.
|
||||
\begin{code}
|
||||
Decidable : ∀ {A : Set} → (A → Set) → Set
|
||||
Decidable {A} P = (x : A) → Dec (P x)
|
||||
Decidable {A} P = ∀ (x : A) → Dec (P x)
|
||||
\end{code}
|
||||
Then if predicate `P` is decidable, it is also decidable whether every
|
||||
element of a list satisfies the predicate.
|
||||
\begin{code}
|
||||
all? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (All P)
|
||||
all? p? [] = yes []
|
||||
all? p? (x ∷ xs) with p? x | all? p? xs
|
||||
... | yes px | yes pxs = yes (px ∷ pxs)
|
||||
... | no ¬px | _ = no λ{ (px ∷ pxs) → ¬px px }
|
||||
... | _ | no ¬pxs = no λ{ (px ∷ pxs) → ¬pxs pxs }
|
||||
All? : ∀ {A : Set} {P : A → Set} → Decidable P → Decidable (All P)
|
||||
All? P? [] = yes []
|
||||
All? P? (x ∷ xs) with P? x | All? P? xs
|
||||
... | yes Px | yes Pxs = yes (Px ∷ Pxs)
|
||||
... | no ¬Px | _ = no λ{ (Px ∷ Pxs) → ¬Px Px }
|
||||
... | _ | no ¬Pxs = no λ{ (Px ∷ Pxs) → ¬Pxs Pxs }
|
||||
\end{code}
|
||||
If the list is empty, then trivially `P` holds for every element of
|
||||
the list. Otherwise, the structure of the proof is similar to that
|
||||
|
|
@ -525,8 +546,21 @@ predicate holds for every element of a list, so does `Any` have
|
|||
analogues `any` and `any?` which determine whether a predicates holds
|
||||
for some element of a list. Give their definitions.
|
||||
|
||||
<!-- import Data.List.All using (All; []; _∷_) renaming (all to all?) -->
|
||||
## Standard Library
|
||||
|
||||
\begin{code}
|
||||
import Data.Bool.Base using (Bool; T; _∧_; _∨_; not)
|
||||
import Data.Nat.Base using (_≤?_)
|
||||
import Data.List.All using (All; []; _∷_) renaming (all to All?)
|
||||
import Relation.Nullary using (Dec; yes; no)
|
||||
import Relation.Nullary.Decidable using (⌊_⌋; toWitness; fromWitness)
|
||||
import Relation.Nullary.Negation using (¬?)
|
||||
import Relation.Nullary.Product using (_×-dec_)
|
||||
import Relation.Nullary.Sum using (_⊎-dec_)
|
||||
\end{code}
|
||||
|
||||
|
||||
## Unicode
|
||||
|
||||
ᵇ U+1D47 MODIFIER LETTER SMALL B (\^b)
|
||||
|
||||
|
|
|
|||
|
|
@ -14,7 +14,7 @@ examples of polymorphic types and higher-order functions.
|
|||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; sym; trans; cong)
|
||||
open Eq.≡-Reasoning
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _≤_; s≤s; z≤n)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
|
||||
open import Data.Nat.Properties using
|
||||
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
|
||||
open import Relation.Nullary using (¬_)
|
||||
|
|
@ -343,8 +343,8 @@ Reversing a list in this way takes time *quadratic* in the length of
|
|||
the list. This is because reverse ends up appending lists of lengths
|
||||
`1`, `2`, up to `n - 1`, where `n` is the length of the list being
|
||||
reversed, append takes time linear in the length of the first
|
||||
list, and the sum of the numbers up to `n` is `n * (n + 1) / 2`.
|
||||
(We will validate that last fact later in this chapter.)
|
||||
list, and the sum of the numbers up to `n - 1` is `n * (n - 1) / 2`.
|
||||
(We will validate that last fact in an exercise later in this chapter.)
|
||||
|
||||
### Exercise (`reverse-++-commute`)
|
||||
|
||||
|
|
@ -544,8 +544,8 @@ the head of the list and the fold of the tail of the list.
|
|||
|
||||
Here is an example showing how to use fold to find the sum of a list.
|
||||
\begin{code}
|
||||
ex₇ : foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10
|
||||
ex₇ =
|
||||
_ : foldr _+_ 0 [ 1 , 2 , 3 , 4 ] ≡ 10
|
||||
_ =
|
||||
begin
|
||||
foldr _+_ 0 (1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
|
||||
≡⟨⟩
|
||||
|
|
@ -570,7 +570,14 @@ sum : List ℕ → ℕ
|
|||
sum = foldr _+_ 0
|
||||
|
||||
_ : sum [ 1 , 2 , 3 , 4 ] ≡ 10
|
||||
_ = ex₇
|
||||
_ =
|
||||
begin
|
||||
sum [ 1 , 2 , 3 , 4 ]
|
||||
≡⟨⟩
|
||||
foldr _+_ 0 [ 1 , 2 , 3 , 4 ]
|
||||
≡⟨⟩
|
||||
10
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
Just as the list type has two constructors, `[]` and `_∷_`,
|
||||
|
|
@ -579,13 +586,13 @@ so the fold function takes two arguments, `e` and `_⊕_`
|
|||
In general, a data type with *n* constructors will have
|
||||
a corresponding fold function that takes *n* arguments.
|
||||
|
||||
*Exercise* (`product`)
|
||||
## Exercise (`product`)
|
||||
|
||||
Use fold to define a function to find the product of a list of numbers.
|
||||
|
||||
product [ 1 , 2 , 3 , 4 ] ≡ 24
|
||||
|
||||
*Exercise* (`foldr-++`)
|
||||
### Exercise (`foldr-++`)
|
||||
|
||||
Show that fold and append are related as follows.
|
||||
\begin{code}
|
||||
|
|
@ -595,7 +602,7 @@ postulate
|
|||
\end{code}
|
||||
|
||||
|
||||
*Exercise* (`map-is-foldr`) <!-- `mapIsFold` in Data.List.Properties -->
|
||||
### Exercise (`map-is-foldr`)
|
||||
|
||||
Show that map can be defined using fold.
|
||||
\begin{code}
|
||||
|
|
@ -605,6 +612,33 @@ postulate
|
|||
\end{code}
|
||||
This requires extensionality.
|
||||
|
||||
### Exercise (`sum-downFrom`)
|
||||
|
||||
Define a function that counts down as follows.
|
||||
\begin{code}
|
||||
downFrom : ℕ → List ℕ
|
||||
downFrom zero = []
|
||||
downFrom (suc n) = n ∷ downFrom n
|
||||
\end{code}
|
||||
For example,
|
||||
\begin{code}
|
||||
_ : downFrom 3 ≡ [ 2 , 1 , 0 ]
|
||||
_ = refl
|
||||
\end{code}
|
||||
Prove that the sum of the numbers `(n - 1) + ⋯ + 0` is
|
||||
equal to `n * (n - 1) / 2`.
|
||||
\begin{code}
|
||||
postulate
|
||||
sum-downFrom : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
|
||||
\end{code}
|
||||
|
||||
|
||||
<!-- `mapIsFold` in Data.List.Properties -->
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
## Monoids
|
||||
|
||||
|
|
@ -828,9 +862,23 @@ Do we also have the following?
|
|||
|
||||
If so, prove; if not, explain why.
|
||||
|
||||
## Standard Library
|
||||
|
||||
Definitions similar to those in this chapter can be found in the standard library.
|
||||
\begin{code}
|
||||
import Data.List using (List; _++_; length; reverse; map; foldr; downFrom)
|
||||
import Data.List.All using (All)
|
||||
import Data.List.Any using (Any)
|
||||
import Algebra.Structures using (IsMonoid)
|
||||
\end{code}
|
||||
The standard library version of `IsMonoid` differs from the
|
||||
one given here, in that it is also parameterised on an equivalence relation.
|
||||
|
||||
|
||||
## Unicode
|
||||
|
||||
This chapter uses the following unicode.
|
||||
|
||||
∷ U+2237 PROPORTION (\::)
|
||||
⊗ U+2297 CIRCLED TIMES (\otimes)
|
||||
∈ U+2208 ELEMENT OF (\in)
|
||||
|
|
|
|||
|
|
@ -290,8 +290,8 @@ just a couple of lines.
|
|||
Here is the definition of addition in Agda:
|
||||
\begin{code}
|
||||
_+_ : ℕ → ℕ → ℕ
|
||||
zero + n = n -- (i)
|
||||
(suc m) + n = suc (m + n) -- (ii)
|
||||
zero + n = n
|
||||
(suc m) + n = suc (m + n)
|
||||
\end{code}
|
||||
|
||||
Let's unpack this definition. Addition is an infix operator. It is
|
||||
|
|
|
|||
|
|
@ -311,11 +311,9 @@ Stable A = ¬ ¬ A → A
|
|||
Show that any negated formula is stable, and that the conjunction
|
||||
of two stable formulas is stable.
|
||||
\begin{code}
|
||||
¬-Stable : Set₁
|
||||
¬-Stable = ∀ {A : Set} → Stable (¬ A)
|
||||
|
||||
×-Stable : Set₁
|
||||
×-Stable = ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
|
||||
postulate
|
||||
¬-stable : ∀ {A : Set} → Stable (¬ A)
|
||||
×-stable : ∀ {A B : Set} → Stable A → Stable B → Stable (A × B)
|
||||
\end{code}
|
||||
|
||||
## Standard Prelude
|
||||
|
|
|
|||
|
|
@ -8,8 +8,9 @@ permalink : /ListsAns
|
|||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl; sym; trans; cong)
|
||||
open Eq.≡-Reasoning
|
||||
open import Data.Nat using (ℕ; suc; zero; _+_; _*_)
|
||||
open import Data.Nat.Properties.Simple using (*-comm; distribʳ-*-+)
|
||||
open import Data.Nat using (ℕ; suc; zero; _+_; _*_; _∸_)
|
||||
open import Data.Nat.Properties using (*-comm; *-distribˡ-+)
|
||||
renaming (*-distribʳ-+ to funny-*-distribʳ-+)
|
||||
open import Data.List using (List; []; _∷_; [_]; _++_; length; foldr)
|
||||
open import Data.Product using (proj₁; proj₂)
|
||||
\end{code}
|
||||
|
|
@ -82,14 +83,6 @@ reverse [] = []
|
|||
reverse (x ∷ xs) = reverse xs ++ [ x ]
|
||||
\end{code}
|
||||
|
||||
The proof of distribution of multiplication over addition from
|
||||
the standard library takes its arguments in a strange order.
|
||||
We fix that here.
|
||||
\begin{code}
|
||||
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
|
||||
*-distrib-+ m n p = distribʳ-*-+ p m n
|
||||
\end{code}
|
||||
|
||||
|
||||
## Reverse and append
|
||||
|
||||
|
|
@ -150,39 +143,44 @@ reverse-involutive (x ∷ xs) =
|
|||
|
||||
## Sum of count
|
||||
|
||||
The proof of distribution of multiplication over addition from
|
||||
the standard library takes its arguments in a strange order.
|
||||
We fix that here.
|
||||
\begin{code}
|
||||
*-distribʳ-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
|
||||
*-distribʳ-+ m n p = funny-*-distribʳ-+ p m n
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
sum : List ℕ → ℕ
|
||||
sum = foldr _+_ 0
|
||||
|
||||
countdown : ℕ → List ℕ
|
||||
countdown zero = []
|
||||
countdown (suc n) = suc n ∷ countdown n
|
||||
|
||||
infix 6 _+
|
||||
|
||||
_+ : ℕ → ℕ → ℕ
|
||||
(m +) n = m + n
|
||||
downFrom : ℕ → List ℕ
|
||||
downFrom zero = []
|
||||
downFrom (suc n) = n ∷ downFrom n
|
||||
|
||||
cong2 : ∀ {A B C : Set} {x x′ : A} {y y′ : B} →
|
||||
(f : A → B → C) → (x ≡ x′) → (y ≡ y′) → (f x y ≡ f x′ y′)
|
||||
cong2 f x≡x′ y≡y′ rewrite x≡x′ | y≡y′ = refl
|
||||
|
||||
sum-countdown : ∀ (n : ℕ) → sum (countdown n) * 2 ≡ suc n * n
|
||||
sum-countdown zero = refl
|
||||
sum-countdown (suc n) =
|
||||
sum-downFrom : ∀ (n : ℕ) → sum (downFrom n) * 2 ≡ n * (n ∸ 1)
|
||||
sum-downFrom zero = refl
|
||||
sum-downFrom (suc zero) = refl
|
||||
sum-downFrom (suc (suc n)) =
|
||||
begin
|
||||
sum (countdown (suc n)) * 2
|
||||
sum (downFrom (suc (suc n))) * 2
|
||||
≡⟨⟩
|
||||
sum (suc n ∷ countdown n) * 2
|
||||
sum (suc n ∷ downFrom (suc n)) * 2
|
||||
≡⟨⟩
|
||||
(suc n + sum (countdown n)) * 2
|
||||
≡⟨ *-distrib-+ (suc n) (sum (countdown n)) 2 ⟩
|
||||
suc n * 2 + sum (countdown n) * 2
|
||||
≡⟨ cong (suc n * 2 +) (sum-countdown n) ⟩
|
||||
(suc n + sum (downFrom (suc n))) * 2
|
||||
≡⟨ *-distribʳ-+ (suc n) (sum (downFrom (suc n))) 2 ⟩
|
||||
suc n * 2 + sum (downFrom (suc n)) * 2
|
||||
≡⟨ cong (suc n * 2 +_) (sum-downFrom (suc n)) ⟩
|
||||
suc n * 2 + suc n * n
|
||||
≡⟨ cong2 _+_ (*-comm (suc n) 2) (*-comm (suc n) n) ⟩
|
||||
2 * suc n + n * suc n
|
||||
≡⟨ sym (*-distrib-+ 2 n (suc n))⟩
|
||||
(2 + n) * suc n
|
||||
≡⟨ sym (*-distribˡ-+ (suc n) 2 n) ⟩
|
||||
suc n * (2 + n)
|
||||
≡⟨ *-comm (suc n) (2 + n) ⟩
|
||||
suc (suc n) * suc n
|
||||
∎
|
||||
\end{code}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue