I was following the documentation on rewriting, specifically confluence checking, which states
[...] 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)).
I tried this via the following code (note --local-confluence-check):
{-# OPTIONS --rewriting --local-confluence-check #-}
module RewriteTest0 where
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
+-suc-suc : ∀ (m n : ℕ) → suc m + suc n ≡ suc (suc (m + n))
+-suc-suc m n rewrite +-suc m n = refl
{-# REWRITE +-identityʳ +-suc +-suc-suc #-}
This gives me the following error message:
+-suc-suc is not a legal rewrite rule, since the left-hand side
suc m + suc n reduces to suc (m + suc n)
when checking the pragma REWRITE +-identityʳ +-suc +-suc-suc
I think this implies a bug or that the documentation is wrong or misleading. Any feedback would be appreciated.
The following works fine:
{-# OPTIONS --rewriting --local-confluence-check #-}
module RewriteTest1 where
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
{-# REWRITE +-identityʳ +-suc #-}
+comm : ∀ {m n : ℕ} → m + n ≡ n + m
+comm {zero} = refl
+comm {suc m} = cong suc (+comm {m})
When changing --local-confluence-check to --confluence-check in RewriteTest1 , I get the following error messages:
Global confluence check failed: suc n + suc n₁ can be rewritten to
either suc (suc n + n₁) or suc (n + suc n₁).
Possible fix: add a rewrite rule with left-hand side suc n + suc n₁
to resolve the ambiguity.
when checking confluence of the rewrite rule +-suc with
Agda.Builtin.Nat._+_-clause2
Global confluence check failed: zero + suc n can be rewritten to
either suc (zero + n) or suc n.
Possible fix: add a rewrite rule with left-hand side zero + suc n
to resolve the ambiguity.
when checking confluence of the rewrite rule +-suc with
Agda.Builtin.Nat._+_-clause1
Global confluence check failed: suc n + 0 can be rewritten to
either suc n or suc (n + 0).
Possible fix: add a rewrite rule with left-hand side suc n + 0 to
resolve the ambiguity.
when checking confluence of the rewrite rule +-identityʳ with
Agda.Builtin.Nat._+_-clause2
Changing my code to include the equalities suggested by the error messages makes Agda accept the program. (I am confused, however, as two of them seem to just be special cases of existing rules, see code comments below. Also, the documentation does not mention these being needed.)
{-# OPTIONS --rewriting --confluence-check #-}
module RewriteTest2 where
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
-- the documentation mentioned, that this rule was needed
+-suc-suc : ∀ (m n : ℕ) → suc m + suc n ≡ suc (suc (m + n))
+-suc-suc m n rewrite +-suc m n = refl
-- we already know this from the definition of ℕ, not sure why we need this
zero+suc-n : ∀ (n : ℕ) → 0 + suc n ≡ suc n
zero+suc-n n = refl
-- a specialisation of identityʳ, not sure why we need this
suc-n+zero : ∀ (n : ℕ) → suc n + 0 ≡ suc n
suc-n+zero n rewrite +-identityʳ n = refl
{-# REWRITE +-identityʳ +-suc +-suc-suc zero+suc-n suc-n+zero #-}
+comm : ∀ {m n : ℕ} → m + n ≡ n + m
+comm {zero} = refl
+comm {suc m} = cong suc (+comm {m})
Changing the flag in RewriteTest2 to --local-confluence-check, however, gives an error message:
+-suc-suc is not a legal rewrite rule, since the left-hand side
suc m + suc n reduces to suc (m + suc n)
when checking the pragma
REWRITE +-identityʳ +-suc +-suc-suc zero+suc-n suc-n+zero
This, despite the documentation saying that --local-confluence-check is less restrictive.
This came from me trying to minimise an error I was getting while using REWRITE in a project, which unfortunately I cannot share at this moment. In that project, enabling --confluence-check gives the following error:
An internal error has occurred. Please report this as a bug.
Location of the error: __IMPOSSIBLE__, called at src/full/Agda/TypeChecking/Rewriting/Confluence.hs:606:19 in Agd-2.6.4.1-d9da44fe:Agda.TypeChecking.Rewriting.Confluence
When using holes in a theorem that uses the rewrite rules, I get the following error:
Panic: uncaught pattern violation
$ agda --version
Agda version 2.6.4.1
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4