Talk at AIM XXIX

16 March 2019

# Rewrite rules in Agda

## 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 + 0 ≡ 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 #-}


# Problems with rewrite rules

## 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) 0


# Checking confluence & termination

## 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?

No! true = f ⊤ (λ x → tt) = false

## 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!