Content deleted Content added
Omnipaedista (talk | contribs) standardized punct. |
m Update syntaxhighlight tags - remove use of deprecated <source> tags - BOT in trial - BRFA |
||
Line 38:
Here is a definition of [[Peano axioms|Peano numbers]] in Agda:
<
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
</syntaxhighlight>
Basically, it means that there are two ways to construct a value of type ℕ, representing a natural number. To begin, <code>zero</code> is a natural number, and if <code>n</code> is a natural number, then <code>suc n</code>, standing for the [[Successor function|successor]] of <code>n</code>, is a natural number too.
Here is a definition of the "less than or equal" relation between two natural numbers:
<
data _≤_ : ℕ → ℕ → Set where
z≤n : {n : ℕ} → zero ≤ n
s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m
</syntaxhighlight>
The first constructor, <code>z≤n</code>, corresponds to the axiom that zero is less than or equal to any natural number. The second constructor, <code>s≤s</code>, corresponds to an inference rule, allowing to turn a proof of <code>n ≤ m</code> into a proof of <code>suc n ≤ suc m</code>.<ref>{{Cite web |url = https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat.agda |title = Nat from Agda standard library |accessdate = 2014-07-20 }}</ref> So the value <code lang="agda">s≤s {zero} {suc zero} (z≤n {suc zero})</code> is a proof that one (the successor of zero), is less than or equal to two (the successor of one). The parameters provided in curly brackets may be omitted if they can be inferred.
=== Dependently typed pattern matching ===
In core type theory, induction and recursion principles are used to prove theorems about [[inductive type]]s. In Agda, dependently typed pattern matching is used instead. For example, natural number addition can be defined like this:
<
add zero n = n
add (suc m) n = suc (add m n)
</syntaxhighlight>
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.
=== Metavariables ===
One of the distinctive features of Agda, when compared with other similar systems such as [[Coq]], is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda:
<
add : ℕ → ℕ → ℕ
add x y = ?
</syntaxhighlight>
<code>?</code> here is a metavariable. When interacting with the system in emacs mode, it will show the user expected type and allow them to refine the metavariable, i.e., to replace it with more detailed code. This feature allows incremental program construction in a way similar to tactics-based proof assistants such as Coq.
=== Proof automation ===
Programming in pure type theory involves a lot of tedious and repetitive proofs. Although Agda has no separate tactics language, it is possible to program useful tactics within Agda itself. Typically, this works by writing an Agda function that optionally returns a proof of some property of interest. A tactic is then constructed by running this function at type-checking time, for example using the following auxiliary definitions:
<
data Maybe (A : Set) : Set where
Just : A → Maybe A
Line 83:
Tactic Nothing ()
Tactic (Just x) auto = x
</syntaxhighlight>
Given a function <code>check-even : (n : ℕ) → Maybe (Even n)</code> that inputs a number and optionally returns a proof of its evenness, a tactic can then be constructed as follows:
<
check-even-tactic : {n : ℕ} → isJust (check-even n) → Even n
check-even-tactic {n} = Tactic (check-even n)
Line 96:
lemma2 : Even (suc (suc zero))
lemma2 = check-even-tactic auto
</syntaxhighlight>
The actual proof of each lemma will be automatically constructed at type-checking time. If the tactic fails, type-checking will fail.
| |||