В этой небольшой статье расскажу про прагму REWRITE, с помощью которой можно заставить компилятор считать разные определения одинаковыми, на примере сложения натуральных чисел.

Не путать с конструкцией rewrite

Определим модуль и импортируем модули для работы с равенством типов

{-# OPTIONS --rewriting #-}
module Rewriting where 

import Relation.Binary.PropositionalEquality as Eq
open Eq 
open Eq.≡-Reasoning

Для примера определим натуральные числа:

data ℕ : Set where 
    zero : ℕ 
    suc : ℕ → ℕ 

И функцию сложения натуральных чисел

_+_ : ℕ → ℕ → ℕ 
zero + b = b 
(suc a) + b = suc (a + b)

Теперь можно доказать утверждение о том, что zero это левый нейтральный элемент

l-unit : ∀ {n} → zero + n ≡ n
l-unit = refl 

refl можно воспринимать как “верно по определению”. Теперь нужно импортировать правило “переписывания” для равенства типов _≡_:

open import Agda.Builtin.Equality.Rewrite

фактически в этом файле содержится только {-# BUILTIN REWRITE _≡_ #-}, что “говорит” компилятору о том, что если у нас есть a ≡ b, то можно заменять a на b и наоборот.

Теперь докажем, что zero это и правый нетрайльный элемент:

r-unit : ∀ {n} → n + zero ≡ n 
r-unit {n = zero} = refl 
r-unit {n = suc a} = cong suc (r-unit {n = a})
{-# REWRITE r-unit #-}

а так же докажем, что если мы будем выносить suc не из первого, а из второго аргумента за скобку, то это ничего не поменяет

+suc : ∀ {m n} → m + (suc n) ≡ suc (m + n)
+suc {zero}  = refl
+suc {suc m} = cong suc (+suc {m}) 
{-# REWRITE +suc #-}

т.е. мы фактически доказали, что наше определение сложения эквивалентно следующему:

_+_ : ℕ → ℕ → ℕ 
a + zero = a
a + (suc b) = suc (a + b)

и “сказали” компилятору с помощью прагмы rewrite, чтобы он имел это ввиду. Теперь можно очень просто доказать коммутативность сложения:

+comm : ∀ {n m} → m + n ≡ n + m
+comm {m = zero} = refl
+comm {n = a} {m = suc b} = cong suc (+comm {n = a} {m = b})

Если убрать REWRITE будет ошибка компиляции

n != n + zero of type ℕ when checking that the expression refl has type (zero + n) ≡ (n + zero)

без rewrite нам бы пришлось доказывать следующую лемму, которая теперь верна “по определению”:

m+1+n=1+m+n : ∀ {m n} → m + suc n ≡ suc m + n 
m+1+n=1+m+n = refl

да и само доказательство выглядело бы сильно сложнее

+-comm` : ∀ {a b} → a + b ≡ b + a
+-comm` {zero} {b} = sym(r-unit {b}) --заменяется на refl
+-comm` {suc a} {b} = begin
    suc a + b   ≡⟨⟩
    suc (a + b) ≡⟨ cong suc (+-comm` {a} {b}) ⟩
    suc (b + a) ≡⟨⟩
    suc b + a   ≡⟨ m+1+n=1+m+n {b} {a} ⟩ --тоже можно заменить на refl
    b + suc a   ∎

Минусы и подводные камни

Данная прагма не считается “безопасной” т.е. конфликтует с опцией --safe и соответственно такие доказательства нельзя использовать в “безопасных” модулях. Документация объясняет это тем, что это может, например, нарушить сходимость, т.е. в теории можно придумать пример, когда компилятор бесконечно будет перебирать разные варианты переписывания и ни к чему не придет.

UPD: Вообще не в теории, пишите {-# REWRITE +comm #-} и наслаждаетесь бесконечной компиляцией.

Ссылки

Еще примеры можно найти тут