Last week, we started a new blog series to introduce you to creating constructive and non-constructive proofs in Agda.
In our previous post, we took a look on logic in itself, we considered classical and intuitionistic logical calculi. It will come in handy today when we start tackling theorem proving in Agda based on a constructive logical framework.
In this article, we will introduce the reader to dependently typed programming and theorem proving in Agda. We will compare our examples of Agda code with their Haskell counterparts. After that, we will consider an example use of Agda in the formalisation of algebra.
General words on Agda
Agda is a dependently typed functional programming language based on a variant of Martin-Löf type theory. This type theory is a constructive proof-theoretic formal system, so Agda doesn’t have the default features for writing classical logic based proofs in contrast to HOL or Isabelle.
Agda has a Haskell-like syntax and a much richer type system (but we’re working on bringing Haskell to the same level), so we may use Agda as a proof-assistant based on the propositions-as-types paradigm. In other words, Agda is a programming language that allows providing formal proofs within constructive mathematics.
In this section, we will make a brief introduction to the syntax and possibilities of Agda.
See here for a more detailed introduction.
Basic stuff
Types in Agda
Datatypes
Datatypes in Agda are introduced as generalized algebraic datatypes (GADT):
Trivial example: a datatype of writers and a datatype of their works.
data Writers : Set where
Wilde Shelley Byron Sartre Camus : Writers
data Literature : Set where
DorianGrey Alastor ChildeHarold LaNausée L’Étranger : Literature
The typical example is a datatype of unary natural numbers:
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
In Haskell we define these types as follows:
data Writers =
Wilde
| Shelley
| Byron
| Sartre
| Camus
data Literature =
DorianGrey
| Alastor
| ChildeHarold
| LaNausée
| L’Étranger
data ℕ = Zero | Suc ℕ
These datatypes are so-called simple datatypes.
Parameterized and indexed datatypes
See to read about parameterized and indexed datatypes in more detail.
A parameterized datatype is a datatype that depends on some parameter that should remain the same in the types of constructors. For instance, List is a datatype parameterized over a type A.
data List (A : Set) : Set where
Nil : List A
Cons : A → List A → List A
Datatypes also can have indexes that could differ from constructor to constructor in contrast to parameters. These datatypes are so-called datatype families. Example:
data Vec (A : Set) : ℕ → Set where
Nil : Vec A zero
Cons : {n : ℕ} → A → Vec A n → Vec A (suc n)
Vec (vector) is a datatype that is applied to another type A and a natural number n. We also say that Vec is parameterized by A and indexed by ℕ. Nil is an empty vector. Cons is a constructor adding a new element to a given vector increasing the length counter. Here n is an implicit argument of the constructor. Cons is also an example of a dependent function, as will be seen below.
In Haskell, we would have the following GADT via DataKinds, PolyKinds and GADTs extensions:
{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}
import Data.Kind (Type)
data Vec :: Type -> ℕ -> Type where
Nil :: Vec a 'Zero
Cons :: a -> Vec a n -> Vec a ('Succ n)
Another example: Fin is a type that describes finite types, in other words, types of finite cardinality. Informally, Fin is a type of finite sets:
data Fin : ℕ → Set where
zero : {n : ℕ} → Fin (suc n)
suc : {n : ℕ} → Fin n → Fin (suc n)
Fin is a datatype indexed by a natural number. zero reflects an empty set which is an element of any finite set. suc is a constructor that applies the finite set i and yields a new finite set, which is a larger than i on one element.
In Haskell, we define Fin using DataKinds and KindSignatures extensions as with vectors above:
{-# LANGUAGE DataKinds, PolyKinds, GADTs #-}
import Data.Kind (Type)
data Fin :: Nat -> Type where
Fzero :: forall (n :: ℕ). Fin ('Succ n)
Fsucc :: forall n. Fin n -> Fin ('Succ n)
Note that, datatypes Vec and Fin implemented in Agda are also examples of dependent types, these types depend on values (in particular, on natural numbers), not only on types.
On the other hand, their counterparts in Haskell are not dependent types in a strict sense, because forall (n :: ℕ) in Haskell does not introduce a value, therefore Fin does not depend on any values.
See here for an introduction to type level programming in Haskell.
Functions
Functions in Agda are arranged similarly to Haskell, using pattern matching:
bookToWriter : Literature → Writers
bookToWriter DorianGrey = Wilde
bookToWriter Alastor = Shelley
bookToWriter ChildeHarold = Byron
bookToWriter LaNausée = Sartre
bookToWriter L’Étranger = Camus
We will discuss dependent functions in more detail. A dependent function is a function that takes a term a of type A and returns some result of type B, where a may appear in B. We consider a simple example, where a is a type itself.
const₁ : (A B : Set) → A → B → A
const₁ A B x y = x
Here types A and B are explicit arguments. If we don’t need to mention these types explicitly, we may take them implicitly:
const₂ : {A B : Set} → A → B → A
const₂ x y = x
We may compare this function in Agda with a similar function implemented in Haskell with the help of the RankNTypes extension that allows writing the universal quantifier on types explicitly:
{-# LANGUAGE RankNTypes #-}
const₁ :: forall a b. a -> b -> a
const₁ x y = x
We introduce the following datatypes to consider the next example:
data Ireland : Set where
Dublin : Ireland
data England : Set where
London : England
data France : Set where
Paris : France
After that, we construct a function that returns some country datatype for a given writer.
WriterToCountry : Writers → Set
WriterToCountry Wilde = Ireland
WriterToCountry Shelley = England
WriterToCountry Byron = England
WriterToCountry Sartre = France
WriterToCountry Camus = France
WriterToCity : (w : Writers) → WriterToCountry w
WriterToCity Wilde = Dublin
WriterToCity Shelley = London
WriterToCity Byron = London
WriterToCity Sartre = Paris
WriterToCity Camus = Paris
WriterToCity is an example of a dependent function, because the type of the result depends on the argument. The type of a dependent function is the so-called -type. More generally, suppose we have some function P: A → Set, then -type is a type of the function that assigns to every term t : A some object of type P t. In Agda notation, we write this type as (t : A) → P t for some {A : Set} {P : A → Set} in context.
Logically -type encodes intuitionistic universal quantifier. In other words, P is a predicate and some function of a type (t : A) → P t is a proof that for each t : A the property P has established.
In Haskell, we don’t have dependent quantification at term level, but we have it at type level. Therefore, we implement comparable functions as closed type families. Similarly, we promote values of type Writers into the type level via DataKinds in both cases:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
data Ireland = Dublin
data France = Paris
data England = London
type family WriterToCountry (a :: Writers) :: Type where
WriterToCountry 'Wilde = Ireland
WriterToCountry 'Shelley = England
WriterToCountry 'Byron = England
WriterToCountry 'Sartre = France
WriterToCountry 'Camus = France
Also, we declare WriterToCity type family that is similar to WriterToCity function implemented in Agda. In contrast to Agda, we should enable the language extension called TypeInType. You may implement this function via PolyKinds since GHC 8.6.
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}
type family WriterToCity (a :: Writers) :: WriterToCountry a where
WriterToCity 'Wilde = 'Dublin
WriterToCity 'Shelley = 'London
WriterToCity 'Byron = 'London
WriterToCity 'Camus = 'Paris
WriterToCity 'Sartre = 'Paris
Dependent pairs
We introduce the dependent pair type (-type) through a simple example.
Let us consider the following inductive predicate on two lists as a GADT:
data IsReverse {A : Set} : (xs ys : List A) → Set where
ReverseNil : IsReverse [] []
ReverseCons : (x : A) (xs ys : List A)
→ IsReverse xs ys
→ IsReverse (x ∷ xs) (ys ++ [ x ])
IsReverse xs ys denotes that the list ys is equal to reversed xs. IsReverse is a datatype parameterized over a type A and indexed over two lists of elements of type A.
We prove the theorem that for all list xs there exists list ys such that ys is a reversed list xs. In other words, we should produce a dependent pair, where the first projection of this pair is some list ys and the second one is a proof that ys is reversed list xs.
We use the dependent pair type to prove existence:
theoremReverse₁ : {A : Set} (xs : List A) → Σ (List A) (λ ys → IsReverse xs ys)
theoremReverse₁ [] = [] , ReverseNil
theoremReverse₁ (z ∷ zs) =
let ys = proj₁ (theoremReverse₁ zs) in
let ysProof = proj₂ (theoremReverse₁ zs) in
ys ++ [ x ] , ReverseCons z zs ys ysProof
We should read the signature {A : Set} (xs : List A) → Σ (List A) (λ ys → IsReverse xs ys) as “let A be type and xs be a list with elements of the type A, then there exists list ys, such that ys is the reversed list xs”.
We prove this theorem by induction on xs and build ys for every case. If xs is empty, then we present an empty list as the desired list ys and ReverseNil is a proof that ys is equal to reversed list xs, because both of them are empty. Thus, we have proved the base case.
The inductive step is a case when xs is a non-empty list, i.e. xs = z :: zs. List zs is smaller than z :: zs, so we can apply induction hypothesis to zs and show that :: preserves the desired property using the ReverseCons constructor.
Generally, -type is defined in Agda as follows:
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
constructor _,_
field
fst : A
snd : B fst
This record is defined for arbitrary universes, and we consider below what universes are in more detail. The given record has two fields. The first field called fst is an object of a type A. The second one is an application B to the argument from the first field.
From a logical point of view, we read Σ A B as “there exists some element of a type A, such that this element satisfies property B”, i.e. -type encodes constructive existential quantifier. As we have told before, to prove the existence of some object with desired property constructively, then we should present the particular object and prove this object satisfies this considered property.
Universes
A hierarchy of types is a quite old idea that initially belongs to the logician and philosopher Bertrand Russell. The basic types such as Nat or Bool have a type called Set, but Set is not Set itself. Set has a type Set₁, etc. Otherwise, we could infer Russell’s paradox, so our system would be inconsistent in that case.
Universe polymorphism also allows defining functions that can be called on types of arbitrary levels. Let us show how universe polymorphism works on the following example. Suppose we have this function called s:
s : {A B C : Set} → (A → B → C) → (A → B) → A → C
s f g x = f x (g x)
We implement a similar function in Haskell via RankNTypes:
{-# LANGUAGE RankNTypes #-}
s :: forall a b c. (a -> b -> c) -> (a -> b) -> a -> c
s f g x = f x (g x)
We can indicate that types A, B, C are types of arbitrary level a:
s₁ : {a : Level} {A B C : Set a} → (A → B → C) → (A → B) → A → C
s₁ f g x = f x (g x)
We generalize s further, because A, B and C in s₁ belong to the same level, but these types may generally belong to different levels :
s₂ : {a b c : Level} {A : Set a} {B : Set b} {C : Set c}
→ (A → B → C) → (A → B) → A → C
s₂ f g x = f x (g x)
We would implement something similar as closed type family in Haskell:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
type family S₂ (f :: a -> b -> c) (g :: a -> b) (x :: a) :: c where
S₂ f g x = f x (g x)
By the way, the most general version of s in Agda is an universe polymorphic dependent function:
S : {a b c : Level} {A : Set a} {B : A → Set b} {C : (x : A) → B x → Set c}
→ (f : (x : A) → (y : B x) → C x y) → (g : (x : A) → B x)
→ (x : A) → C x (g x)
S f g x = f x (g x)
Records
Records in Agda are arranged similarly to Haskell. This record implemented in Haskell
data Person = Person {
name :: String
, country :: String
, age :: Int
}
may be translated to Agda as follows via keyword record:
record Person : Set where
field
name : String
country : String
age : Int
Typeclasses are introduced in Agda as records. For example, we implement typeclass called Functor:
record Functor {a} (F : Set a → Set a) : Set (suc a) where
field
fmap : ∀ {A B} → (A → B) → F A → F B
Instances may be declared either by constructing a record explicitly or by using copatterns:
instance
ListFunctor₁ : Functor List
ListFunctor₁ = record { fmap = map }
instance
ListFunctor₂ : Functor List
fmap {{ListFunctor₂}} = map
Propositional equality
The identity type is a datatype that reflects equality of terms in predicate logic. This type is defined as follows:
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
refl : x ≡ x
We consider a few examples where propositional equality is used. The first one is a proof of distributivity of natural number multiplication over addition.
*-+-distr : ∀ a b c → (b + c) * a ≡ b * a + c * a
*-+-distr a zero c = refl
*-+-distr a (suc b) c =
begin
(suc b + c) * a ≡⟨ refl ⟩
a + (b + c) * a ≡⟨ cong (_+_ a) (*-+-distr a b c) ⟩
a + (b * a + c * a) ≡⟨ sym (+-assoc a (b * a) (c * a)) ⟩
suc b * a + c * a
∎
This property is proved by induction on b. When b equals zero, the equality holds trivially. Otherwise, if b is a non-zero number, then equality is proved using the induction hypothesis.
Propositional equality in Haskell
See the relevant part of the Haskell Prelude documentation.
We have propositional equality in Haskell as well:
data a :~: b where
Refl :: a :~: a
Unlike in Agda, this datatype is defined on types of arbitrary kinds, not on terms. In other words, (:~:) :: k -> k -> *, where k is an arbitrary kind.
Algebraic example
We consider a few more examples in Agda to better understand its possibilities. Remember the abstract algebra, especially ring theory. We provide some algebraic definitions below:
Definition 3 A ring is an algebraic system , where is a non-empty set, , , are binary operations on and is a unary operation on such that:
- ;
- ;
- ;
- ;
- ;
- .
We define a ring in Agda similarly by declaring a record called Ring. Ring is a type R with additional operations:
record Ring (R : Set) : Set₁ where
constructor mkRing
infixr 7 _·_
infixr 6 _+_
field
θ : R
-_ : R → R
_+_ : R → R → R
_·_ : R → R → R
After that, we formulate the axioms of a ring having declared operations above:
+-assoc : (a b c : R) → (a + b) + c ≡ a + (b + c)
+-commute : (a b : R) → a + b ≡ b + a
+-inv₁ : (a : R) → - a + a ≡ θ
+-θ : (a : R) → a + θ ≡ a
·-distr-right : (a b c : R) → (a + b) · c ≡ (a · c) + (b · c)
·-distr-left : (a b c : R) → a · (b + c) ≡ (a · b) + (a · c)
open Ring {{...}} public
It is easy to see that the definition of a ring in Agda is similar to the informal definition of a ring proposed above.
Suppose we need to extend a ring with additional axioms. Consider a Lie ring that generalizes Lie algebra, which is a well-known construction in linear algebra widely applied in mathematical physics and quantum mechanics. Initially, we suggest the following informal definition:
Definition 4 A Lie ring is a ring with two additional axioms:
- (Alternation) ;
- (Jacobi identity) .
We extend a ring to a Lie ring in Agda by declaring a new record, but we need to tell somehow that a given type R is already a ring. We pass an additional instance argument in a signature of a record called LieRing for this purpose:
record LieRing (R : Set){{ring : Ring R}} : Set₁ where
Then we add the special axioms of a Lie ring as usual:
constructor mkLeeRing
field
alternation : (a : R) → a · a ≡ θ
jacobiIdentity : (a b c : R) → (a · b) · c + b · (c · a) + c · (a · b) ≡ θ
Lie ring is anticommutative, in other words:
Lemma 1 Let be Lie ring, then forall , .
Proof Firstly, we prove this fact informally. For convenience, we prove this useful proposition.
Proposition 1 If is a Lie ring, then forall , .
Thus by proposition above and alternation.
Formalisation of this proof completely preserves the reasoning above. The first lemma is the sequence of equalities applied sequentially via transitivity of propositional equality:
lemma : (a b : R) → (a + b) · (a + b) ≡ (a · b) + (b · a)
lemma a b =
begin
((a + b) · (a + b)
≡⟨ ·-distr-right a b (a + b) ⟩
a · (a + b) + b · (a + b)
≡⟨ cong₂ _+_ (·-distr-left a a b) (·-distr-left b a b) ⟩
(a · a + a · b) + (b · a + b · b)
≡⟨ cong (_+_ (a · a + a · b)) (cong₂ _+_ refl (alternation b)) ⟩
(a · a + a · b) + (b · a + θ)
≡⟨ cong (_+_ (a · a + a · b)) (+-θ (b · a)) ⟩
(a · a + a · b) + (b · a)
≡⟨ cong₂ _+_
(cong₂ _+_ (alternation a) refl)
refl ⟩
(θ + a · b) + (b · a)
≡⟨ cong₂ _+_ (trans (+-commute θ (a · b)) (+-θ (a · b))) refl ⟩
(a · b + b · a)
∎)
Anticommutativity is proved in the same way using the obtained lemma:
anticommutativity : (a b : R) → (a · b + b · a) ≡ θ
anticommutativity a b = (a · b + b · a) ≡⟨ sym $ lemma a b ⟩ (alternation (a + b))
Conclusion
In this post, we have briefly described basic concepts of dependently typed programming and theorem proving in Agda via examples. In the next post, we will introduce negation with classical postulates and play with non-constructive proofs in Agda.
Follow Serokell on Twitter and Facebook to keep in touch!
Find out about our Haskell consulting services.
.jpg)
