From b04439d6afd548051a130a04d749cf4be6de3092 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Mon, 4 Mar 2024 20:24:26 +0000
Subject: [PATCH 01/15] =?UTF-8?q?=E2=8C=9E=5F=E2=8C=9F=20for=20marking=20s?=
 =?UTF-8?q?pots=20to=20rewrite.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Tactic/Cong.agda | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 2c02ec6a4c..52ade4d6e9 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -55,6 +55,9 @@ open import Reflection.AST.Term                 as Term
 
 open import Reflection.TCM.Syntax
 
+⌞_⌟ : ∀ {a} {A : Set a} → A → A
+⌞_⌟ x = x
+
 ------------------------------------------------------------------------
 -- Utilities
 ------------------------------------------------------------------------
@@ -136,6 +139,8 @@ private
   antiUnifyClauses : ℕ → Clauses → Clauses → Maybe Clauses
   antiUnifyClause  : ℕ → Clause → Clause → Maybe Clause
 
+  pattern apply-⌞⌟ t = (def (quote ⌞_⌟) (_ ∷ _ ∷ arg _ t ∷ []))
+
   antiUnify ϕ (var x args) (var y args') with x ℕ.≡ᵇ y | antiUnifyArgs ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ uargs
@@ -144,6 +149,7 @@ private
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ []
   ... | true  | just uargs = con c uargs
+  antiUnify ϕ (def f args) (apply-⌞⌟ t) = antiUnify ϕ (def f args) t
   antiUnify ϕ (def f args) (def f' args') with f Name.≡ᵇ f' | antiUnifyArgs ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ []

From 3258d127bb1b3284b5a74eb828ac1b1fb4961000 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Wed, 6 Mar 2024 13:40:52 +0000
Subject: [PATCH 02/15] Added documentation.

---
 doc/README/Tactic/Cong.agda | 25 ++++++++++++++++++++++++-
 src/Tactic/Cong.agda        | 13 +++++++++++++
 2 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda
index 20cb5ad7d9..af24b128a2 100644
--- a/doc/README/Tactic/Cong.agda
+++ b/doc/README/Tactic/Cong.agda
@@ -8,7 +8,7 @@ open import Data.Nat.Properties
 open import Relation.Binary.PropositionalEquality as Eq
 import Relation.Binary.Reasoning.Preorder as PR
 
-open import Tactic.Cong using (cong!)
+open import Tactic.Cong using (cong! ; ⌞_⌟)
 
 ----------------------------------------------------------------------
 -- Usage
@@ -68,6 +68,29 @@ succinct-example m n eq =
 -- to deduce where to generalize. When presented with two sides
 -- of an equality like 'm + n ≡ n + m', it will anti-unify to
 -- 'ϕ + ϕ', which is too specific.
+--
+-- In these cases, you may explicitly mark the subterms to be
+-- generalized by wrapping them in the marker function, ⌞_⌟.
+
+marker-example₁ : ∀ m n o p → m + n + (o + p) ≡ n + m + (p + o)
+marker-example₁ m n o p =
+  let open Eq.≡-Reasoning in
+  begin
+    ⌞ m + n ⌟ + (o + p)
+  ≡⟨ cong! (+-comm m n) ⟩
+    n + m + ⌞ o + p ⌟
+  ≡⟨ cong! (+-comm o p) ⟩
+    n + m + (p + o)
+  ∎
+
+marker-example₂ : ∀ m n → m + n + (m + n) ≡ n + m + (n + m)
+marker-example₂ m n =
+  let open Eq.≡-Reasoning in
+  begin
+    ⌞ m + n ⌟ + ⌞ m + n ⌟
+  ≡⟨ cong! (+-comm m n) ⟩
+    n + m + (n + m)
+  ∎
 
 ----------------------------------------------------------------------
 -- Unit Tests
diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 52ade4d6e9..0d855683cf 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -18,6 +18,8 @@
 --   ≡⟨ cong! (+-identityʳ n) ⟨
 --     suc (suc n) + (n + 0)
 --   ∎
+--
+-- Please see README.Tactic.Cong for more details.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}
@@ -55,6 +57,17 @@ open import Reflection.AST.Term                 as Term
 
 open import Reflection.TCM.Syntax
 
+-- Marker to keep anti-unification from descending into the wrapped
+-- subterm.
+--
+-- For instance, anti-unification of ⌞ a + b ⌟ + c and b + a + c
+-- yields λ ϕ → ϕ + c, as opposed to λ ϕ → ϕ + ϕ + c without ⌞_⌟.
+--
+-- The marker is only visible to the cong! tactic, which inhibits
+-- normalisation. Anywhere else, ⌞ a + b ⌟ reduces to a + b.
+--
+-- Thus, proving ⌞ a + b ⌟ + c ≡ b + a + c via cong! (+-comm a b)
+-- also proves a + b + c ≡ b + a + c.
 ⌞_⌟ : ∀ {a} {A : Set a} → A → A
 ⌞_⌟ x = x
 

From b1065a35d4df560f2592b2e2ff48276161469c71 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Thu, 7 Mar 2024 18:09:03 +0000
Subject: [PATCH 03/15] =?UTF-8?q?In=20case=20of=20failure,=20try=20swappin?=
 =?UTF-8?q?g=20the=20RHS=20with=20the=20LHS.=20Fixes=20=E2=89=A1=CB=98?=
 =?UTF-8?q?=E2=9F=A8=20...=20=E2=9F=A9.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Tactic/Cong.agda | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 0d855683cf..d15efaadad 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -236,6 +236,12 @@ macro
     withNormalisation false $ do
       goal ← inferType hole
       eqGoal ← destructEqualityGoal goal
-      let cong-lam = antiUnify 0 (EqualityGoal.lhs eqGoal) (EqualityGoal.rhs eqGoal)
-      cong-tm ← `cong eqGoal cong-lam x≡y
-      unify cong-tm hole
+      let uni = do
+        let cong-lam = antiUnify 0 (EqualityGoal.lhs eqGoal) (EqualityGoal.rhs eqGoal)
+        cong-tm ← `cong eqGoal cong-lam x≡y
+        unify cong-tm hole
+      let uni' = do
+        let cong-lam = antiUnify 0 (EqualityGoal.rhs eqGoal) (EqualityGoal.lhs eqGoal)
+        cong-tm ← `cong eqGoal cong-lam x≡y
+        unify cong-tm hole
+      catchTC uni uni'

From 3a5cc94569f8a12b8c0a06cc023dd36e377e06f1 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Thu, 7 Mar 2024 18:14:01 +0000
Subject: [PATCH 04/15] Added comments.

---
 src/Tactic/Cong.agda | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index d15efaadad..fee2ea6fd3 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -241,7 +241,9 @@ macro
         cong-tm ← `cong eqGoal cong-lam x≡y
         unify cong-tm hole
       let uni' = do
+        -- Like uni, but with RHS and LHS swapped.
         let cong-lam = antiUnify 0 (EqualityGoal.rhs eqGoal) (EqualityGoal.lhs eqGoal)
         cong-tm ← `cong eqGoal cong-lam x≡y
         unify cong-tm hole
+      -- When using ⌞_⌟ with ≡˘⟨ ... ⟩, uni fails and uni' succeeds.
       catchTC uni uni'

From 9a26cb0418bc9915e9537b88d3ae9da9167b27cf Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Fri, 8 Mar 2024 12:18:03 +0000
Subject: [PATCH 05/15] More clarity. Less redundancy.

---
 doc/README/Tactic/Cong.agda |  4 ++--
 src/Tactic/Cong.agda        | 16 +++++++---------
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda
index af24b128a2..8bdc351598 100644
--- a/doc/README/Tactic/Cong.agda
+++ b/doc/README/Tactic/Cong.agda
@@ -69,8 +69,8 @@ succinct-example m n eq =
 -- of an equality like 'm + n ≡ n + m', it will anti-unify to
 -- 'ϕ + ϕ', which is too specific.
 --
--- In these cases, you may explicitly mark the subterms to be
--- generalized by wrapping them in the marker function, ⌞_⌟.
+-- In cases like these, you may explicitly mark the subterms to
+-- be generalized by wrapping them in the marker function, ⌞_⌟.
 
 marker-example₁ : ∀ m n o p → m + n + (o + p) ≡ n + m + (p + o)
 marker-example₁ m n o p =
diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index fee2ea6fd3..a91507f9b7 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -236,14 +236,12 @@ macro
     withNormalisation false $ do
       goal ← inferType hole
       eqGoal ← destructEqualityGoal goal
-      let uni = do
-        let cong-lam = antiUnify 0 (EqualityGoal.lhs eqGoal) (EqualityGoal.rhs eqGoal)
+      let uni = λ lhs rhs → do
+        let cong-lam = antiUnify 0 lhs rhs
         cong-tm ← `cong eqGoal cong-lam x≡y
         unify cong-tm hole
-      let uni' = do
-        -- Like uni, but with RHS and LHS swapped.
-        let cong-lam = antiUnify 0 (EqualityGoal.rhs eqGoal) (EqualityGoal.lhs eqGoal)
-        cong-tm ← `cong eqGoal cong-lam x≡y
-        unify cong-tm hole
-      -- When using ⌞_⌟ with ≡˘⟨ ... ⟩, uni fails and uni' succeeds.
-      catchTC uni uni'
+      let lhs = EqualityGoal.rhs eqGoal
+      let rhs = EqualityGoal.lhs eqGoal
+      -- When using ⌞_⌟ with ≡˘⟨ ... ⟩, (uni lhs rhs) fails and
+      -- (uni rhs lhs) succeeds.
+      catchTC (uni lhs rhs) (uni rhs lhs)

From ac7650df99192d7bfb550a8149977518dcc0b749 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Fri, 8 Mar 2024 12:21:20 +0000
Subject: [PATCH 06/15] Fixed performance regression.

---
 src/Tactic/Cong.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index a91507f9b7..d29d2c6d1e 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -240,8 +240,8 @@ macro
         let cong-lam = antiUnify 0 lhs rhs
         cong-tm ← `cong eqGoal cong-lam x≡y
         unify cong-tm hole
-      let lhs = EqualityGoal.rhs eqGoal
-      let rhs = EqualityGoal.lhs eqGoal
+      let lhs = EqualityGoal.lhs eqGoal
+      let rhs = EqualityGoal.rhs eqGoal
       -- When using ⌞_⌟ with ≡˘⟨ ... ⟩, (uni lhs rhs) fails and
       -- (uni rhs lhs) succeeds.
       catchTC (uni lhs rhs) (uni rhs lhs)

From aaa0e3225004107bb236e738ed2c2f0a9d625263 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Fri, 8 Mar 2024 15:21:34 +0000
Subject: [PATCH 07/15] Changelog entry.

---
 CHANGELOG.md | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bbc65af5d7..a279f506ee 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -54,7 +54,7 @@ New modules
   ```agda
   Algebra.Module.Construct.Idealization
   ```
-  
+
 * `Function.Relation.Binary.Equality`
   ```agda
   setoid : Setoid a₁ a₂ → Setoid b₁ b₂ → Setoid _ _
@@ -269,3 +269,6 @@ Additions to existing modules
   ↭-sym       : Symmetric (Vector A) _↭_
   ↭-trans     : Transitive (Vector A) _↭_
   ```
+
+* `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
+  anti-unification.

From 02b92a38e5374131c4b538fdeb5b7e3fd34284c9 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Fri, 8 Mar 2024 21:11:26 +0000
Subject: [PATCH 08/15] cong!-specific combinators instead of catchTC.

---
 src/Tactic/Cong.agda | 53 +++++++++++++++++++++++++++++++++-----------
 1 file changed, 40 insertions(+), 13 deletions(-)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index d29d2c6d1e..6a52941513 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -38,7 +38,7 @@ open import Data.Unit.Base            using (⊤)
 open import Data.Word.Base   as Word  using (toℕ)
 open import Data.Product.Base         using (_×_; map₁; _,_)
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong ; sym ; trans)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the
 -- builtin for maximum speed.
@@ -132,6 +132,17 @@ private
     `y ← quoteTC y
     pure $ def (quote cong) $ `a ⟅∷⟆ `A ⟅∷⟆ level ⟅∷⟆ type ⟅∷⟆ vLam "ϕ" f ⟨∷⟩ `x ⟅∷⟆ `y ⟅∷⟆ eq ⟨∷⟩ []
 
+  -- Helper for constructing applications of 'trans'
+  `trans : ∀ {a} {A : Set a} (x : A) {y z : A} → Term → y ≡ z → TC Term
+  `trans {a} {A} x {y} {z} x≡y y≡z = do
+    eq ← quoteTC y≡z
+    `a ← quoteTC a
+    `A ← quoteTC A
+    `x ← quoteTC x
+    `y ← quoteTC y
+    `z ← quoteTC z
+    pure $ def (quote trans) $ `a ⟅∷⟆ `A ⟅∷⟆ `x ⟅∷⟆ `y ⟅∷⟆ `z ⟅∷⟆ x≡y ⟨∷⟩ eq ⟨∷⟩ []
+
 ------------------------------------------------------------------------
 -- Anti-Unification
 --
@@ -220,6 +231,20 @@ private
   antiUnifyClauses ϕ _ _ =
     just []
 
+  makeGoal : ∀ {a} {A : Set a} (x : A) {y z : A} → y ≡ z → Term → TC Term
+  makeGoal x y≡z hole = do
+    inner ← checkType unknown unknown
+    trans-tm ← `trans x inner y≡z
+    unify trans-tm hole
+    pure inner
+
+  solveGoal : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Term → TC ⊤
+  solveGoal x≡y hole = do
+    goal ← inferType hole
+    eqGoal ← destructEqualityGoal goal
+    let cong-lam = antiUnify 0 (EqualityGoal.lhs eqGoal) (EqualityGoal.rhs eqGoal)
+    cong-tm ← `cong eqGoal cong-lam x≡y
+    unify cong-tm hole
 
 ------------------------------------------------------------------------
 -- Rewriting
@@ -233,15 +258,17 @@ macro
     -- the endpoints of the equality are already specified in
     -- the form that the -- programmer expects them to be in,
     -- so normalising buys us nothing.
-    withNormalisation false $ do
-      goal ← inferType hole
-      eqGoal ← destructEqualityGoal goal
-      let uni = λ lhs rhs → do
-        let cong-lam = antiUnify 0 lhs rhs
-        cong-tm ← `cong eqGoal cong-lam x≡y
-        unify cong-tm hole
-      let lhs = EqualityGoal.lhs eqGoal
-      let rhs = EqualityGoal.rhs eqGoal
-      -- When using ⌞_⌟ with ≡˘⟨ ... ⟩, (uni lhs rhs) fails and
-      -- (uni rhs lhs) succeeds.
-      catchTC (uni lhs rhs) (uni rhs lhs)
+    withNormalisation false (solveGoal x≡y hole)
+
+  cong!-≡-⟫ : ∀ {a} {A : Set a} (x : A) {x' y' y z : A} → y ≡ z → x' ≡ y' → Term → TC ⊤
+  cong!-≡-⟫ x y≡z x'≡y' outer = withNormalisation false $
+    makeGoal x y≡z outer >>= solveGoal x'≡y'
+
+  cong!-≡-⟪ : ∀ {a} {A : Set a} (x : A) {x' y' y z : A} → y ≡ z → y' ≡ x' → Term → TC ⊤
+  cong!-≡-⟪ x y≡z y'≡x' outer = withNormalisation false $
+    makeGoal x y≡z outer >>= solveGoal (sym y'≡x')
+
+infixr 2 cong!-≡-⟫ cong!-≡-⟪
+
+syntax cong!-≡-⟫ x y≡z x'≡y' = x ≡⟪ x'≡y' ⟫ y≡z
+syntax cong!-≡-⟪ x y≡z y'≡x' = x ≡⟪ y'≡x' ⟪ y≡z

From 4a37b04fc6699965fb5783ae6945fa29455b96c5 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Mon, 11 Mar 2024 00:29:17 +0000
Subject: [PATCH 09/15] Support other reasoning modules.

---
 doc/README/Tactic/Cong.agda |  12 ++---
 src/Tactic/Cong.agda        | 103 ++++++++++++++++++++++++++----------
 2 files changed, 80 insertions(+), 35 deletions(-)

diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda
index 8bdc351598..eac29ec352 100644
--- a/doc/README/Tactic/Cong.agda
+++ b/doc/README/Tactic/Cong.agda
@@ -8,7 +8,7 @@ open import Data.Nat.Properties
 open import Relation.Binary.PropositionalEquality as Eq
 import Relation.Binary.Reasoning.Preorder as PR
 
-open import Tactic.Cong using (cong! ; ⌞_⌟)
+open import Tactic.Cong
 
 ----------------------------------------------------------------------
 -- Usage
@@ -77,18 +77,18 @@ marker-example₁ m n o p =
   let open Eq.≡-Reasoning in
   begin
     ⌞ m + n ⌟ + (o + p)
-  ≡⟨ cong! (+-comm m n) ⟩
+  ≡⟨! +-comm m n ⟩
     n + m + ⌞ o + p ⌟
-  ≡⟨ cong! (+-comm o p) ⟩
+  ≡⟨! +-comm p o ⟨
     n + m + (p + o)
   ∎
 
 marker-example₂ : ∀ m n → m + n + (m + n) ≡ n + m + (n + m)
 marker-example₂ m n =
-  let open Eq.≡-Reasoning in
-  begin
+  let open ≤-Reasoning in
+  begin-equality
     ⌞ m + n ⌟ + ⌞ m + n ⌟
-  ≡⟨ cong! (+-comm m n) ⟩
+  ≡⟨! +-comm m n ⟩
     n + m + (n + m)
   ∎
 
diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 6a52941513..eab9045bb4 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -31,14 +31,14 @@ open import Function.Base using (_$_)
 open import Data.Bool.Base            using (true; false; if_then_else_; _∧_)
 open import Data.Char.Base   as Char  using (toℕ)
 open import Data.Float.Base  as Float using (_≡ᵇ_)
-open import Data.List.Base   as List  using ([]; _∷_)
+open import Data.List.Base   as List  using (List; []; _∷_; _++_)
 open import Data.Maybe.Base  as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base    as ℕ     using (ℕ; zero; suc; _≡ᵇ_; _+_)
 open import Data.Unit.Base            using (⊤)
 open import Data.Word.Base   as Word  using (toℕ)
 open import Data.Product.Base         using (_×_; map₁; _,_)
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong ; sym ; trans)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong ; sym)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the
 -- builtin for maximum speed.
@@ -132,17 +132,6 @@ private
     `y ← quoteTC y
     pure $ def (quote cong) $ `a ⟅∷⟆ `A ⟅∷⟆ level ⟅∷⟆ type ⟅∷⟆ vLam "ϕ" f ⟨∷⟩ `x ⟅∷⟆ `y ⟅∷⟆ eq ⟨∷⟩ []
 
-  -- Helper for constructing applications of 'trans'
-  `trans : ∀ {a} {A : Set a} (x : A) {y z : A} → Term → y ≡ z → TC Term
-  `trans {a} {A} x {y} {z} x≡y y≡z = do
-    eq ← quoteTC y≡z
-    `a ← quoteTC a
-    `A ← quoteTC A
-    `x ← quoteTC x
-    `y ← quoteTC y
-    `z ← quoteTC z
-    pure $ def (quote trans) $ `a ⟅∷⟆ `A ⟅∷⟆ `x ⟅∷⟆ `y ⟅∷⟆ `z ⟅∷⟆ x≡y ⟨∷⟩ eq ⟨∷⟩ []
-
 ------------------------------------------------------------------------
 -- Anti-Unification
 --
@@ -231,13 +220,6 @@ private
   antiUnifyClauses ϕ _ _ =
     just []
 
-  makeGoal : ∀ {a} {A : Set a} (x : A) {y z : A} → y ≡ z → Term → TC Term
-  makeGoal x y≡z hole = do
-    inner ← checkType unknown unknown
-    trans-tm ← `trans x inner y≡z
-    unify trans-tm hole
-    pure inner
-
   solveGoal : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Term → TC ⊤
   solveGoal x≡y hole = do
     goal ← inferType hole
@@ -246,6 +228,69 @@ private
     cong-tm ← `cong eqGoal cong-lam x≡y
     unify cong-tm hole
 
+  -- Associate each relation with its step function
+  module _ where
+    open import Relation.Binary.PropositionalEquality using (_≡_ ; trans)
+
+    go₁ : Name × Name
+    go₁ = quote _≡_ , quote trans
+
+  module _ where
+    open import Relation.Binary.Reasoning.Base.Single using (_IsRelatedTo_ ; ≡-go)
+
+    go₂ : Name × Name
+    go₂ = quote _IsRelatedTo_ , quote ≡-go
+
+  module _ where
+    open import Relation.Binary.Reasoning.Base.Double using (_IsRelatedTo_ ; ≡-go)
+
+    go₃ : Name × Name
+    go₃ = quote _IsRelatedTo_ , quote ≡-go
+
+  module _ where
+    open import Relation.Binary.Reasoning.Base.Triple using (_IsRelatedTo_ ; ≡-go)
+
+    go₄ : Name × Name
+    go₄ = quote _IsRelatedTo_ , quote ≡-go
+
+  goMap : List (Name × Name)
+  goMap = go₁ ∷ go₂ ∷ go₃ ∷ go₄ ∷ []
+
+  -- Map a relation to its step function
+  relToGo : Name → List (Name × Name) → TC Name
+  relToGo rel [] = typeError (strErr "cong! - unsupported relation: " ∷ nameErr rel ∷ [])
+  relToGo rel ((rel' , go) ∷ gos) = if rel' Name.≡ᵇ rel then pure go else relToGo rel gos
+
+  -- Drop the last two arguments to a relation, e.g., the x and y in x ≡ y
+  dropArgs : Args Term → TC (Args Term)
+  dropArgs (_ ∷ _ ∷ []) = pure []
+  dropArgs (a₁ ∷ a₂ ∷ a₃ ∷ as) = (a₁ ∷_) <$> dropArgs (a₂ ∷ a₃ ∷ as)
+  dropArgs _ = typeError (strErr "cong! - short argument list" ∷ [])
+
+  parseRel : Term → TC (Name × Args Term)
+  parseRel `yRz = inferType `yRz >>= λ where
+    (def rel args) → pure $ rel , args
+    term → typeError (strErr "cong! - not a relation: " ∷ termErr term ∷ [])
+
+  -- Construct an application of the given relation's step function
+  `go : ∀ {a r} {A : Set a} {R : Set r} → A → Term → R → TC Term
+  `go {a = a} {A = A} x inner yRz = do
+    `x ← quoteTC x
+    `yRz ← quoteTC yRz
+    rel , args ← parseRel `yRz
+    go ← relToGo rel goMap
+    args' ← dropArgs args
+    -- Assume that the step function has arguments args' followed by
+    -- {x} {y} {z} x≡y yRz. We skip {y} and {z}, which we don't know.
+    pure $ def go $ args' ++ `x ⟅∷⟆ inner ⟨∷⟩ `yRz ⟨∷⟩ []
+
+  makeGoal : ∀ {a r} {A : Set a} {R : Set r} → A → R → Term → TC Term
+  makeGoal x yRz outer = do
+    inner ← checkType unknown unknown
+    go-tm ← `go x inner yRz
+    unify go-tm outer
+    pure inner
+
 ------------------------------------------------------------------------
 -- Rewriting
 ------------------------------------------------------------------------
@@ -260,15 +305,15 @@ macro
     -- so normalising buys us nothing.
     withNormalisation false (solveGoal x≡y hole)
 
-  cong!-≡-⟫ : ∀ {a} {A : Set a} (x : A) {x' y' y z : A} → y ≡ z → x' ≡ y' → Term → TC ⊤
-  cong!-≡-⟫ x y≡z x'≡y' outer = withNormalisation false $
-    makeGoal x y≡z outer >>= solveGoal x'≡y'
+  cong!-≡-⟩ : ∀ {a r} {A : Set a} {R : Set r} {x' y' : A} → A → R → x' ≡ y' → Term → TC ⊤
+  cong!-≡-⟩ x yRz x'≡y' outer = withNormalisation false $ do
+    makeGoal x yRz outer >>= solveGoal x'≡y'
 
-  cong!-≡-⟪ : ∀ {a} {A : Set a} (x : A) {x' y' y z : A} → y ≡ z → y' ≡ x' → Term → TC ⊤
-  cong!-≡-⟪ x y≡z y'≡x' outer = withNormalisation false $
-    makeGoal x y≡z outer >>= solveGoal (sym y'≡x')
+  cong!-≡-⟨ : ∀ {a r} {A : Set a} {R : Set r} {x' y' : A} → A → R → y' ≡ x' → Term → TC ⊤
+  cong!-≡-⟨ x yRz y'≡x' outer = withNormalisation false $
+    makeGoal x yRz outer >>= solveGoal (sym y'≡x')
 
-infixr 2 cong!-≡-⟫ cong!-≡-⟪
+infixr 2 cong!-≡-⟩ cong!-≡-⟨
 
-syntax cong!-≡-⟫ x y≡z x'≡y' = x ≡⟪ x'≡y' ⟫ y≡z
-syntax cong!-≡-⟪ x y≡z y'≡x' = x ≡⟪ y'≡x' ⟪ y≡z
+syntax cong!-≡-⟩ x yRz x'≡y' = x ≡⟨! x'≡y' ⟩ yRz
+syntax cong!-≡-⟨ x yRz y'≡x' = x ≡⟨! y'≡x' ⟨ yRz

From ab4a102c147be4418a11f62da4a84ae3a249590d Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Mon, 11 Mar 2024 01:19:41 +0000
Subject: [PATCH 10/15] Clarifying comment.

---
 src/Tactic/Cong.agda | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index eab9045bb4..491b668012 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -282,6 +282,10 @@ private
     args' ← dropArgs args
     -- Assume that the step function has arguments args' followed by
     -- {x} {y} {z} x≡y yRz. We skip {y} and {z}, which we don't know.
+    -- We must specify {x}, because the x we have at hand had
+    -- normalisation inhibited and thus still contains the markers,
+    -- ⌞_⌟. If we let Agda figure out {x} instead, then any markers
+    -- would be lost.
     pure $ def go $ args' ++ `x ⟅∷⟆ inner ⟨∷⟩ `yRz ⟨∷⟩ []
 
   makeGoal : ∀ {a r} {A : Set a} {R : Set r} → A → R → Term → TC Term

From 0a73d756cfb8938c05a179ef45e2986cd7e12f88 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Mon, 11 Mar 2024 08:54:02 +0000
Subject: [PATCH 11/15] Slight performance boost.

---
 src/Tactic/Cong.agda | 27 +++++++++++++++++----------
 1 file changed, 17 insertions(+), 10 deletions(-)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 491b668012..091c6f74f0 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -26,7 +26,7 @@
 
 module Tactic.Cong where
 
-open import Function.Base using (_$_)
+open import Function.Base using (_$_ ; case_of_)
 
 open import Data.Bool.Base            using (true; false; if_then_else_; _∧_)
 open import Data.Char.Base   as Char  using (toℕ)
@@ -257,15 +257,17 @@ private
   goMap = go₁ ∷ go₂ ∷ go₃ ∷ go₄ ∷ []
 
   -- Map a relation to its step function
-  relToGo : Name → List (Name × Name) → TC Name
-  relToGo rel [] = typeError (strErr "cong! - unsupported relation: " ∷ nameErr rel ∷ [])
-  relToGo rel ((rel' , go) ∷ gos) = if rel' Name.≡ᵇ rel then pure go else relToGo rel gos
+  relToGo : Name → List (Name × Name) → Maybe Name
+  relToGo rel [] = nothing
+  relToGo rel ((rel' , go) ∷ gos) = if rel' Name.≡ᵇ rel then just go else relToGo rel gos
 
   -- Drop the last two arguments to a relation, e.g., the x and y in x ≡ y
-  dropArgs : Args Term → TC (Args Term)
-  dropArgs (_ ∷ _ ∷ []) = pure []
-  dropArgs (a₁ ∷ a₂ ∷ a₃ ∷ as) = (a₁ ∷_) <$> dropArgs (a₂ ∷ a₃ ∷ as)
-  dropArgs _ = typeError (strErr "cong! - short argument list" ∷ [])
+  dropArgs : Args Term → Maybe (Args Term)
+  dropArgs (_ ∷ _ ∷ []) = just []
+  dropArgs (a₁ ∷ a₂ ∷ a₃ ∷ as) = case dropArgs (a₂ ∷ a₃ ∷ as) of λ where
+    nothing → nothing
+    (just as') → just (a₁ ∷ as')
+  dropArgs _ = nothing
 
   parseRel : Term → TC (Name × Args Term)
   parseRel `yRz = inferType `yRz >>= λ where
@@ -278,8 +280,13 @@ private
     `x ← quoteTC x
     `yRz ← quoteTC yRz
     rel , args ← parseRel `yRz
-    go ← relToGo rel goMap
-    args' ← dropArgs args
+    -- Recursing in Maybe seems faster than recursing in TC.
+    go ← case relToGo rel goMap of λ where
+      nothing → typeError (strErr "cong! - short argument list" ∷ [])
+      (just go) → pure go
+    args' ← case dropArgs args of λ where
+      nothing → typeError (strErr "cong! - unsupported relation: " ∷ nameErr rel ∷ [])
+      (just args') → pure args'
     -- Assume that the step function has arguments args' followed by
     -- {x} {y} {z} x≡y yRz. We skip {y} and {z}, which we don't know.
     -- We must specify {x}, because the x we have at hand had

From 8b58264047a6bc795772c842f6e4108e172f60ce Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Fri, 15 Mar 2024 10:14:38 +0000
Subject: [PATCH 12/15] Go back to catchTC.

---
 doc/README/Tactic/Cong.agda |  10 ++--
 src/Tactic/Cong.agda        | 113 +++++-------------------------------
 2 files changed, 20 insertions(+), 103 deletions(-)

diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda
index eac29ec352..fc843d5e80 100644
--- a/doc/README/Tactic/Cong.agda
+++ b/doc/README/Tactic/Cong.agda
@@ -8,7 +8,7 @@ open import Data.Nat.Properties
 open import Relation.Binary.PropositionalEquality as Eq
 import Relation.Binary.Reasoning.Preorder as PR
 
-open import Tactic.Cong
+open import Tactic.Cong using (cong! ; ⌞_⌟)
 
 ----------------------------------------------------------------------
 -- Usage
@@ -77,10 +77,10 @@ marker-example₁ m n o p =
   let open Eq.≡-Reasoning in
   begin
     ⌞ m + n ⌟ + (o + p)
-  ≡⟨! +-comm m n ⟩
+  ≡⟨ cong! (+-comm m n) ⟩
     n + m + ⌞ o + p ⌟
-  ≡⟨! +-comm p o ⟨
-    n + m + (p + o)
+  ≡⟨ cong! (+-comm p o) ⟨
+     + m + (p + o)
   ∎
 
 marker-example₂ : ∀ m n → m + n + (m + n) ≡ n + m + (n + m)
@@ -88,7 +88,7 @@ marker-example₂ m n =
   let open ≤-Reasoning in
   begin-equality
     ⌞ m + n ⌟ + ⌞ m + n ⌟
-  ≡⟨! +-comm m n ⟩
+  ≡⟨ cong! (+-comm m n) ⟩
     n + m + (n + m)
   ∎
 
diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index 091c6f74f0..d29d2c6d1e 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -26,19 +26,19 @@
 
 module Tactic.Cong where
 
-open import Function.Base using (_$_ ; case_of_)
+open import Function.Base using (_$_)
 
 open import Data.Bool.Base            using (true; false; if_then_else_; _∧_)
 open import Data.Char.Base   as Char  using (toℕ)
 open import Data.Float.Base  as Float using (_≡ᵇ_)
-open import Data.List.Base   as List  using (List; []; _∷_; _++_)
+open import Data.List.Base   as List  using ([]; _∷_)
 open import Data.Maybe.Base  as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base    as ℕ     using (ℕ; zero; suc; _≡ᵇ_; _+_)
 open import Data.Unit.Base            using (⊤)
 open import Data.Word.Base   as Word  using (toℕ)
 open import Data.Product.Base         using (_×_; map₁; _,_)
 
-open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong ; sym)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the
 -- builtin for maximum speed.
@@ -220,87 +220,6 @@ private
   antiUnifyClauses ϕ _ _ =
     just []
 
-  solveGoal : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Term → TC ⊤
-  solveGoal x≡y hole = do
-    goal ← inferType hole
-    eqGoal ← destructEqualityGoal goal
-    let cong-lam = antiUnify 0 (EqualityGoal.lhs eqGoal) (EqualityGoal.rhs eqGoal)
-    cong-tm ← `cong eqGoal cong-lam x≡y
-    unify cong-tm hole
-
-  -- Associate each relation with its step function
-  module _ where
-    open import Relation.Binary.PropositionalEquality using (_≡_ ; trans)
-
-    go₁ : Name × Name
-    go₁ = quote _≡_ , quote trans
-
-  module _ where
-    open import Relation.Binary.Reasoning.Base.Single using (_IsRelatedTo_ ; ≡-go)
-
-    go₂ : Name × Name
-    go₂ = quote _IsRelatedTo_ , quote ≡-go
-
-  module _ where
-    open import Relation.Binary.Reasoning.Base.Double using (_IsRelatedTo_ ; ≡-go)
-
-    go₃ : Name × Name
-    go₃ = quote _IsRelatedTo_ , quote ≡-go
-
-  module _ where
-    open import Relation.Binary.Reasoning.Base.Triple using (_IsRelatedTo_ ; ≡-go)
-
-    go₄ : Name × Name
-    go₄ = quote _IsRelatedTo_ , quote ≡-go
-
-  goMap : List (Name × Name)
-  goMap = go₁ ∷ go₂ ∷ go₃ ∷ go₄ ∷ []
-
-  -- Map a relation to its step function
-  relToGo : Name → List (Name × Name) → Maybe Name
-  relToGo rel [] = nothing
-  relToGo rel ((rel' , go) ∷ gos) = if rel' Name.≡ᵇ rel then just go else relToGo rel gos
-
-  -- Drop the last two arguments to a relation, e.g., the x and y in x ≡ y
-  dropArgs : Args Term → Maybe (Args Term)
-  dropArgs (_ ∷ _ ∷ []) = just []
-  dropArgs (a₁ ∷ a₂ ∷ a₃ ∷ as) = case dropArgs (a₂ ∷ a₃ ∷ as) of λ where
-    nothing → nothing
-    (just as') → just (a₁ ∷ as')
-  dropArgs _ = nothing
-
-  parseRel : Term → TC (Name × Args Term)
-  parseRel `yRz = inferType `yRz >>= λ where
-    (def rel args) → pure $ rel , args
-    term → typeError (strErr "cong! - not a relation: " ∷ termErr term ∷ [])
-
-  -- Construct an application of the given relation's step function
-  `go : ∀ {a r} {A : Set a} {R : Set r} → A → Term → R → TC Term
-  `go {a = a} {A = A} x inner yRz = do
-    `x ← quoteTC x
-    `yRz ← quoteTC yRz
-    rel , args ← parseRel `yRz
-    -- Recursing in Maybe seems faster than recursing in TC.
-    go ← case relToGo rel goMap of λ where
-      nothing → typeError (strErr "cong! - short argument list" ∷ [])
-      (just go) → pure go
-    args' ← case dropArgs args of λ where
-      nothing → typeError (strErr "cong! - unsupported relation: " ∷ nameErr rel ∷ [])
-      (just args') → pure args'
-    -- Assume that the step function has arguments args' followed by
-    -- {x} {y} {z} x≡y yRz. We skip {y} and {z}, which we don't know.
-    -- We must specify {x}, because the x we have at hand had
-    -- normalisation inhibited and thus still contains the markers,
-    -- ⌞_⌟. If we let Agda figure out {x} instead, then any markers
-    -- would be lost.
-    pure $ def go $ args' ++ `x ⟅∷⟆ inner ⟨∷⟩ `yRz ⟨∷⟩ []
-
-  makeGoal : ∀ {a r} {A : Set a} {R : Set r} → A → R → Term → TC Term
-  makeGoal x yRz outer = do
-    inner ← checkType unknown unknown
-    go-tm ← `go x inner yRz
-    unify go-tm outer
-    pure inner
 
 ------------------------------------------------------------------------
 -- Rewriting
@@ -314,17 +233,15 @@ macro
     -- the endpoints of the equality are already specified in
     -- the form that the -- programmer expects them to be in,
     -- so normalising buys us nothing.
-    withNormalisation false (solveGoal x≡y hole)
-
-  cong!-≡-⟩ : ∀ {a r} {A : Set a} {R : Set r} {x' y' : A} → A → R → x' ≡ y' → Term → TC ⊤
-  cong!-≡-⟩ x yRz x'≡y' outer = withNormalisation false $ do
-    makeGoal x yRz outer >>= solveGoal x'≡y'
-
-  cong!-≡-⟨ : ∀ {a r} {A : Set a} {R : Set r} {x' y' : A} → A → R → y' ≡ x' → Term → TC ⊤
-  cong!-≡-⟨ x yRz y'≡x' outer = withNormalisation false $
-    makeGoal x yRz outer >>= solveGoal (sym y'≡x')
-
-infixr 2 cong!-≡-⟩ cong!-≡-⟨
-
-syntax cong!-≡-⟩ x yRz x'≡y' = x ≡⟨! x'≡y' ⟩ yRz
-syntax cong!-≡-⟨ x yRz y'≡x' = x ≡⟨! y'≡x' ⟨ yRz
+    withNormalisation false $ do
+      goal ← inferType hole
+      eqGoal ← destructEqualityGoal goal
+      let uni = λ lhs rhs → do
+        let cong-lam = antiUnify 0 lhs rhs
+        cong-tm ← `cong eqGoal cong-lam x≡y
+        unify cong-tm hole
+      let lhs = EqualityGoal.lhs eqGoal
+      let rhs = EqualityGoal.rhs eqGoal
+      -- When using ⌞_⌟ with ≡˘⟨ ... ⟩, (uni lhs rhs) fails and
+      -- (uni rhs lhs) succeeds.
+      catchTC (uni lhs rhs) (uni rhs lhs)

From b26ca089914611042477370d6042e4512c1f88ae Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Fri, 15 Mar 2024 16:19:10 +0000
Subject: [PATCH 13/15] Fix example after merge.

---
 doc/README/Tactic/Cong.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda
index b496abea98..c80a2e1c16 100644
--- a/doc/README/Tactic/Cong.agda
+++ b/doc/README/Tactic/Cong.agda
@@ -74,13 +74,13 @@ succinct-example m n eq =
 
 marker-example₁ : ∀ m n o p → m + n + (o + p) ≡ n + m + (p + o)
 marker-example₁ m n o p =
-  let open Eq.≡-Reasoning in
+  let open ≡-Reasoning in
   begin
     ⌞ m + n ⌟ + (o + p)
   ≡⟨ cong! (+-comm m n) ⟩
     n + m + ⌞ o + p ⌟
   ≡⟨ cong! (+-comm p o) ⟨
-     + m + (p + o)
+    n + m + (p + o)
   ∎
 
 marker-example₂ : ∀ m n → m + n + (m + n) ≡ n + m + (n + m)

From 71812c172dcbc909269c942346d26918b277ca44 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Fri, 15 Mar 2024 16:35:20 +0000
Subject: [PATCH 14/15] Use renamed backward step.

---
 src/Tactic/Cong.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda
index d29d2c6d1e..0259191800 100644
--- a/src/Tactic/Cong.agda
+++ b/src/Tactic/Cong.agda
@@ -242,6 +242,6 @@ macro
         unify cong-tm hole
       let lhs = EqualityGoal.lhs eqGoal
       let rhs = EqualityGoal.rhs eqGoal
-      -- When using ⌞_⌟ with ≡˘⟨ ... ⟩, (uni lhs rhs) fails and
+      -- When using ⌞_⌟ with ≡⟨ ... ⟨, (uni lhs rhs) fails and
       -- (uni rhs lhs) succeeds.
       catchTC (uni lhs rhs) (uni rhs lhs)

From 6756add8aacb671242e1fb0ee5c7eec9f153d475 Mon Sep 17 00:00:00 2001
From: Thomas Lopatic <thomas@lopatic.de>
Date: Sat, 16 Mar 2024 17:51:16 +0000
Subject: [PATCH 15/15] Language tweaks.

---
 CHANGELOG.md                | 2 +-
 doc/README/Tactic/Cong.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6442181f60..7694de59c0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -283,4 +283,4 @@ Additions to existing modules
   ```
 
 * `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
-  anti-unification.
+  anti-unification. See README.Tactic.Cong for details.
diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda
index c80a2e1c16..f6adfe9f9f 100644
--- a/doc/README/Tactic/Cong.agda
+++ b/doc/README/Tactic/Cong.agda
@@ -56,7 +56,7 @@ succinct-example m n eq =
   ∎
 
 ----------------------------------------------------------------------
--- Limitations
+-- Explicit markings
 ----------------------------------------------------------------------
 
 -- The 'cong!' tactic can handle simple cases, but will