\nonstopmode \documentclass{scrartcl} % KOMA-Script article \usepackage{amsmath} %include agda.fmt %% dot patterns: %format . = "\mathord{.\!\!}" \DeclareUnicodeCharacter{9675}{\ensuremath{\circ}} \DeclareUnicodeCharacter{8744}{\ensuremath{\vee}} \newcommand{\textlambda}{\ensuremath{\lambda}} \newcommand{\textSigma}{\ensuremath{\Sigma}} \newcommand{\hide}[1]{} \title{Agda: Equality} \author{Andreas Abel} \date{2 July 2012} \begin{document} \maketitle \hide{ \begin{code} module Equality where \end{code} } \section{Definitional Equality} Agda has an internal notion of program equality. In essence, two programs are equal if they compute the same value. For instance, |(λ x → x + y) 5| and |5 + y| are equal since the second arises if you compute the value of the first expression. When you define a function \begin{code} open import Data.Bool hiding (_∨_) _∨_ : Bool → Bool → Bool true ∨ y = true false ∨ y = y \end{code} then you add the defining equations to Agda's internal equality. This internal equality is usually called \emph{definitional equality}. But careful, not every equation you write holds literally in Agda! Consider the following, alternative definition of disjunction: \begin{spec} _∨_ : Bool → Bool → Bool false ∨ false = false x ∨ y = true \end{spec} Only the first equation holds as such, and this is actually good, otherwise we would also have |false ∨ false = true| as instance of the second equation. In this case, the second equation does not hold because it overlaps with the first equation. Internally, it is expanded into three equations, which hold definitionally. \begin{spec} false ∨ true = true true ∨ false = true true ∨ true = true \end{spec} Consider yet another version of disjunction: \begin{spec} _∨_ : Bool → Bool → Bool false ∨ false = false true ∨ false = true x ∨ true = true \end{spec} These clauses are not overlapping, yet still the third equation does not hold definitionally. We can test it by normalizing the following expression: \begin{code} test∨ : Bool → Bool test∨ = λ x → x ∨ true \end{code} If type \verb|C-c C-n test∨| we do not get |λ x → true| as we might expect, but |λ x → x ∨ true|. Internally, Agda has split the third clause |x ∨ true = true| into the two clauses: \begin{spec} false ∨ true = true true ∨ true = true \end{spec} Because the first clause did not have a variable as first argument but the constructor |false|, Agda splits the first argument of all clauses into the two cases |false| and |true|. To get the correct behavior, we need to change the order of the clauses. \begin{spec} _∨_ : Bool → Bool → Bool x ∨ true = true false ∨ false = false true ∨ false = true \end{spec} Now |test∨| evaluates to |λ x → true|. \section{Propositional Equality} If we want to \emph{prove} that two programs are equal, we cannot directly use the definitional equality. A proof is itself a program with a type, and in this the type should express that two things are equal. This type can be defined in Agda; to use it, import |Relation.Binary.PropositionalEquality|. Propositional equality as defined in the standard library is universe polymorphic; we start with a simpler version. \begin{code} module Level0Equality (A : Set) where data _≡_ : A → A → Set where refl : (a : A) → a ≡ a \end{code} We are defining |_≡_|, the least binary relation on |A| such that |a ≡ a| for all |a : A|. If we have two \emph{definitionally} equal terms |a| and |b|, then |refl a| and |refl b| are both proofs of \emph{(propositional)} equality of |a| and |b|. This is because internally, Agda does not distinguish between definitionally equal terms. Propositional equality is an \emph{equivalence relation}, meaning that it is reflexive (by definition), symmetric (|sym|), and transitive (|trans|). Symmetry and transitivity can be proven by pattern matching. \begin{code} sym : ∀ x y → x ≡ y → y ≡ x sym .a .a (refl a) = refl a \end{code} We match on |x ≡ y|, and since |refl| is the only constructor of this data type, |refl a| for some variable |a| is only matching pattern. By this in turn forces |x ≡ y| to be definitionally equal to |a ≡ a| meaning that both |x| and |y| must be definitionally equal to |a|. Such a forced coincidence is expressed in Agda via a \emph{dot pattern} (aka \emph{inaccessible} pattern). If instead of a pattern, we write |.expression|, we mean that during the match, the value at this position is forced to be |expression|, and an actual match is not necessary. Transitivity is likewise easy, using dependent pattern matching: \begin{code} trans : ∀ x y z → x ≡ y → y ≡ z → x ≡ z trans .a .a .a (refl .a) (refl a)= refl a \end{code} A central concept of equality is \emph{substitutivity}: in any proposition (type), we can replace a term with a propositionally equal one, without changing the meaning of the proposition (type). \begin{code} subst : ∀ x y → x ≡ y → ∀ (P : A → Set) → P x → P y subst .a .a (refl a) P Pa = Pa \end{code} If |P x| holds and |x ≡ y| then |P y| also holds. Leibniz took substitutivity as the \emph{definition} of equality: If two objects |x| and |y| are indistinguishable by any observation |P|, then they are equal. Thus, |x ≡ y = ∀ (P : A → Set) → P x → P y| would be an alternative definition of propositional equality. It is equivalent to the inductive definition, since we can prove the opposite of |subst|: \begin{code} leibniz : ∀ x y → (∀ (P : A → Set) → P x → P y) → x ≡ y leibniz x y H = H (_≡_ x) (refl x) \end{code} The proof |H| that |x| and |y| are Leibniz-equal is instantiated to the predicate |P a = (x ≡ a)|. Then we supply a proof |refl x| of |P x| and obtain the desired proof of |P y = (x ≡ y)|. \section{The Standard Definition of Propositional Equality} If we import |Relation.Binary.PropositionalEquality|, we get the definition and standard tools to work with equality. \begin{code} open import Relation.Binary.PropositionalEquality \end{code} The definition in the standard library is universe polymorphic. It is hidden in a |.Core| module---such modules do not need to be imported explicitly. \begin{spec} module Relation.Binary.Core where data _≡_ {a} {A : Set a} (x : A) : A → Set a where refl : x ≡ x \end{spec} Further, |refl| does not require an argument. The properties of equality are specified with more hidden arguments than we did in the last section. \begin{spec} module Relation.Binary.PropositionalEquality.Core where sym : ∀ {a} {A : Set a} → Symmetric (_≡_ {A = A}) sym refl = refl trans : ∀ {a} {A : Set a} → Transitive (_≡_ {A = A}) trans refl eq = eq subst : ∀ {a p} {A : Set a} → Substitutive (_≡_ {A = A}) p subst P refl p = p \end{spec} Note the different argument order in |subst|. An important consequence of substitutivity is \emph{congruence}. \begin{spec} module Relation.Binary.PropositionalEquality where cong : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x y} → x ≡ y → f x ≡ f y cong f refl = refl \end{spec} It says that any function |f| respects propositional equality, i.e., yields propositionally equal results if applied to propositionally equal arguments. We use |cong| if we want to apply equality in a subterm. % \begin{spec} % data _≡_ {A : Set}(a : A) : A → Set where % refl : a ≡ a % \end{spec} % The type of |_≡_| is |{A : Set} → A → A → Set|, thus, % \begin{spec} % _≡_ {A} : A → A → Set % \end{spec} % which means that |_≡_ {A}| is a binary relation on |A|. \section{An Example} Let us prove the associativity of list concatenation! \begin{code} open import Data.List \end{code} \begin{spec} ++-assoc : ∀ {a}{A : Set a}(xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) \end{spec} We start with the following universal template that we load into Agda (\verb|C-c C-l|): \begin{spec} ++-assoc xs ys zs = ? \end{spec} What is the best way to proceed? Append |_++_| is defined by cases on the first argument: \begin{spec} _++_ : ∀ {a} {A : Set a} → List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) \end{spec} A good proof strategy is to case on the same argument as the involved recursive function does, because then definitional equality triggers simplifications. So, let us case (\verb|C-c C-c|) on variable |xs|. \begin{spec} ++-assoc [] ys zs = { }0 ++-assoc (x ∷ xs) ys zs = { }1 \end{spec} The first goal |?0 : ([] ++ ys) ++ zs ≡ [] ++ ys ++ zs| is definitionally equal to |ys ++ zs ≡ ys ++ zs|; this can be seen by pressing \verb|C-C C-,| in hole 0. The proof is simply |refl|. The second goal simplifies to |x ∷ ((xs ++ ys) ++ zs) ≡ x ∷ (xs ++ (ys ++ zs))| which we can prove by applying the induction hypothesis in subterm |l| of |x ∷ l|. \begin{spec} ++-assoc [] ys zs = refl ++-assoc (x ∷ xs) ys zs = cong (λ l → x ∷ l) (++-assoc xs ys zs) \end{spec} The induction hypothesis is just a recursive call. Since the first argument is decreasing, the termination checker accepts this call. In essence, we have proven the associativity of append by induction on the first argument. Admittedly, this proof is not very readable. The proposition we are currently manipulating is not visible. One has to have trained Agda-eyes to recognize the argument. We can make the proof more verbose by using the equation chains of the standard library. \section{Equation Chains} |Relation.Binary.PropositionalEquality| provides a module |≡-Reasoning| that provides nice mixfix syntax for writing down a chain of equalities: \begin{code} open ≡-Reasoning ++-assoc : ∀ {a}{A : Set a}(xs ys zs : List A) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) ++-assoc [] ys zs = begin ([] ++ ys) ++ zs ≡⟨ refl ⟩ ys ++ zs ≡⟨ refl ⟩ [] ++ (ys ++ zs) ∎ \end{code} We start our chain with |begin| and end it with |∎| (enter \verb|\qed|). Each equality sign is decorated with a justification (proof term) of that equation; in this case all proofs are just |refl| (enter \verb|\equiv\< refl \>|, because all these equations hold by definition. In the step case of our induction, we make also each single transformation step obvious. \begin{code} ++-assoc (x ∷ xs) ys zs = begin ((x ∷ xs) ++ ys) ++ zs ≡⟨ refl ⟩ (x ∷ (xs ++ ys)) ++ zs ≡⟨ refl ⟩ x ∷ ((xs ++ ys) ++ zs) ≡⟨ cong (_∷_ x) (++-assoc xs ys zs) ⟩ x ∷ (xs ++ (ys ++ zs)) ≡⟨ refl ⟩ (x ∷ xs) ++ (ys ++ zs) ∎ \end{code} Now our proof is similar to a detailed pen and paper proof! While easier to read, it may be a bit harder to maintain due to its verbosity. \paragraph*{Acknowledgements} This document has been generated with lhs2TeX by Ralf Hinze and Andres L\"oh. A great tool! \end{document}