diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 6ab85b7c..704dbf0b 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -456,6 +456,9 @@ definition to equivalent inference rules for judgements about equality. ------------ zero + n = n + m : ℕ + n : ℕ + p : ℕ m + n = p ------------------- (suc m) + n = suc p diff --git a/src/Properties.lagda b/src/Properties.lagda index aca3a909..0317e8d3 100644 --- a/src/Properties.lagda +++ b/src/Properties.lagda @@ -21,6 +21,7 @@ everything in the previous chapter is also found in the library module We also require propositional equality. --> \begin{code} +open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_) open import Relation.Binary.PropositionalEquality using (_≡_; refl) \end{code} @@ -72,15 +73,9 @@ The answer is yes! We can prove a property holds for all naturals using ## Proof by induction -Recall the definition of natural numbers. -\begin{code} -data ℕ : Set where - zero : ℕ - suc : ℕ → ℕ -\end{code} -This tells us that `zero` is a natural---the *base case*---and that if -`m` is a natural then `suc m` is also a natural---the *inductive -case*. +Recall the definition of natural numbers consists of a *base case* +which tells us that `zero` is a natural, and an *inductive case* +which tells us that if `m` is a natural then `suc m` is also a natural. Proofs by induction follow the structure of this definition. To prove a property of natural numbers by induction, we need prove two cases. @@ -173,12 +168,10 @@ we must show to hold, become: In the inference rules, `n` and `p` are any arbitary natural numbers, so when we are done with the proof we know it holds for any `n` and `p` as well as any `m`. -Recall the definition of addition. -\begin{code} -_+_ : ℕ → ℕ → ℕ -zero + n = n -- (i) -(suc m) + n = suc (m + n) -- (ii) -\end{code} +Recall the definition of addition has two clauses. + + zero + n = n -- (i) + (suc m) + n = suc (m + n) -- (ii) For the base case, we must show: @@ -561,10 +554,9 @@ 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 -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 - +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 \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 diff --git a/src/Relations.lagda b/src/Relations.lagda new file mode 100644 index 00000000..7097cd61 --- /dev/null +++ b/src/Relations.lagda @@ -0,0 +1,158 @@ +--- +title : "Relations: Inductive Definition of Relations" +layout : page +permalink : /Relations +--- + +After having defined operations such as addition and multiplication, +the next step is to define relations, such as *less than or equal*. + +## Imports + +\begin{code} +open import Naturals using (ℕ; zero; suc; _+_; _*_; _∸_) +open import Properties using (com+; com+zero; com+suc) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) +\end{code} + +## Defining relations + +The relation *less than or equal* has an infinite number of +instances. Here are just a few of them: + + 0 ≤ 0 0 ≤ 1 0 ≤ 2 0 ≤ 3 ... + 1 ≤ 1 1 ≤ 2 1 ≤ 3 ... + 2 ≤ 2 2 ≤ 3 ... + 3 ≤ 3 ... + ... + +And yet, we can write a finite definition that encompasses +all of these instances in just a few lines. Here is the +definition as a pair of inference rules: + + z≤n -------- + zero ≤ n + + m ≤ n + s≤s ------------- + suc m ≤ suc n + +And here is the definition in Agda: +\begin{code} +data _≤_ : ℕ → ℕ → Set where + z≤n : ∀ {m : ℕ} → zero ≤ m + s≤s : ∀ {m n : ℕ} → m ≤ n → suc m ≤ suc n +\end{code} +Here `z≤n` and `s≤s` (with no spaces) are constructor names, +while `m ≤ m`, and `m ≤ n` and `suc m ≤ suc n` (with spaces) +are propositions. + +Both definitions above tell us the same two things: + ++ *Base case*: for all naturals `n`, the proposition `zero ≤ n` holds ++ *Inductive case*: for all naturals `m` and `n`, if the proposition + `m ≤ n` holds, then the proposition `suc m ≤ suc n` holds. + +In fact, they each give us a bit more detail: + ++ *Base case*: for all naturals `n`, the constructor `z≤n` + produces evidence that `zero ≤ n` holds. ++ *Inductive case*: for all naturals `m` and `n`, the constructor + `s≤s` takes evidence that `m ≤ n` holds into evidence that + `suc m ≤ suc n` holds. + +Here we have used the word *evidence* as interchangeable with the +word *proof*. We will tend to say *evidence* when we want to stress +that proofs are just terms in Agda. + +For example, here in inference rule notation is the proof that +`2 ≤ 4`. + + z≤n ----- + 0 ≤ 2 + s≤s ------- + 1 ≤ 3 + s≤s --------- + 2 ≤ 4 + +And here is the corresponding Agda proof. +\begin{code} +ex₁ : 2 ≤ 4 +ex₁ = s≤s (s≤s z≤n) +\end{code} + +## Implicit arguments + +In the Agda definition, the two lines defining the constructors +use `∀`, very similar to our use of `∀` in propositions such as: + + com+ : ∀ (m n : ℕ) → m + n ≡ n + m + +However, here the declarations are surrounded by curly braces `{ }` +rather than parentheses `( )`. This means that the arguments are +*implicit* and need not be written explicitly. Thus, we would write, +for instance, `com+ m n` for the proof that `m + n ≡ n + m`, but +here will write `z≤n` for the proof that `m ≤ m`, leaving the `m` implicit, +or if `m≤n` is evidence that `m ≤ n`, we write write `s≤s m≤n` for the +evidence that `suc m ≤ suc n`, leaving both `m` and `n` implicit. + +It is possible to provide implicit arguments explicitly if we wish. +For instance, here is the Agda proof that `2 ≤ 4` repeated, with the +implicit arguments made explicit. +\begin{code} +ex₂ : 2 ≤ 4 +ex₂ = s≤s {1} {3} (s≤s {0} {2} (z≤n {2})) +\end{code} + +## Proving properties of inductive definitions. + +\begin{code} +infix 4 _≤_ + +refl≤ : ∀ (n : ℕ) → n ≤ n +refl≤ zero = z≤n +refl≤ (suc n) = s≤s (refl≤ n) + +trans≤ : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p +trans≤ z≤n n≤p = z≤n +trans≤ (s≤s m≤n) (s≤s n≤p) = s≤s (trans≤ m≤n n≤p) + +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 + +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) + +mono+≤′ : ∀ (m n p : ℕ) → m ≤ n → m + p ≤ n + p +mono+≤′ m n p m≤n rewrite com+ m p | com+ n p = mono+≤ p m n m≤n + +mono+≤″ : ∀ (m n p q : ℕ) → m ≤ n → p ≤ q → m + p ≤ n + q +mono+≤″ m n p q m≤n p≤q = trans≤ (mono+≤′ m n p m≤n) (mono+≤ n p q p≤q) + +inverse+∸≤ : ∀ (m n : ℕ) → m ≤ n → (n ∸ m) + m ≡ n +inverse+∸≤ zero n z≤n rewrite com+zero n = refl +inverse+∸≤ (suc m) (suc n) (s≤s m≤n) + rewrite com+suc m (n ∸ m) | inverse+∸≤ m n m≤n = refl + +data _<_ : ℕ → ℕ → Set where + z