Rewrite rules in Agda

{-# OPTIONS --rewriting #-}

open import Prelude.Equality
{-# BUILTIN REWRITE _≡_ #-}

A first example

open import Agda.Builtin.Nat
variable m n : Nat

module Fails where
  +-comm : m + n ≡ n + m
  +-comm {zero}  = {!refl!}
              -- ^ n != n + zero
  +-comm {suc m} = {!cong suc (+-comm {m})!}
              -- ^ suc (m + n) != n + suc m

Fixing the problem with rewrite rules

postulate
  +0 : m +  ≡ m
  +suc : m + (suc n) ≡ suc (m + n)
{-# REWRITE +0   #-}
{-# REWRITE +suc #-}

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

Higher inductive types

postulate
  I : Set
  i0 i1 : I
  seg : i0 ≡ i1

module _ (P : I → Set) (p0 : P i0) (p1 : P i1)
         (pseg : transport P seg p0 ≡ p1) where

  postulate
    elim-I   : (i : I) → P i
    elim-i0  : elim-I i0 ≡ p0
    elim-i1  : elim-I i1 ≡ p1
    elim-seg-fail : cong′ elim-I seg ≡ {!pseg!}
          -- ^ p0 != elim-I i0

Rewrite rules to the rescue!

  {-# REWRITE elim-i0 #-}
  {-# REWRITE elim-i1 #-}
  postulate
    elim-seg : cong′ elim-I seg ≡ pseg

Exceptional type theory

postulate raise : {A : Set} → A

module _ (P : Bool → Set)
         (ptrue : P true) (pfalse : P false)
         (handle : P raise) where
  postulate
    catch : (b : Bool) → P b
    catch-true : catch true ≡ ptrue
    catch-false : catch false ≡ pfalse
    catch-raise : catch raise ≡ handle
{-# REWRITE catch-true  #-}
{-# REWRITE catch-false #-}
{-# REWRITE catch-raise #-}

Rewrite rules are dangerous!

• Non-termination: loop ⟶ loop
• Non-confluence: b ⟶ true, b ⟶ false
• Loss of subject reduction (!)

Main objective: automatically check safety of user-defined rewrite rules

Non-confluence ⇒ no subject reduction:

data Unit : Set where unit : Unit

postulate
  A : Unit → Set
  A-is-Bool : A unit ≡ Bool
{-# REWRITE A-is-Bool #-}

f : (x : Unit) → A x
f unit = true

postulate A-is-Nat  : ∀ {x} → A x ≡ Nat
{-# REWRITE A-is-Nat #-}

true' : Nat
true' = f unit -- reduces to true!

Confluence ⇒ still no subject reduction:

record Box (A : Set) : Set where
  constructor box
  field unbox : A
open Box

postulate rew : Box (Nat → Nat) ≡ Box (Nat → Bool)
{-# REWRITE rew #-}

zero' : Bool  -- reduces to 0!
zero' = unbox {A = Nat → Bool}
         (box {A = Nat → Nat} λ x → x) 

How to prove subject reduction

The standard proof of subject reduction requires:

• confluence of reduction
• injectivity of Π-types

We can get injectivity of Π-types by restricting rewrite rules to new (postulated) symbols.

So all we need is a confluence checker

A dilemma of checkers

• Most confluence checking algorithms require termination
• Most termination checking algorithms require confluence

How to get out of this loop?

Checking confluence + termination

• Step 1: replace full reduction relation ⟶ by a deterministic rewrite strategy ⟶ₛ
• Step 2: run termination check on ⟶, conclude termination of ⟶ₛ
• Step 3: run confluence check on ⟶ using ⟶ₛ to join critical pairs, conclude confluence of ⟶ₛ
• Step 4: from 2 + 3, conclude termination of ⟶

Adding an equational theory

Equality is not just reduction:

• η-equality for functions and record types
• irrelevance and Prop

We should take these into account for rewriting!

Example

module _ (A : Set) where
  postulate
    h : (A → A) → Bool
    h-id : h (λ x → x) ≡ true
    h-const : ∀ c → h (λ x → c) ≡ false
{-# REWRITE h-id    #-}
{-# REWRITE h-const #-}

Q: is this confluent?

Conclusion

Rewrite rules are useful, but also dangerous

There are many things to take into account when checking safety of rewrite rules

We are currently working hard to add these checks to both Agda and Coq!