renaming to match standard library
This commit is contained in:
wadler
parent
2fc99f5b5d
commit
0e4c77c0fb
3 changed files with 146 additions and 107 deletions
|
|
@ -452,13 +452,9 @@ Again, it is possible to assign our definition a meaning without
|
|||
resorting to unpermitted circularities. We do so by reducing our
|
||||
definition to equivalent inference rules for judgements about equality.
|
||||
|
||||
n : ℕ
|
||||
------------
|
||||
zero + n = n
|
||||
|
||||
m : ℕ
|
||||
n : ℕ
|
||||
p : ℕ
|
||||
m + n = p
|
||||
-------------------
|
||||
(suc m) + n = suc p
|
||||
|
|
|
|||
|
|
@ -15,20 +15,22 @@ by their name, properties of *inductive datatypes* are proved by
|
|||
Each chapter will begin with a list of the imports we require from the
|
||||
Agda standard library.
|
||||
|
||||
<!-- We will, of course, require the naturals;
|
||||
everything in the previous chapter is also found in the library module
|
||||
`Data.Nat`, so we import the required definitions from there.
|
||||
We also require propositional equality. -->
|
||||
<!-- We will, of course, require the naturals; everything in the
|
||||
previous chapter is also found in the library module `Data.Nat`, so we
|
||||
import the required definitions from there. We also require
|
||||
propositional equality. -->
|
||||
|
||||
\begin{code}
|
||||
open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
|
||||
\end{code}
|
||||
|
||||
Each import consists of the keywords `open` and `import`, followed by
|
||||
the module name, followed by the keyword `using`, followed by the
|
||||
names of each identifier imported from the module, surrounded by
|
||||
parentheses and separated by semicolons.
|
||||
parentheses and separated by semicolons. Parentheses and semicolons
|
||||
are among the few characters that cannot appear in names, so we do not
|
||||
need extra spaces in the import list.
|
||||
|
||||
|
||||
## Associativity
|
||||
|
|
@ -157,7 +159,6 @@ In order to prove associativity, we take `P m` to be the property
|
|||
Then the appropriate instances of the inference rules, which
|
||||
we must show to hold, become:
|
||||
|
||||
n : ℕ p : ℕ
|
||||
-------------------------------
|
||||
(zero + n) + p ≡ zero + (n + p)
|
||||
|
||||
|
|
@ -222,9 +223,9 @@ induction hypothesis.
|
|||
|
||||
We encode this proof in Agda as follows.
|
||||
\begin{code}
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p rewrite assoc+ m n p = refl
|
||||
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
+-assoc zero n p = refl
|
||||
+-assoc (suc m) n p rewrite +-assoc m n p = refl
|
||||
\end{code}
|
||||
Here we have named the proof `assoc+`. In Agda, identifiers can consist of
|
||||
any sequence of characters not including spaces or the characters `@.(){};_`.
|
||||
|
|
@ -290,15 +291,15 @@ in combination provide features that help to create proofs interactively.
|
|||
|
||||
Begin by typing
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ m n p = ?
|
||||
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
+-assoc m n p = ?
|
||||
|
||||
The question mark indicates that you would like Agda to help with
|
||||
filling in that part of the code. If you type `^C ^L` (control-C
|
||||
followed by control-L), the question mark will be replaced.
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ m n p = { }0
|
||||
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
+-assoc m n p = { }0
|
||||
|
||||
The empty braces are called a *hole*, and 0 is a number used for
|
||||
referring to the hole. The hole may display highlighted in green.
|
||||
|
|
@ -319,9 +320,9 @@ the prompt:
|
|||
Typing `m` will cause a split on that variable, resulting
|
||||
in an update to the code.
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = { }0
|
||||
assoc+ (suc m) n p = { }1
|
||||
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
+-assoc zero n p = { }0
|
||||
+-assoc (suc m) n p = { }1
|
||||
|
||||
There are now two holes, and the window at the bottom tells you what
|
||||
each is required to prove:
|
||||
|
|
@ -342,9 +343,9 @@ available to use in the proof. The proof of the given goal is
|
|||
trivial, and going into the goal and typing `^C ^R` will fill it in,
|
||||
renumbering the remaining hole to 0:
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p = { }0
|
||||
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
+-assoc zero n p = refl
|
||||
+-assoc (suc m) n p = { }0
|
||||
|
||||
Going into the new hold 0 and typing `^C ^,` will display the text:
|
||||
|
||||
|
|
@ -358,9 +359,9 @@ Again, this gives the simplified goal and the available variables.
|
|||
In this case, we need to rewrite by the induction
|
||||
hypothesis, so let's edit the text accordingly:
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p rewrite assoc+ m n p = { }0
|
||||
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
+-assoc zero n p = refl
|
||||
+-assoc (suc m) n p rewrite +-assoc m n p = { }0
|
||||
|
||||
Going into the remaining hole and typing `^C ^,` will show the
|
||||
goal is now trivial:
|
||||
|
|
@ -374,9 +375,9 @@ goal is now trivial:
|
|||
The proof of the given goal is trivial, and going into the goal and
|
||||
typing `^C ^R` will fill it in, completing the proof:
|
||||
|
||||
assoc+ : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
assoc+ zero n p = refl
|
||||
assoc+ (suc m) n p rewrite assoc+ m n p = refl
|
||||
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
|
||||
+-assoc zero n p = refl
|
||||
+-assoc (suc m) n p rewrite +-assoc m n p = refl
|
||||
|
||||
|
||||
## Creation, one last time
|
||||
|
|
@ -434,7 +435,6 @@ this by induction, we take `P m` to be the property
|
|||
Then the appropriate instances of the inference rules, which
|
||||
we must show to hold, become:
|
||||
|
||||
n : ℕ
|
||||
-------------------
|
||||
zero + n ≡ n + zero
|
||||
|
||||
|
|
@ -546,29 +546,73 @@ QED.
|
|||
|
||||
These proofs can be encoded concisely in Agda.
|
||||
\begin{code}
|
||||
com+zero : ∀ (n : ℕ) → n + zero ≡ n
|
||||
com+zero zero = refl
|
||||
com+zero (suc n) rewrite com+zero n = refl
|
||||
+-identity : ∀ (n : ℕ) → n + zero ≡ n
|
||||
+-identity zero = refl
|
||||
+-identity (suc n) rewrite +-identity n = refl
|
||||
|
||||
com+suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
|
||||
com+suc m zero = refl
|
||||
com+suc m (suc n) rewrite com+suc m n = refl
|
||||
+-suc : ∀ (m n : ℕ) → n + suc m ≡ suc (n + m)
|
||||
+-suc m zero = refl
|
||||
+-suc m (suc n) rewrite +-suc m n = refl
|
||||
|
||||
com+ : ∀ (m n : ℕ) → m + n ≡ n + m
|
||||
com+ zero n rewrite com+zero n = refl
|
||||
com+ (suc m) n rewrite com+suc m n | com+ m n = refl
|
||||
+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
|
||||
+-comm zero n rewrite +-identity n = refl
|
||||
+-comm (suc m) n rewrite +-suc m n | +-comm m n = refl
|
||||
\end{code}
|
||||
Here we have renamed Lemma (x) and (xi) to `com+zero` and `com+suc`,
|
||||
respectively. In the final line, rewriting with two equations
|
||||
(lemma (xi) and the inductive hypothesis) is indicated by
|
||||
separating the two proofs of the relevant equations by a vertical bar;
|
||||
the rewrites on the left is performed before that on the right.
|
||||
Here we have renamed Lemma (x) and (xi) to `+-identity` and `+-suc`,
|
||||
respectively. In the final line, rewriting with two equations is
|
||||
indicated by separating the two proofs of the relevant equations by a
|
||||
vertical bar; the rewrite on the left is performed before that on the
|
||||
right.
|
||||
|
||||
## Exercises
|
||||
|
||||
+ *Swapping terms*. Show
|
||||
|
||||
m + (n + p) ≡ n + (m + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`. No induction is needed,
|
||||
just apply the previous results which show addition
|
||||
is associative and commutative. You may need to use
|
||||
one or more of the following functions from the standard library:
|
||||
|
||||
sym : ∀ {m n : ℕ} → m ≡ n → n ≡ m
|
||||
trans : ∀ {m n p : ℕ} → m ≡ n → n ≡ p → m ≡ p
|
||||
|
||||
Name your proof `+-swap`.
|
||||
|
||||
+ *Multiplication distributes over addition*. Show
|
||||
|
||||
(m + n) * p = m * p + n * p
|
||||
|
||||
for all naturals `m`, `n`, and `p`. Name your proof `*-distrib-+`.
|
||||
|
||||
+ *Multiplication is associative*. Show
|
||||
|
||||
(m * n) * p ≡ m * (n * p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`. Name your proof `*-assoc`.
|
||||
|
||||
+ *Multiplication is commutative*. Show
|
||||
|
||||
m * n = n * m
|
||||
|
||||
for all naturals `m` and `n`. As with commutativity of addition,
|
||||
you will need to formulate and prove suitable lemmas.
|
||||
Name your proof `*-comm`.
|
||||
|
||||
+ *Monus from zero* Show
|
||||
|
||||
zero ∸ n = zero
|
||||
|
||||
for all naturals `n`. Did your proof require induction?
|
||||
Name your proof `0∸n≡0`.
|
||||
|
||||
+ *Associativity of monus with addition* Show
|
||||
|
||||
m ∸ n ∸ p = m ∸ (n + p)
|
||||
|
||||
for all naturals `m`, `n`, and `p`.
|
||||
Name your proof `∸-+-assoc`.
|
||||
|
||||
## Unicode
|
||||
|
||||
|
|
@ -576,4 +620,3 @@ In this chapter we use the following unicode.
|
|||
|
||||
≡ U+2261 IDENTICAL TO (\==)
|
||||
∀ U+2200 FOR ALL (\forall)
|
||||
λ U+03BB GREEK SMALL LETTER LAMBDA (\Gl, \lambda)
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@ the next step is to define relations, such as *less than or equal*.
|
|||
|
||||
\begin{code}
|
||||
open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_)
|
||||
open import Properties using (com+; com+zero; com+suc)
|
||||
open import Properties using (+-comm)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
|
||||
\end{code}
|
||||
|
||||
|
|
@ -158,13 +158,13 @@ such relations?)
|
|||
The first property to prove about comparison is that it is reflexive:
|
||||
for any natural `n`, the relation `n ≤ n` holds.
|
||||
\begin{code}
|
||||
refl≤ : ∀ (n : ℕ) → n ≤ n
|
||||
refl≤ zero = z≤n
|
||||
refl≤ (suc n) = s≤s (refl≤ n)
|
||||
≤-refl : ∀ (n : ℕ) → n ≤ n
|
||||
≤-refl zero = z≤n
|
||||
≤-refl (suc n) = s≤s (≤-refl n)
|
||||
\end{code}
|
||||
The proof is a straightforward induction on `n`. In the base case,
|
||||
`zero ≤ zero` holds by `z≤n`. In the inductive case, the inductive
|
||||
hypothesis `refl≤ n` gives us a proof of `n ≤ n`, and applying `s≤s`
|
||||
hypothesis `≤-refl n` gives us a proof of `n ≤ n`, and applying `s≤s`
|
||||
to that yields a proof of `suc n ≤ suc n`.
|
||||
|
||||
It is a good exercise to prove reflexivity interactively in Emacs,
|
||||
|
|
@ -177,9 +177,9 @@ The second property to prove about comparison is that it is
|
|||
transitive: for any naturals `m`, `n`, andl `p`, if `m ≤ n` and `n ≤
|
||||
p` hold, then `m ≤ p` holds.
|
||||
\begin{code}
|
||||
trans≤ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
|
||||
trans≤ z≤n _ = z≤n
|
||||
trans≤ (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤ m≤n n≤p)
|
||||
≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p
|
||||
≤-trans z≤n _ = z≤n
|
||||
≤-trans (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans m≤n n≤p)
|
||||
\end{code}
|
||||
Here the proof is most easily thought of as by induction on the
|
||||
*evidence* that `m ≤ n`, so we have left `m`, `n`, and `p` implicit.
|
||||
|
|
@ -195,20 +195,20 @@ In the inductive case, `m ≤ n` holds by `s≤s m≤n`, so it must be that `m`
|
|||
is `suc m′` and `n` is `suc n′` for some `m′` and `n′`, and `m≤n` is
|
||||
evidence that `m′ ≤ n′`. In this case, the only way that `p ≤ n` can
|
||||
hold is by `s≤s n≤p`, where `p` is `suc p′` for some `p′` and `n≤p` is
|
||||
evidence that `n′ ≤ p′`. The inductive hypothesis `trans≤ m≤n n≤p`
|
||||
evidence that `n′ ≤ p′`. The inductive hypothesis `≤-trans m≤n n≤p`
|
||||
provides evidence that `m′ ≤ p′`, and applying `s≤s` to that gives
|
||||
evidence of the desired conclusion, `suc m′ ≤ suc p′`.
|
||||
|
||||
The case `trans≤ (s≤s m≤n) z≤n` cannot arise, since the first piece of
|
||||
The case `≤-trans (s≤s m≤n) z≤n` cannot arise, since the first piece of
|
||||
evidence implies `n` must be `suc n′` for some `n′` while the second
|
||||
implies `n` must be `zero`. Agda can determine that such a case cannot
|
||||
arise, and does not require it to be listed.
|
||||
|
||||
Alternatively, we could make the implicit parameters explicit.
|
||||
\begin{code}
|
||||
trans≤′ : ∀ (m n p : ℕ) → m ≤ n → n ≤ p → m ≤ p
|
||||
trans≤′ zero n p z≤n _ = z≤n
|
||||
trans≤′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤′ m n p m≤n n≤p)
|
||||
≤-trans′ : ∀ (m n p : ℕ) → m ≤ n → n ≤ p → m ≤ p
|
||||
≤-trans′ zero n p z≤n _ = z≤n
|
||||
≤-trans′ (suc m) (suc n) (suc p) (s≤s m≤n) (s≤s n≤p) = s≤s (≤-trans′ m n p m≤n n≤p)
|
||||
\end{code}
|
||||
One might argue that this is clearer, since it shows us the forms of `m`, `n`,
|
||||
and `p`, or one might argue that the extra length obscures the essence of the
|
||||
|
|
@ -228,9 +228,9 @@ The third property to prove about comparison is that it is antisymmetric:
|
|||
for all naturals `m` and `n`, if both `m ≤ n` and `n ≤ m` hold, then
|
||||
`m ≡ n` holds.
|
||||
\begin{code}
|
||||
antisym≤ : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n
|
||||
antisym≤ z≤n z≤n = refl
|
||||
antisym≤ (s≤s m≤n) (s≤s n≤m) rewrite antisym≤ m≤n n≤m = refl
|
||||
≤-antisym : ∀ {m n : ℕ} → m ≤ n → n ≤ m → m ≡ n
|
||||
≤-antisym z≤n z≤n = refl
|
||||
≤-antisym (s≤s m≤n) (s≤s n≤m) rewrite ≤-antisym m≤n n≤m = refl
|
||||
\end{code}
|
||||
Again, the proof is by induction over the evidence that `m ≤ n`
|
||||
and `n ≤ m` hold, and so we have left `m` and `n` implicit.
|
||||
|
|
@ -243,7 +243,7 @@ of equivalance, that is, not the reflexivity of comparison.)
|
|||
In the inductive case, `m ≤ n` holds by `s≤s m≤n` and `n ≤ m` holds by
|
||||
`s≤s n≤m`, so it must be that `m` is `suc m′` and `n` is `suc n′`, for
|
||||
some `m′` and `n′`, where `m≤n` is evidence that `m′ ≤ n′` and `n≤m`
|
||||
is evidence that `n′ ≤ m′`. The inductive hypothesis `antisym≤ m≤n n≤m`
|
||||
is evidence that `n′ ≤ m′`. The inductive hypothesis `≤-antisym m≤n n≤m`
|
||||
establishes that `m′ ≡ n′`, and rewriting by this equation establishes
|
||||
that `m ≡ n` holds by reflexivity.
|
||||
|
||||
|
|
@ -254,12 +254,12 @@ the notion that given two propositions either one or the other holds.
|
|||
In Agda, we do so by declaring a suitable inductive type.
|
||||
\begin{code}
|
||||
data _⊎_ : Set → Set → Set where
|
||||
left : ∀ {A B : Set} → A → A ⊎ B
|
||||
right : ∀ {A B : Set} → B → A ⊎ B
|
||||
inj₁ : ∀ {A B : Set} → A → A ⊎ B
|
||||
inj₂ : ∀ {A B : Set} → B → A ⊎ B
|
||||
\end{code}
|
||||
This tells us that if `A` and `B` are propositions then `A ⊎ B` is
|
||||
also a proposition. Evidence that `A ⊎ B` holds is either of the form
|
||||
`left a`, where `a` is evidence that `A` holds, or `right b`, where
|
||||
`inj₁ a`, where `a` is evidence that `A` holds, or `inj₂ b`, where
|
||||
`b` is evidence that `B` holds.
|
||||
|
||||
We set the precedence of disjunction so that it binds less tightly
|
||||
|
|
@ -275,19 +275,19 @@ The fourth property to prove about comparison is that it is total:
|
|||
for any naturals `m` and `n` either `m ≤ n` or `n ≤ m`, or both if
|
||||
`m` and `n` are equal.
|
||||
\begin{code}
|
||||
total≤ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m
|
||||
total≤ zero n = left z≤n
|
||||
total≤ (suc m) zero = right z≤n
|
||||
total≤ (suc m) (suc n) with total≤ m n
|
||||
... | left m≤n = left (s≤s m≤n)
|
||||
... | right n≤m = right (s≤s n≤m)
|
||||
≤-total : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m
|
||||
≤-total zero n = inj₁ z≤n
|
||||
≤-total (suc m) zero = inj₂ z≤n
|
||||
≤-total (suc m) (suc n) with ≤-total m n
|
||||
... | inj₁ m≤n = inj₁ (s≤s m≤n)
|
||||
... | inj₂ n≤m = inj₂ (s≤s n≤m)
|
||||
\end{code}
|
||||
In this case the proof is by induction over both the first
|
||||
and second arguments. We perform a case analysis:
|
||||
|
||||
+ *First base case*: If the first argument is `zero` and the
|
||||
second argument is `n` then
|
||||
the left disjunct holds, with `z≤n` as evidence that `zero ≤ n`.
|
||||
the first disjunct holds, with `z≤n` as evidence that `zero ≤ n`.
|
||||
|
||||
+ *Second base case*: If the first argument is `suc m` and the
|
||||
second argument is `n` then the right disjunct holds, with
|
||||
|
|
@ -295,14 +295,14 @@ and second arguments. We perform a case analysis:
|
|||
|
||||
+ *Inductive case*: If the first argument is `suc m` and the
|
||||
second argument is `suc n`, then the inductive hypothesis
|
||||
`total≤ m n` establishes one of the following:
|
||||
`≤-total m n` establishes one of the following:
|
||||
|
||||
- The left disjunct of the inductive hypothesis holds with `m≤n` as
|
||||
evidence that `m ≤ n`, in which case the left disjunct of the
|
||||
- The first disjunct of the inductive hypothesis holds with `m≤n` as
|
||||
evidence that `m ≤ n`, in which case the first disjunct of the
|
||||
proposition holds with `s≤s m≤n` as evidence that `suc m ≤ suc n`.
|
||||
|
||||
- The right disjunct of the inductive hypothesis holds with `n≤m` as
|
||||
evidence that `n ≤ m`, in which case the right disjunct of the
|
||||
- The second disjunct of the inductive hypothesis holds with `n≤m` as
|
||||
evidence that `n ≤ m`, in which case the second disjunct of the
|
||||
proposition holds with `s≤s n≤m` as evidence that `suc n ≤ suc m`.
|
||||
|
||||
This is our first use of the `with` clause in Agda. The keyword
|
||||
|
|
@ -314,14 +314,14 @@ sign, and the right-hand side of the equation.
|
|||
Every use of `with` is equivalent to defining a helper function. For
|
||||
example, the definition above is equivalent to the following.
|
||||
\begin{code}
|
||||
total≤′ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m
|
||||
total≤′ zero n = left z≤n
|
||||
total≤′ (suc m) zero = right z≤n
|
||||
total≤′ (suc m) (suc n) = helper (total≤′ m n)
|
||||
≤-total′ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m
|
||||
≤-total′ zero n = inj₁ z≤n
|
||||
≤-total′ (suc m) zero = inj₂ z≤n
|
||||
≤-total′ (suc m) (suc n) = helper (≤-total′ m n)
|
||||
where
|
||||
helper : m ≤ n ⊎ n ≤ m → suc m ≤ suc n ⊎ suc n ≤ suc m
|
||||
helper (left m≤n) = left (s≤s m≤n)
|
||||
helper (right n≤m) = right (s≤s n≤m)
|
||||
helper (inj₁ m≤n) = inj₁ (s≤s m≤n)
|
||||
helper (inj₂ n≤m) = inj₂ (s≤s n≤m)
|
||||
\end{code}
|
||||
This is also our first use of a `where` clause in Agda. The keyword
|
||||
`where` is followed by one or more definitions, which must be
|
||||
|
|
@ -331,17 +331,17 @@ in the right-hand side of the preceding equation (in this case,
|
|||
preceding equation are in scope within the nested definition (in this
|
||||
case, `m` and `n`).
|
||||
|
||||
If both arguments are equal, then both the left and right disjuncts
|
||||
If both arguments are equal, then both the first and second disjuncts
|
||||
hold and we could return evidence of either. In the code above we
|
||||
always return the left disjunct, but there is a minor variant that
|
||||
always returns the right disjunct.
|
||||
always return the first disjunct, but there is a minor variant that
|
||||
always returns the second disjunct.
|
||||
\begin{code}
|
||||
total≤″ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m
|
||||
total≤″ m zero = right z≤n
|
||||
total≤″ zero (suc n) = left z≤n
|
||||
total≤″ (suc m) (suc n) with total≤″ m n
|
||||
... | left m≤n = left (s≤s m≤n)
|
||||
... | right n≤m = right (s≤s n≤m)
|
||||
≤-total″ : ∀ (m n : ℕ) → m ≤ n ⊎ n ≤ m
|
||||
≤-total″ m zero = inj₂ z≤n
|
||||
≤-total″ zero (suc n) = inj₁ z≤n
|
||||
≤-total″ (suc m) (suc n) with ≤-total″ m n
|
||||
... | inj₁ m≤n = inj₁ (s≤s m≤n)
|
||||
... | inj₂ n≤m = inj₂ (s≤s n≤m)
|
||||
\end{code}
|
||||
|
||||
|
||||
|
|
@ -360,11 +360,11 @@ Addition (precedence level 6) binds more tightly than comparison
|
|||
|
||||
The proof is straightforward using the techniques we have learned,
|
||||
and is best broken into three parts. First, we deal with the special
|
||||
case where the left arguments of addition are identical.
|
||||
case of showing addition is monotonic on the right.
|
||||
\begin{code}
|
||||
mono+≤l : ∀ (m p q : ℕ) → p ≤ q → m + p ≤ m + q
|
||||
mono+≤l zero p q p≤q = p≤q
|
||||
mono+≤l (suc m) p q p≤q = s≤s (mono+≤l m p q p≤q)
|
||||
+-monoʳ-≤ : ∀ (m p q : ℕ) → p ≤ q → m + p ≤ m + q
|
||||
+-monoʳ-≤ zero p q p≤q = p≤q
|
||||
+-monoʳ-≤ (suc m) p q p≤q = s≤s (+-monoʳ-≤ m p q p≤q)
|
||||
\end{code}
|
||||
The proof is by induction on the first argument.
|
||||
|
||||
|
|
@ -374,27 +374,27 @@ The proof is by induction on the first argument.
|
|||
|
||||
+ *Inductive case*: The first argument is `suc m`, in which case
|
||||
`suc m + p ≤ suc m + q` simplifies to `suc (m + p) ≤ suc (m + q)`.
|
||||
The inductive hypothesis `mono+≤₁ {m} p≤q` establishes that
|
||||
The inductive hypothesis `+-monoʳ-≤ m p q p≤q` establishes that
|
||||
`m + p ≤ m + q`, from which the desired conclusion follows
|
||||
by an application of `s≤s`.
|
||||
|
||||
Second, we deal with the special case where the right arguments
|
||||
of the addition are identical. This follows from the previous
|
||||
Second, we deal with the special case of showing addition is
|
||||
monotonic on the left. This follows from the previous
|
||||
result and the commutativity of addition.
|
||||
\begin{code}
|
||||
mono+≤r : ∀ (m n p : ℕ) → m ≤ n → m + p ≤ n + p
|
||||
mono+≤r m n p m≤n rewrite com+ m p | com+ n p = mono+≤l p m n m≤n
|
||||
+-monoˡ-≤ : ∀ (m n p : ℕ) → m ≤ n → m + p ≤ n + p
|
||||
+-monoˡ-≤ m n p m≤n rewrite +-comm m p | +-comm n p = +-monoˡ-≤ p m n m≤n
|
||||
\end{code}
|
||||
Rewriting by `com+ m p` and `com+ n p` converts `m + p ≤ n + p` into
|
||||
`p + m ≤ p + n`, which is proved by invoking `mono+≤left p m n m≤n`.
|
||||
Rewriting by `+-comm m p` and `+-comm n p` converts `m + p ≤ n + p` into
|
||||
`p + m ≤ p + n`, which is proved by invoking `+-monoʳ-≤ p m n m≤n`.
|
||||
|
||||
Third, we combine the two previous results.
|
||||
\begin{code}
|
||||
mono+≤ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m + p ≤ n + q
|
||||
mono+≤ m n p q m≤n p≤q = trans≤ (mono+≤r m n p m≤n) (mono+≤l n p q p≤q)
|
||||
mono+≤ m n p q m≤n p≤q = ≤-trans (+-monoˡ-≤ m n p m≤n) (+-monoʳ-≤ n p q p≤q)
|
||||
\end{code}
|
||||
Invoking `mono+≤r m n p m≤n` proves `m + p ≤ n + p` and invoking
|
||||
`mono+≤l n p q p≤q` proves `n + p ≤ n + q`, and combining these with
|
||||
Invoking `+-monoˡ-≤ m n p m≤n` proves `m + p ≤ n + p` and invoking
|
||||
`+-monoʳ-≤ n p q p≤q` proves `n + p ≤ n + q`, and combining these with
|
||||
transitivity proves `m + p ≤ n + q`, as was to be shown.
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue