Last note was quite chill introduction to how we change the way looking at programs and making connections between programs and proofs and how to define inductive structure (using inductive datatype). This time, I’ll show more insightful things about how we represent proofs using depently-typed languages such as Agda. It will tell you how to do constructive proof.
Dependent Type is a type system where types depends on terms. The very obvious feature of dependent type is that you can see value (generally speaking) inhabitate on a type. For instance, a common way we define an list is
data List a = Empty | Cons a (List a)
and we can see the polymorphic data type allows you to make a type of List depends on another type a. From a type signature, say $xs \colon List Int$. what we only know is that xs is a List of Integers. But in dependent type, we can do more: including the length of the List in its type.
data List (A : Set) : ℕ -> Set where
[] : List A zero
_::_ : {l : ℕ} -> A -> List A l -> List A (suc l)
The first case, [], which is the empty list, has the type List A zero, and the natural number in the type denotes that the length of the list is zero. As for the second case, which corresponds to some element concat to the list, we can see that by accepting an element of type A and adding it to a list with type List A l, which stands for the type of a list of elements of type A with the length l, we get a list with type List A (suc l), having one more element than the given one. We call this representation of dependent type List is parametrized by a set A and indexed by natural numbers. Two List have the same type if and only if they are parametrized by the same set and they have the same natural number index.
The advantages of using this type system is that when we pattern match on a List, we can also get the information about its length; we can also omitt some safety checking cases (like poping an element out of a list) since we can ensure the security of our operations on a language level.
The evidence of equality comes from what we call Unification. When the type checker checks through the program, it will unify two data when it figures out that two terms represent the same thing (or have the same normal form).
data _≡_ {A : Set} (x : A) -> A -> Set where
refl : x ≡ x
the set , $\equiv$, is parametrized by a set A, where A can be inferred by the type checker so we put it in {} which carries implicit arguments, and a parameter x, and is indexed by an element of set A. We have only one case of equality which is refl, the short for reflexivity. We put x on both LHS and RHS, this will lead the type checker to perform unification while matching some terms against the pattern refl, since when constructing the type $\equiv$, there is no evidence showing that the parameter (x) and the index are the same thing. But when we match something against the pattern, the RHS becomes x too, so in this case, the type checker will check whether x, after big-step evaluation to a normal form (or a canonical form), is the same as the index (also after a big-step evaluation). If they are the same, then the term represented by x and the term of index will be interchangeable in future computations with the same context.
Let’s continue what we were doing about $\mathbb{N}$. Let me put the definition from Previous note here.
data ℕ : Set where
Z : ℕ
S : ℕ -> ℕ
where Z stands for the beginning of natural numbers zero, and S stands for how we inductively construct the next natural number of a given one.
Recall the operation “+” on the set:
_+_ : ℕ -> ℕ -> ℕ
zero + n = n
suc m + n = suc (m + n)
Which is pretty intuitive: zero plus anything yields itself, whereas a non-zero number $suc m$ plus another number $n$ is the successor of $m$ and $n$, denoted by $suc (m + n)$.
With the definition of $\mathbb{N}$ and the evaluation rule of $+$, we can do some reasoning about equality and plus on natural numbers.
Let’s take a look at how to prove that plus is associative; that is, $\forall n,m,p \in \mathbb{N}\ n + (m + p)\equiv (n + m) + p$, whose informal proof has been shown in the previous Note. Here we formalize it into our proof assistant Agda.
-- Recall that _≡_ accepts two values and yields a type that
-- will cause type checker to perform unification and
-- take the expressions on both sides as the same expr.
+-assoc : (m n p : ℕ) -> m + (n + p) ≡ (n + m) + p
First we do induction on $m$. To achieve this, we need to first perform case analysis and then include the induction hypothesis. As noted before, pattern matching is a sort of case analysis. Therefore, we can split the cases of $m$ to do pattern matching.
+-assoc : (m n p : ℕ) -> m + (n + p) ≡ (m + n) + p
+-assoc zero n p = ?
+-assoc (suc m₀) n p = ?
After we split out the patterns, in each case during type check, Agda will substitute the actual value into the type signature and then reduce the expression as far as possible. For example, in the first case, $m$ will be substituted by zero and the target (goal) of our proof is to construct a value that has the type $zero + (n + p) \equiv (zero + n) + p$. Since Adga reduces this expression to a normal form, the type will become $(n + p) \equiv n + p$ accodring to the definition of $+$. Here we can see that this reaches the pattern of $refl$, so we can directly get:
-- Base case
+-assoc zero n p = refl
In the inductive case, $m$ is substituted by $suc\ m_0$. Then after exhaustive reduction, the type of the righ-hand-side we are going to construct becomes $suc (m_0 + (n + p)) \equiv suc (m_0 + n + p)$. The induction hypothesis tells us that $m_0 + (n + p) \equiv (m_0 + n) + p$. How do we include the induction hypothesis? As noted in the previous post, recursion <-> induction. So our induction hypothesis is:
-- IH
+-assoc m₀ n p
which will yields the equality $m_0 + (n + p) \equiv (m_0 + n) + p$.
Applying the hypothesis and rewriting (substitue all occurence of LHS to RHS), our proof is complete.
+-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 (suc m₀) n p = cong suc (+-assoc m₀ n p)
-- Congruence
cong : ∀{A B : Set}{x y : A} -> (f : A -> B) -> x ≡ y -> (f x) ≡ (f y)
Side note: we can also apply the proof of equality ($m_0 + (n + p) \equiv (m_0 + n) + p$) to the congruence property of $suc$ (because after a total reduction, the goal becomes $suc (m_0 + (n + p)) \equiv suc (m_0 + n + p)$).
(Work in-progress…)