module lecture-notes-Relations where
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; cong; cong₂)
Recall that a predicate is a statement involving a variable that can
be true or false. In math, a predicate P is often represented as a
Boolean-valued function, so P x ≡ true if the statement is true of
the object x and P x ≡ false if it is false.
In Agda, we often uses datatypes to represent predicates. We define a
datatype named P that is parameterized over the appropriate type,
the ℕ below. We then say that P x is true if we can
construct an object of type P x.
data Even : ℕ → Set where
even-0 : Even 0
even-+2 : (n : ℕ) → Even n → Even (2 + n)
The following constructs a value of type Even 2, so it’s true that
2 is even.
_ : Even 2
_ = even-+2 0 even-0
Similarly for the number 4.
_ : Even 4
_ = even-+2 2 (even-+2 0 even-0)
Taking this process to its logical conclusion, we prove that every
number of the form 2 * n, or equivalently n + n, is even.
We’ll do this by defining a recursive function even-dub
that takes a number n and produces an object of type
Even (n + n).
even-dub : (n : ℕ) → Even (n + n)
even-dub zero = even-0
even-dub (suc n) rewrite +-comm n (suc n) =
let IH : Even (n + n)
IH = even-dub n in
even-+2 (n + n) IH
For the base case, we construct an object of type Even (0 + 0),
that is Even 0, using even-0.
For the induction step, we need to construct an object of type Even
(suc (n + suc n)). We rewrite using the equation sn+sn≡n+n+2 to
transform this goal to Even ((n + n) + 2). By the induction
hypothesis (i.e. recursive call to even-dub), we have Even (n +
n), so we conclude by applying the constructor even-+2.
If we know a number is Even, then it must have been generated by one
of the two rules. We can use the pattern matching associated with
function definitions to reason backwards about the rules. For
example, if Even m and m is not zero, then there is a number n
two less-than m that is also even.
open import Relation.Binary.PropositionalEquality using (_≢_)
open import Data.Empty using (⊥-elim)
inv-Even : (n m : ℕ) → Even m → m ≢ 0 → suc (suc n) ≡ m → Even n
inv-Even n .0 even-0 m≢0 n+2≡m = ⊥-elim (m≢0 refl)
inv-Even n .(suc (suc n')) (even-+2 n' even-m) m≢0 refl = even-m
In the case for even-0, we have a contradiction: m ≡ 0 and m ≢ 0.
We can ⊥-elim to prove anything from a proof of false, written ⊥.
Also, recall that m ≢ 0 is short for ¬ (m ≡ 0) and
negation is shorthand for implication to false, in this case
m ≡ 0 → ⊥.
In the case for even-+2 we know that m is n' + 2,
so n + 2 ≡ n' + 2 and therefore n = n' by
+-cancelʳ-≡. We have even-m : Even n' and
the goal is Even n, so we conclude by rewriting by
n = n' and then using even-m.
Like predicates, relations can be represented in Agda with data types, they just have more parameters.
One of the most important relations in Number Theory is the divides
(evenly) relation. We say that m divides n if some number of
copies of m can be concatenated (added) to form n.
data _div_ : ℕ → ℕ → Set where
div-refl : (m : ℕ) → m ≢ 0 → m div m
div-step : (n m : ℕ) → m div n → m div (m + n)
For example, 3 div 3, 3 div 6, and 3 div 6.
3-div-3 : 3 div 3
3-div-3 = div-refl 3 λ ()
3-div-6 : 3 div 6
3-div-6 = div-step 3 3 3-div-3
3-div-9 : 3 div 9
3-div-9 = div-step 6 3 3-div-6
A common property of relations is transitivity. Indeed, the div
relation is transitive. To prove this we need the following standard
fact about divides and addition.
div-+ : ∀ l m n → l div m → l div n → l div (m + n)
div-+ l .l n (div-refl .l l≢0) ln = div-step n l ln
div-+ l .(l + m) n (div-step m .l lm) ln
rewrite +-assoc l m n =
let IH = div-+ l m n lm ln in
div-step (m + n) l IH
In the case for div-refl, we have m ≡ l so we need to
prove that l div (l + n), which we do directly with div-step.
In the case for div-step, we need to prove that l div ((l + m) + n),
which we re-associate to l div (l + (m + n)).
The induction hypothesis gives us l div (m + n),
so we conclude by applying div-step.
We prove that div is transitive by induction on the derivation
of m div n.
div-trans : ∀ l m n → l div m → m div n → l div n
div-trans l m .m lm (div-refl .m m≢0) = lm
div-trans l m .(m + n) lm (div-step n .m mn) =
let IH:ln = div-trans l m n lm mn in
div-+ l m n lm IH:ln
In the case for div-refl, we have n ≡ m
so we need to prove l div m, which we already know.
In the case for div-step, we need to prove
that l div (m + n)
and the induction hypothesis for m div n gives us
l div n. So using this with the assumption that
l div m, we apply div-+ to conclude that
l div (m + n).