Agda (theorem prover)

Agda is a dependently typed functional programming language originally developed by Ulf Norell at Chalmers University of Technology with implementation described in his PhD thesis. The current version of Agda was originally known as Agda 2. The original Agda system was developed at Chalmers by Catarina Coquand in 1999. The current version is a full rewrite, which should be considered a new language that shares name and tradition.

Agda, unlike Coq, has no support for tactics, and proofs are written in a functional programming style. The language has ordinary programming constructs such as data types, pattern matching, records, let expressions and modules, and a Haskell-like syntax. The system has an Emacs interface but can also be run in batch mode from the command line.

Agda is based on Zhaohui Luo's Unified Theory of Dependent Types (UTT) a type theory similar to Martin-Löf type theory.

The main way of defining data types in Agda is via inductive data types which are similar to algebraic data types in non-dependently typed programming languages.

Here is a definition of Peano numbers in Agda:

Basically, it means that there are two ways to construct a natural number. Zero is a natural number, and if n is a natural number, then suc n is a natural number too.

Here's a definition of less than or equal relation:

The first constructor allows us to state that zero is less than or equal to any number. The second constructor states that if n ≤ m then suc n ≤ suc m.

In core type theory, induction and recursion principles are used to prove theorems about inductive types. In Agda, dependently typed pattern matching is used instead. For example, natural number addition can be defined like this:

This way of writing recursive functions/inductive proofs is more natural than applying raw induction principles. In Agda, dependently typed pattern matching is a primitive of the language; the core language lacks the induction/recursion principles that pattern matching translates to.