Rewriting

Rewrite rules allow you to extend Agda’s evaluation relation with new computation rules.

Rules are safe to use with Agda.Builtin.Equality if –confluence-check is enabled. Confluent but non-terminating rewrite rules can not break consistency, unlike to non-terminating functions. Those results were proven by Cockx, Tabareau, and Winterhalter, see section 3 for statements.

Note

This page is about the --rewriting option and the associated REWRITE builtin. You might be looking for the documentation on the rewrite construct instead.

Rewrite rules by example

To enable rewrite rules, you should run Agda with the flag --rewriting and import the modules Agda.Builtin.Equality and Agda.Builtin.Equality.Rewrite:

{-# OPTIONS --rewriting #-}

module language.rewriting where

open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

Overlapping pattern matching

To start, let’s look at an example where rewrite rules can solve a problem that is encountered by almost every newcomer to Agda. This problem usually pops up as the question why 0 + m computes to m, but m + 0 does not (and similarly, (suc m) + n computes to suc (m + n) but m + (suc n) does not). This problem manifests itself for example when trying to prove commutativity of _+_:

+comm : m + n ≡ n + m
+comm {m = zero}  = refl
+comm {m = suc m} = cong suc (+comm {m = m})

Here, Agda complains that n != n + zero of type Nat. The usual way to solve this problem is by proving the equations m + 0 ≡ m and m + (suc n) ≡ suc (m + n) and using an explicit rewrite statement in the main proof (N.B.: Agda’s rewrite keyword should not be confused with rewrite rules, which are added by a REWRITE pragma.)

By using rewrite rules, we can simulate the solution from our paper. First, we need to prove that the equations we want hold as propositional equalities:

+zero : m + zero ≡ m
+zero {m = zero}  = refl
+zero {m = suc m} = cong suc +zero

+suc : m + (suc n) ≡ suc (m + n)
+suc {m = zero}  = refl
+suc {m = suc m} = cong suc +suc

Next we mark the equalities as rewrite rules with a REWRITE pragma:

{-# REWRITE +zero +suc #-}

Now the proof of commutativity works exactly as we wrote it before:

+comm : m + n ≡ n + m
+comm {m = zero}  = refl
+comm {m = suc m} = cong suc (+comm {m = m})

Note that there is no way to make this proof go through without rewrite rules: it is essential that _+_ computes both on its first and its second argument, but there’s no way to define _+_ in such a way using Agda’s regular pattern matching.

More examples

Additional examples of how to use rewrite rules can be found in a blog post by Jesper Cockx.

Controlling rewrite rule matching with primRewriteNoMatch

Rewrite rule matching does not reduce pattern-matching definitions. This can cause seemingly harmless rewrite rules to be non-confluent. For example, consider the rewrite rule for associativity of vector concatenation (which itself depends on associativity of addition).

_++_ : Vec A n → Vec A m → Vec A (n + m)
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

++-assoc : {xs : Vec A n} {ys : Vec A m} {zs : Vec A l}
         → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc {xs = []}     = refl
++-assoc {xs = x ∷ xs} = cong (x ∷_) (++-assoc {xs = xs})

Unfortunately, if we specialise the length of the first vector to zero, the ++-assoc rewrite rule does not apply correctly.

{-# REWRITE ++-assoc #-}

++-assoc-fail : {xs : Vec A zero} {ys : Vec A m} {zs : Vec A l}
              → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc-fail = refl -- error: [UnequalTerms]
                     -- The terms
                     --   _++_ {n = m} (xs ++ ys) zs
                     -- and
                     --   _++_ {n = zero} xs (ys ++ zs)
                     -- are not equal at type Vec A (m + l)

The problem is that the outer _++_ on ++-assoc’s left-hand side takes an implicit length argument {n = n + m} but in our special-case, n is zero and so the implicit argument reduces to just {n = m}. Agda does not reduce pattern-matching definitions during rewrite rule matching, so it fails to match m against n + m and the rewrite does not apply.

The primRewriteNoMatch primitive (exported by Agda.Builtin.Equality.Rewrite) enables manually working around this limitation. Wrapping subterms of rewrite rule left-hand sides with the primitive tells Agda to not strictly match against those subterms (only check conversion after matching the rest of the rewrite rule LHS has succeeded). All variables which freely occur in primRewriteNoMatch-wrapped subterms must be bound somewhere else on the left-hand side.

If we wrap the implicit length argument to the outer _++_ on the left-hand side of the associativity of vector concatenation rewrite rule with primRewriteNoMatch, then we find the rewrite rule works correctly.

++-assoc' : {xs : Vec A n} {ys : Vec A m} {zs : Vec A l}
          → _++_ {n = primRewriteNoMatch (n + m)} (xs ++ ys) zs
          ≡ xs ++ (ys ++ zs)
++-assoc' {xs = xs} = ++-assoc {xs = xs}

{-# REWRITE ++-assoc' #-}

++-assoc-succeed : {xs : Vec A zero} {ys : Vec A m} {zs : Vec A l}
                 → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
++-assoc-succeed = refl

Definitional singletons and subject reduction

Some useful rewrite rules break subject reduction in the presence of definitional singletons (such as the unit type, ⊤).

For example, consider the following axiomatisation of the circle as a higher inductive type:

IdOver : (P : A → Set) → x ≡ y → P x → P y → Set
IdOver P refl x y = x ≡ y

syntax IdOver P p x y = x ≡[ P ↓ p ]≡ y

dcong : ∀ {B : A → Set} (f : (x : A) → B x) (p : x ≡ y) → f x ≡[ B ↓ p ]≡ f y
dcong f refl = refl

postulate
  Circle : Set
  base   : Circle
  loop   : base ≡ base

  circle-elim : ∀ (P : Circle → Set) (baseP : P base)
              → baseP ≡[ P ↓ loop ]≡ baseP
              → ∀ x → P x

  circle-elim-base : ∀ (P : Circle → Set) (baseP : P base)
                       (loopP : baseP ≡[ P ↓ loop ]≡ baseP)
                   → circle-elim P baseP loopP base ≡ baseP
  {-# REWRITE circle-elim-base #-}

  circle-elim-loop : ∀ (P : Circle → Set) (baseP : P base)
                       (loopP : baseP ≡[ P ↓ loop ]≡ baseP)
                   → dcong (circle-elim P baseP loopP) loop ≡ loopP

Ideally, we would also turn the computation rule for circle-elim applied to the path constructor loop (circle-elim-loop) into a rewrite rule:

{-# REWRITE circle-elim-loop #-}

Unfortunately, this causes subject reduction issues when eliminating into ⊤. Note that, by η-equality, we have circle-elim (λ _ → ⊤) tt p = circle-elim (λ _ → ⊤) tt q definitionally for any two identity proofs p and q.

open import Agda.Builtin.Unit

circle-elim-pq : ∀ {p q}
               → circle-elim (λ _ → ⊤) tt p
               ≡ circle-elim (λ _ → ⊤) tt q
circle-elim-pq = refl

The computation rule circle-elim-loop should therefore also imply p ≡ q definitionally, but the inductive identity type does not satisfy such an η rule.

Agda tries to detect such problematic rewrite rules and will throw a RewriteVariablesBoundInSingleton warning if it is not certain that the rewrite is safe. If you are confident your rewrite rule is actually safe or you know you are not using definitional singletons, or you are simply not worried about weirdly behaving definitional equality, you can silence the warning with -WnoRewriteVariablesBoundInSingleton and continue to rely on the rewrite rule.

General shape of rewrite rules

In general, an equality proof eq may be registered as a rewrite rule using the pragma {-# REWRITE eq #-}, provided the following requirements are met:

• The type of eq is of the form eq : (x₁ : A₁) ... (xₖ : Aₖ) → f p₁ ... pₙ ≡ v

• f is a postulate, a defined function symbol, or a constructor applied to fully general parameters (i.e. the parameters must be distinct variables)

• Each variable x₁, …, xₖ occurs at least once in a pattern position in p₁ ... pₙ (see below for the definition of pattern positions)

• The left-hand side f p₁ ... pₙ should be neutral, i.e. it should not reduce.

The following patterns are supported:

• x y₁ ... yₙ, where x is a pattern variable and y₁, …, yₙ are distinct variables that are bound locally in the pattern

• f p₁ ... pₙ, where f is a postulate, a defined function, a constructor, or a data/record type, and p₁, …, pₙ are again patterns

• λ x → p, where p is again a pattern

• (x : P) → Q, where P and Q are again patterns

• y p₁ ... pₙ, where y is a variable bound locally in the pattern and p₁, …, pₙ are again patterns

• Set p or Prop p, where p is again a pattern

• Any other term v (here the variables in v are not considered to be in a pattern position)

Once a rewrite rule has been added, Agda automatically rewrites all instances of the left-hand side to the corresponding instance of the right-hand side during reduction. More precisely, a term (definitionally equal to) f p₁σ ... pₙσ is rewritten to vσ, where σ is any substitution on the pattern variables x₁, … xₖ.

Since rewriting happens after normal reduction, rewrite rules are only applied to terms that would otherwise be neutral.

Confluence checking

Agda can optionally check confluence of rewrite rules by enabling the --confluence-check flag. Concretely, it does so by enforcing two properties:

1. For any two left-hand sides of the rewrite rules that overlap (either at the root position or at a subterm), the most general unifier of the two left-hand sides is again a left-hand side of a rewrite rule. For example, if there are two rules suc m + n = suc (m + n) and m + suc n = suc (m + n), then there should also be a rule suc m + suc n = suc (suc (m + n)).

2. Each rewrite rule should satisfy the triangle property: For any rewrite rule u = w and any single-step parallel unfolding u => v, we should have another single-step parallel unfolding v => w.

There is also a flag --local-confluence-check that is less restrictive but only checks local confluence of rewrite rules. In case the rewrite rules are terminating (currently not checked), these two properties are equivalent.

Advanced usage

Instead of importing Agda.Builtin.Equality.Rewrite, a different type may be chosen as the rewrite relation by registering it as the REWRITE builtin. For example, using the pragma {-# BUILTIN REWRITE _~_ #-} registers the type _~_ as the rewrite relation. To qualify as the rewrite relation, the type must take at least two arguments, and the final two arguments should be visible.

Importing rewrite rules

With import M, all of M’s rewrite rules get imported no matter whether they are private or in submodules of M. Further, all the rewrite rules that M imports will also get imported, transitively. Thus, say module M0 declares or imports some rewrite rules, and M1 imports M0, then any module M2 importing M1 will import these rewrite rules even if M2 does not directly import M0.

The reason for this transitive import behavior of rewrite rules is to ensure the subject reduction (aka type preservation) property. Say M0 exports a type A and a rule that rewrites A to Nat, then M1 can declare a constant a = zero of type A. If M2 could import A and a from M1 but not the rewrite rule for A, then in the context of M2 the reduction from a to zero would change its type from A to Nat which is not equal to A in absence of the rewrite rule. Thus, type preservation under reduction would fail.

In summary, the scoping rules for rewrite rules are same as the scoping rules for instances in Haskell 2010.