From 887d5cd868e0faef32f9df5a6a16214d85034cf6 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 15 Dec 2021 20:35:57 -0800
Subject: [PATCH 01/11] Export primitive name + meta equality from Reflection

---
 src/Reflection/AlphaEquality.agda | 12 ++++++------
 src/Reflection/Meta.agda          |  2 +-
 src/Reflection/Name.agda          |  2 +-
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/Reflection/AlphaEquality.agda b/src/Reflection/AlphaEquality.agda
index 73d90a5a55..4360e31298 100644
--- a/src/Reflection/AlphaEquality.agda
+++ b/src/Reflection/AlphaEquality.agda
@@ -106,7 +106,7 @@ mutual
   (arg i a) =α=-ArgPattern (arg i′ a′) = a =α=-Pattern a′
 
   _=α=-Term_ : Term → Term → Bool
-  (var     x  args) =α=-Term (var     x′  args′) = (x  ≡ᵇ  x′)  ∧ (args =α=-ArgsTerm args′)
+  (var     x  args) =α=-Term (var     x′  args′) = (x  ℕ.≡ᵇ  x′)  ∧ (args =α=-ArgsTerm args′)
   (con     c  args) =α=-Term (con     c′  args′) = (c  =α= c′)  ∧ (args =α=-ArgsTerm args′)
   (def     f  args) =α=-Term (def     f′  args′) = (f  =α= f′)  ∧ (args =α=-ArgsTerm args′)
   (meta    x  args) =α=-Term (meta     x′ args′) = (x  =α= x′)  ∧ (args =α=-ArgsTerm args′)
@@ -210,10 +210,10 @@ mutual
 
   _=α=-Sort_ : Sort → Sort → Bool
   (set t    ) =α=-Sort (set t′    ) = t =α=-Term t′
-  (lit n    ) =α=-Sort (lit n′    ) = n ≡ᵇ n′
+  (lit n    ) =α=-Sort (lit n′    ) = n ℕ.≡ᵇ n′
   (prop t   ) =α=-Sort (prop t′   ) = t =α=-Term t′
-  (propLit n) =α=-Sort (propLit n′) = n ≡ᵇ n′
-  (inf n    ) =α=-Sort (inf n′    ) = n ≡ᵇ n′
+  (propLit n) =α=-Sort (propLit n′) = n ℕ.≡ᵇ n′
+  (inf n    ) =α=-Sort (inf n′    ) = n ℕ.≡ᵇ n′
   (unknown  ) =α=-Sort (unknown   ) = true
 
   (set _    ) =α=-Sort (lit _    ) = false
@@ -267,11 +267,11 @@ mutual
 
   _=α=-Pattern_ : Pattern → Pattern → Bool
   (con c ps) =α=-Pattern (con c′ ps′) = (c =α= c′) ∧ (ps =α=-ArgsPattern ps′)
-  (var x   ) =α=-Pattern (var x′    ) = x ≡ᵇ x′
+  (var x   ) =α=-Pattern (var x′    ) = x ℕ.≡ᵇ x′
   (lit l   ) =α=-Pattern (lit l′    ) = l =α= l′
   (proj a  ) =α=-Pattern (proj a′   ) = a =α= a′
   (dot t   ) =α=-Pattern (dot t′    ) = t =α=-Term t′
-  (absurd x) =α=-Pattern (absurd x′ ) = x ≡ᵇ x′
+  (absurd x) =α=-Pattern (absurd x′ ) = x ℕ.≡ᵇ x′
 
   (con x x₁) =α=-Pattern (dot x₂    ) = false
   (con x x₁) =α=-Pattern (var x₂    ) = false
diff --git a/src/Reflection/Meta.agda b/src/Reflection/Meta.agda
index 46fe960e29..f0ced0fed3 100644
--- a/src/Reflection/Meta.agda
+++ b/src/Reflection/Meta.agda
@@ -16,7 +16,7 @@ import Relation.Binary.Construct.On as On
 open import Relation.Binary.PropositionalEquality
 
 open import Agda.Builtin.Reflection public
-  using (Meta) renaming (primMetaToNat to toℕ)
+  using (Meta) renaming (primMetaToNat to toℕ; primMetaEquality to _≡ᵇ_)
 
 open import Agda.Builtin.Reflection.Properties public
   renaming (primMetaToNatInjective to toℕ-injective)
diff --git a/src/Reflection/Name.agda b/src/Reflection/Name.agda
index 26b579ea41..723ca0c619 100644
--- a/src/Reflection/Name.agda
+++ b/src/Reflection/Name.agda
@@ -21,7 +21,7 @@ open import Relation.Binary.PropositionalEquality
 -- Re-export built-ins
 
 open import Agda.Builtin.Reflection public
-  using (Name) renaming (primQNameToWord64s to toWords)
+  using (Name) renaming (primQNameToWord64s to toWords; primQNameEquality to _≡ᵇ_)
 
 open import Agda.Builtin.Reflection.Properties public
   renaming (primQNameToWord64sInjective to toWords-injective)

From b9d58e5a5a7219a8616d976d756ca5e011d6dbb3 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 15 Dec 2021 20:36:33 -0800
Subject: [PATCH 02/11] Implement the 'rw' tactic

---
 src/Tactic/Rewrite.agda | 177 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 177 insertions(+)
 create mode 100644 src/Tactic/Rewrite.agda

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
new file mode 100644
index 0000000000..35c80570ec
--- /dev/null
+++ b/src/Tactic/Rewrite.agda
@@ -0,0 +1,177 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A simple tactic for used to automatically compute the function
+-- argument to cong.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Tactic.Rewrite where
+
+open import Function 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.Maybe.Base  as Maybe using (Maybe; just; nothing)
+open import Data.Nat.Base    as Nat   using (ℕ; zero; suc; _≡ᵇ_; _+_)
+open import Data.Unit.Base            using (⊤)
+open import Data.Word.Base   as Word  using (toℕ)
+open import Data.Product
+
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+
+-- 'Data.String.Properties' defines this via 'Dec', so let's use the builtin
+-- for maximum speed.
+import Agda.Builtin.String as String renaming (primStringEquality to _≡ᵇ_)
+
+open import Reflection
+open import Reflection.Abstraction
+open import Reflection.AlphaEquality        as Alpha
+open import Reflection.Argument             as Arg
+open import Reflection.Argument.Information as ArgInfo
+open import Reflection.Argument.Visibility  as Visibility
+open import Reflection.Meta                 as Meta
+open import Reflection.Name                 as Name
+open import Reflection.Term                 as Term
+
+open import Reflection.TypeChecking.Monad.Syntax
+
+----------------------------------------------------------------------
+-- Utilities
+----------------------------------------------------------------------
+
+private
+  -- Determine the number of variables a pattern binds
+  pattern-bindings : Pattern → ℕ
+  patterns-bindings : Args Pattern → ℕ
+
+  pattern-bindings (con _ ps) = suc (patterns-bindings ps)
+  pattern-bindings (dot t)    = 0
+  pattern-bindings (var x)    = 1
+  pattern-bindings (lit l)    = 0
+  pattern-bindings (proj f)   = 1
+  pattern-bindings (absurd x) = 0
+
+  patterns-bindings [] = 0
+  patterns-bindings (arg i pat ∷ pats) = pattern-bindings pat + patterns-bindings pats
+
+  -- Helper for constructing applications of 'cong'
+  `cong : Term → Term → Term
+  `cong f eq = def (quote cong) (4 ⋯⟅∷⟆ vArg (lam visible (abs "ϕ" f)) ∷ 2 ⋯⟅∷⟆ vArg eq ∷ [])
+
+  -- Construct an error when the goal is not 'x ≡ y' for some 'x' and 'y'.
+  not-equality-error : ∀ {A : Set} Term → TC A
+  not-equality-error goal = typeError (strErr "Cannot rewrite a goal that is not equality: " ∷ termErr goal ∷ [])
+
+  -- Extract out both endpoints of an equality type.
+  endpoints : Term → TC (Term × Term)
+  endpoints goal@(def x (lvl ∷ tp ∷ (arg _ e0) ∷ (arg _ e1) ∷ [])) =
+    if x Name.≡ᵇ (quote _≡_) then return (e0 , e1) else not-equality-error goal 
+  endpoints goal = not-equality-error goal 
+
+----------------------------------------------------------------------
+-- Anti-Unification
+----------------------------------------------------------------------
+
+anti-unify : ℕ → Term → Term → Term
+anti-unify-args : ℕ → Args Term → Args Term → Maybe (Args Term)
+anti-unify-clauses : ℕ → Clauses → Clauses → Maybe Clauses
+anti-unify-clause : ℕ → Clause → Clause → Maybe Clause
+
+anti-unify ϕ (var x args) (var y args') with x Nat.≡ᵇ y | anti-unify-args ϕ args args'
+... | _     | nothing    = var ϕ []
+... | false | just uargs = var ϕ uargs
+... | true  | just uargs = var x uargs
+anti-unify ϕ (con c args) (con c' args') with c Name.≡ᵇ c' | anti-unify-args ϕ args args'
+... | _     | nothing    = var ϕ []
+... | false | just uargs = var ϕ []
+... | true  | just uargs = con c uargs
+anti-unify ϕ (def f args) (def f' args') with f Name.≡ᵇ f' | anti-unify-args ϕ args args'
+... | _     | nothing    = var ϕ []
+... | false | just uargs = var ϕ []
+... | true  | just uargs = def f uargs
+anti-unify ϕ (lam v (abs s t)) (lam _ (abs _ t')) =
+  lam v (abs s (anti-unify (suc ϕ) t t'))
+anti-unify ϕ (pat-lam cs args) (pat-lam cs' args') with anti-unify-clauses ϕ cs cs' | anti-unify-args ϕ args args'
+... | nothing  | _       = var ϕ []
+... | _        | nothing = var ϕ []
+... | just ucs | just uargs = pat-lam ucs uargs
+anti-unify ϕ (Π[ s ∶ arg i a ] b) (Π[ _ ∶ arg _ a' ] b') =
+  Π[ s ∶ arg i (anti-unify ϕ a a') ] anti-unify (suc ϕ) b b'
+anti-unify ϕ (sort (set t)) (sort (set t')) =
+  sort (set (anti-unify ϕ t t'))
+anti-unify ϕ (sort (lit n)) (sort (lit n')) with n Nat.≡ᵇ n'
+... | true  = sort (lit n)
+... | false = var ϕ []
+anti-unify ϕ (sort (prop t)) (sort (prop t')) =
+  sort (prop (anti-unify ϕ t t'))
+anti-unify ϕ (sort (propLit n)) (sort (propLit n')) with n Nat.≡ᵇ n'
+... | true  = sort (propLit n)
+... | false = var ϕ []
+anti-unify ϕ (sort (inf n)) (sort (inf n')) with n Nat.≡ᵇ n'
+... | true  = sort (inf n)
+... | false = var ϕ []
+anti-unify ϕ (sort unknown) (sort unknown) =
+  sort unknown
+anti-unify ϕ (lit (nat n)) (lit (nat n')) with n Nat.≡ᵇ n'
+... | true  = lit (nat n)
+... | false = var ϕ []
+anti-unify ϕ (lit (word64 n)) (lit (word64 n')) with Word.toℕ n Nat.≡ᵇ Word.toℕ n'
+... | true  = lit (word64 n)
+... | false = var ϕ []
+anti-unify ϕ (lit (float x)) (lit (float x')) with x Float.≡ᵇ x'
+... | true  = lit (float x)
+... | false = var ϕ []
+anti-unify ϕ (lit (char c)) (lit (char c')) with Char.toℕ c Nat.≡ᵇ Char.toℕ c'
+... | true  = lit (char c)
+... | false = var ϕ []
+anti-unify ϕ (lit (string s)) (lit (string s')) with s String.≡ᵇ s'
+... | true = lit (string s)
+... | false = var ϕ []
+anti-unify ϕ (lit (name x)) (lit (name x')) with x Name.≡ᵇ x'
+... | true  = lit (name x)
+... | false = var ϕ []
+anti-unify ϕ (lit (meta x)) (lit (meta x')) with x Meta.≡ᵇ x'
+... | true = lit (meta x)
+... | false = var ϕ []
+anti-unify ϕ (meta x args) (meta x' args') with x Meta.≡ᵇ x' | anti-unify-args ϕ args args'
+... | _     | nothing    = var ϕ []
+... | false | _          = var ϕ []
+... | true  | just uargs = meta x uargs
+anti-unify ϕ unknown unknown = unknown
+anti-unify ϕ _ _ = var ϕ []
+
+anti-unify-args ϕ (arg i t ∷ args) (arg _ t' ∷ args') =
+  Maybe.map (arg i (anti-unify ϕ t t') ∷_) (anti-unify-args ϕ args args')
+anti-unify-args ϕ [] [] =
+  just []
+anti-unify-args ϕ _ _ =
+  nothing
+
+anti-unify-clause ϕ (clause Γ pats t) (clause Δ pats' t') =
+  Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (clause Γ pats (anti-unify (ϕ + patterns-bindings pats) t t'))
+anti-unify-clause ϕ (absurd-clause Γ pats) (absurd-clause Δ pats') =
+  Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (absurd-clause Γ pats)
+anti-unify-clause ϕ _ _ =
+  nothing
+
+anti-unify-clauses ϕ (c ∷ cs) (c' ∷ cs') =
+  Maybe.ap (Maybe.map _∷_ (anti-unify-clause ϕ c c')) (anti-unify-clauses ϕ cs cs')
+anti-unify-clauses ϕ _ _ =
+  just []
+
+
+----------------------------------------------------------------------
+-- Rewriting
+----------------------------------------------------------------------
+
+macro
+  rw : Term → Term → TC ⊤
+  rw eq hole = withNormalisation false $ do
+    goal ← inferType hole
+    (e0 , e1) ← endpoints goal
+    let f = anti-unify 0 e0 e1
+    unify (`cong f eq) hole

From 7606a693e5028d10f60073a667b9fa460a9953d5 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 15 Dec 2021 20:46:27 -0800
Subject: [PATCH 03/11] Document `Tactic.Rewrite`

---
 src/Tactic/Rewrite.agda | 41 ++++++++++++++++++++++++++++++++++++-----
 1 file changed, 36 insertions(+), 5 deletions(-)

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
index 35c80570ec..0b2326485a 100644
--- a/src/Tactic/Rewrite.agda
+++ b/src/Tactic/Rewrite.agda
@@ -3,6 +3,21 @@
 --
 -- A simple tactic for used to automatically compute the function
 -- argument to cong.
+--
+-- The main use for this tactic is getting a similar experience to
+-- 'rewrite' during equational reasoning. This allows us to write very
+-- succinct proofs:
+--
+-- example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
+-- example m n eq = begin
+--     suc (suc (m + 0)) + m
+--   ≡⟨ rw (+-identityʳ m) ⟩
+--     suc (suc m) + m
+--   ≡⟨ rw eq ⟩
+--     suc (suc n) + n
+--   ≡˘⟨ rw (+-identityʳ n) ⟩
+--     suc (suc n) + (n + 0)
+--   ∎
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -74,6 +89,16 @@ private
 
 ----------------------------------------------------------------------
 -- Anti-Unification
+--
+-- The core idea of the tactic is that we can compute the input
+-- to 'cong' by syntactically anti-unifying both sides of the
+-- equality, and then using that to construct a lambda
+-- where all the differences are replaced by the lambda-abstracted
+-- variable.
+--
+-- For instance, the two terms 'suc (m + (m + 0)) + (m + 0)' and
+-- 'suc (m + m) + (m + 0)' would anti unify to 'suc (m + _) + (m + 0)'
+-- which we can then use to construct the lambda 'λ ϕ → suc (m + ϕ) + (m + 0)'.
 ----------------------------------------------------------------------
 
 anti-unify : ℕ → Term → Term → Term
@@ -170,8 +195,14 @@ anti-unify-clauses ϕ _ _ =
 
 macro
   rw : Term → Term → TC ⊤
-  rw eq hole = withNormalisation false $ do
-    goal ← inferType hole
-    (e0 , e1) ← endpoints goal
-    let f = anti-unify 0 e0 e1
-    unify (`cong f eq) hole
+  rw eq hole =
+    -- NOTE: We avoid doing normalisation here as this tactic
+    -- is mainly meant for equational reasoning. In that context,
+    -- the endpoints 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
+      (e0 , e1) ← endpoints goal
+      let f = anti-unify 0 e0 e1
+      unify (`cong f eq) hole

From 0252726a592669b61598dbc1e88b1cc48f3d99e1 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 15 Dec 2021 20:48:06 -0800
Subject: [PATCH 04/11] Make Anti-Unification code private in `Tactic.Rewrite`

---
 src/Tactic/Rewrite.agda | 173 ++++++++++++++++++++--------------------
 1 file changed, 87 insertions(+), 86 deletions(-)

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
index 0b2326485a..b0d8293dfa 100644
--- a/src/Tactic/Rewrite.agda
+++ b/src/Tactic/Rewrite.agda
@@ -101,92 +101,93 @@ private
 -- which we can then use to construct the lambda 'λ ϕ → suc (m + ϕ) + (m + 0)'.
 ----------------------------------------------------------------------
 
-anti-unify : ℕ → Term → Term → Term
-anti-unify-args : ℕ → Args Term → Args Term → Maybe (Args Term)
-anti-unify-clauses : ℕ → Clauses → Clauses → Maybe Clauses
-anti-unify-clause : ℕ → Clause → Clause → Maybe Clause
-
-anti-unify ϕ (var x args) (var y args') with x Nat.≡ᵇ y | anti-unify-args ϕ args args'
-... | _     | nothing    = var ϕ []
-... | false | just uargs = var ϕ uargs
-... | true  | just uargs = var x uargs
-anti-unify ϕ (con c args) (con c' args') with c Name.≡ᵇ c' | anti-unify-args ϕ args args'
-... | _     | nothing    = var ϕ []
-... | false | just uargs = var ϕ []
-... | true  | just uargs = con c uargs
-anti-unify ϕ (def f args) (def f' args') with f Name.≡ᵇ f' | anti-unify-args ϕ args args'
-... | _     | nothing    = var ϕ []
-... | false | just uargs = var ϕ []
-... | true  | just uargs = def f uargs
-anti-unify ϕ (lam v (abs s t)) (lam _ (abs _ t')) =
-  lam v (abs s (anti-unify (suc ϕ) t t'))
-anti-unify ϕ (pat-lam cs args) (pat-lam cs' args') with anti-unify-clauses ϕ cs cs' | anti-unify-args ϕ args args'
-... | nothing  | _       = var ϕ []
-... | _        | nothing = var ϕ []
-... | just ucs | just uargs = pat-lam ucs uargs
-anti-unify ϕ (Π[ s ∶ arg i a ] b) (Π[ _ ∶ arg _ a' ] b') =
-  Π[ s ∶ arg i (anti-unify ϕ a a') ] anti-unify (suc ϕ) b b'
-anti-unify ϕ (sort (set t)) (sort (set t')) =
-  sort (set (anti-unify ϕ t t'))
-anti-unify ϕ (sort (lit n)) (sort (lit n')) with n Nat.≡ᵇ n'
-... | true  = sort (lit n)
-... | false = var ϕ []
-anti-unify ϕ (sort (prop t)) (sort (prop t')) =
-  sort (prop (anti-unify ϕ t t'))
-anti-unify ϕ (sort (propLit n)) (sort (propLit n')) with n Nat.≡ᵇ n'
-... | true  = sort (propLit n)
-... | false = var ϕ []
-anti-unify ϕ (sort (inf n)) (sort (inf n')) with n Nat.≡ᵇ n'
-... | true  = sort (inf n)
-... | false = var ϕ []
-anti-unify ϕ (sort unknown) (sort unknown) =
-  sort unknown
-anti-unify ϕ (lit (nat n)) (lit (nat n')) with n Nat.≡ᵇ n'
-... | true  = lit (nat n)
-... | false = var ϕ []
-anti-unify ϕ (lit (word64 n)) (lit (word64 n')) with Word.toℕ n Nat.≡ᵇ Word.toℕ n'
-... | true  = lit (word64 n)
-... | false = var ϕ []
-anti-unify ϕ (lit (float x)) (lit (float x')) with x Float.≡ᵇ x'
-... | true  = lit (float x)
-... | false = var ϕ []
-anti-unify ϕ (lit (char c)) (lit (char c')) with Char.toℕ c Nat.≡ᵇ Char.toℕ c'
-... | true  = lit (char c)
-... | false = var ϕ []
-anti-unify ϕ (lit (string s)) (lit (string s')) with s String.≡ᵇ s'
-... | true = lit (string s)
-... | false = var ϕ []
-anti-unify ϕ (lit (name x)) (lit (name x')) with x Name.≡ᵇ x'
-... | true  = lit (name x)
-... | false = var ϕ []
-anti-unify ϕ (lit (meta x)) (lit (meta x')) with x Meta.≡ᵇ x'
-... | true = lit (meta x)
-... | false = var ϕ []
-anti-unify ϕ (meta x args) (meta x' args') with x Meta.≡ᵇ x' | anti-unify-args ϕ args args'
-... | _     | nothing    = var ϕ []
-... | false | _          = var ϕ []
-... | true  | just uargs = meta x uargs
-anti-unify ϕ unknown unknown = unknown
-anti-unify ϕ _ _ = var ϕ []
-
-anti-unify-args ϕ (arg i t ∷ args) (arg _ t' ∷ args') =
-  Maybe.map (arg i (anti-unify ϕ t t') ∷_) (anti-unify-args ϕ args args')
-anti-unify-args ϕ [] [] =
-  just []
-anti-unify-args ϕ _ _ =
-  nothing
-
-anti-unify-clause ϕ (clause Γ pats t) (clause Δ pats' t') =
-  Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (clause Γ pats (anti-unify (ϕ + patterns-bindings pats) t t'))
-anti-unify-clause ϕ (absurd-clause Γ pats) (absurd-clause Δ pats') =
-  Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (absurd-clause Γ pats)
-anti-unify-clause ϕ _ _ =
-  nothing
-
-anti-unify-clauses ϕ (c ∷ cs) (c' ∷ cs') =
-  Maybe.ap (Maybe.map _∷_ (anti-unify-clause ϕ c c')) (anti-unify-clauses ϕ cs cs')
-anti-unify-clauses ϕ _ _ =
-  just []
+private
+  anti-unify : ℕ → Term → Term → Term
+  anti-unify-args : ℕ → Args Term → Args Term → Maybe (Args Term)
+  anti-unify-clauses : ℕ → Clauses → Clauses → Maybe Clauses
+  anti-unify-clause : ℕ → Clause → Clause → Maybe Clause
+  
+  anti-unify ϕ (var x args) (var y args') with x Nat.≡ᵇ y | anti-unify-args ϕ args args'
+  ... | _     | nothing    = var ϕ []
+  ... | false | just uargs = var ϕ uargs
+  ... | true  | just uargs = var x uargs
+  anti-unify ϕ (con c args) (con c' args') with c Name.≡ᵇ c' | anti-unify-args ϕ args args'
+  ... | _     | nothing    = var ϕ []
+  ... | false | just uargs = var ϕ []
+  ... | true  | just uargs = con c uargs
+  anti-unify ϕ (def f args) (def f' args') with f Name.≡ᵇ f' | anti-unify-args ϕ args args'
+  ... | _     | nothing    = var ϕ []
+  ... | false | just uargs = var ϕ []
+  ... | true  | just uargs = def f uargs
+  anti-unify ϕ (lam v (abs s t)) (lam _ (abs _ t')) =
+    lam v (abs s (anti-unify (suc ϕ) t t'))
+  anti-unify ϕ (pat-lam cs args) (pat-lam cs' args') with anti-unify-clauses ϕ cs cs' | anti-unify-args ϕ args args'
+  ... | nothing  | _       = var ϕ []
+  ... | _        | nothing = var ϕ []
+  ... | just ucs | just uargs = pat-lam ucs uargs
+  anti-unify ϕ (Π[ s ∶ arg i a ] b) (Π[ _ ∶ arg _ a' ] b') =
+    Π[ s ∶ arg i (anti-unify ϕ a a') ] anti-unify (suc ϕ) b b'
+  anti-unify ϕ (sort (set t)) (sort (set t')) =
+    sort (set (anti-unify ϕ t t'))
+  anti-unify ϕ (sort (lit n)) (sort (lit n')) with n Nat.≡ᵇ n'
+  ... | true  = sort (lit n)
+  ... | false = var ϕ []
+  anti-unify ϕ (sort (prop t)) (sort (prop t')) =
+    sort (prop (anti-unify ϕ t t'))
+  anti-unify ϕ (sort (propLit n)) (sort (propLit n')) with n Nat.≡ᵇ n'
+  ... | true  = sort (propLit n)
+  ... | false = var ϕ []
+  anti-unify ϕ (sort (inf n)) (sort (inf n')) with n Nat.≡ᵇ n'
+  ... | true  = sort (inf n)
+  ... | false = var ϕ []
+  anti-unify ϕ (sort unknown) (sort unknown) =
+    sort unknown
+  anti-unify ϕ (lit (nat n)) (lit (nat n')) with n Nat.≡ᵇ n'
+  ... | true  = lit (nat n)
+  ... | false = var ϕ []
+  anti-unify ϕ (lit (word64 n)) (lit (word64 n')) with Word.toℕ n Nat.≡ᵇ Word.toℕ n'
+  ... | true  = lit (word64 n)
+  ... | false = var ϕ []
+  anti-unify ϕ (lit (float x)) (lit (float x')) with x Float.≡ᵇ x'
+  ... | true  = lit (float x)
+  ... | false = var ϕ []
+  anti-unify ϕ (lit (char c)) (lit (char c')) with Char.toℕ c Nat.≡ᵇ Char.toℕ c'
+  ... | true  = lit (char c)
+  ... | false = var ϕ []
+  anti-unify ϕ (lit (string s)) (lit (string s')) with s String.≡ᵇ s'
+  ... | true = lit (string s)
+  ... | false = var ϕ []
+  anti-unify ϕ (lit (name x)) (lit (name x')) with x Name.≡ᵇ x'
+  ... | true  = lit (name x)
+  ... | false = var ϕ []
+  anti-unify ϕ (lit (meta x)) (lit (meta x')) with x Meta.≡ᵇ x'
+  ... | true = lit (meta x)
+  ... | false = var ϕ []
+  anti-unify ϕ (meta x args) (meta x' args') with x Meta.≡ᵇ x' | anti-unify-args ϕ args args'
+  ... | _     | nothing    = var ϕ []
+  ... | false | _          = var ϕ []
+  ... | true  | just uargs = meta x uargs
+  anti-unify ϕ unknown unknown = unknown
+  anti-unify ϕ _ _ = var ϕ []
+  
+  anti-unify-args ϕ (arg i t ∷ args) (arg _ t' ∷ args') =
+    Maybe.map (arg i (anti-unify ϕ t t') ∷_) (anti-unify-args ϕ args args')
+  anti-unify-args ϕ [] [] =
+    just []
+  anti-unify-args ϕ _ _ =
+    nothing
+  
+  anti-unify-clause ϕ (clause Γ pats t) (clause Δ pats' t') =
+    Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (clause Γ pats (anti-unify (ϕ + patterns-bindings pats) t t'))
+  anti-unify-clause ϕ (absurd-clause Γ pats) (absurd-clause Δ pats') =
+    Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (absurd-clause Γ pats)
+  anti-unify-clause ϕ _ _ =
+    nothing
+  
+  anti-unify-clauses ϕ (c ∷ cs) (c' ∷ cs') =
+    Maybe.ap (Maybe.map _∷_ (anti-unify-clause ϕ c c')) (anti-unify-clauses ϕ cs cs')
+  anti-unify-clauses ϕ _ _ =
+    just []
 
 
 ----------------------------------------------------------------------

From b67f55468814b8591986f6e339fa46e78a989e51 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 15 Dec 2021 21:20:50 -0800
Subject: [PATCH 05/11] Handle DeBruijin arithmetic correctly in
 `Tactic.Rewrite`

---
 src/Tactic/Rewrite.agda | 62 ++++++++++++++++++++++++++++++-----------
 1 file changed, 45 insertions(+), 17 deletions(-)

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
index b0d8293dfa..3d4f7af0aa 100644
--- a/src/Tactic/Rewrite.agda
+++ b/src/Tactic/Rewrite.agda
@@ -36,7 +36,7 @@ open import Data.Unit.Base            using (⊤)
 open import Data.Word.Base   as Word  using (toℕ)
 open import Data.Product
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the builtin
 -- for maximum speed.
@@ -59,19 +59,29 @@ open import Reflection.TypeChecking.Monad.Syntax
 ----------------------------------------------------------------------
 
 private
-  -- Determine the number of variables a pattern binds
-  pattern-bindings : Pattern → ℕ
-  patterns-bindings : Args Pattern → ℕ
-
-  pattern-bindings (con _ ps) = suc (patterns-bindings ps)
-  pattern-bindings (dot t)    = 0
-  pattern-bindings (var x)    = 1
-  pattern-bindings (lit l)    = 0
-  pattern-bindings (proj f)   = 1
-  pattern-bindings (absurd x) = 0
-
-  patterns-bindings [] = 0
-  patterns-bindings (arg i pat ∷ pats) = pattern-bindings pat + patterns-bindings pats
+  -- Descend past a variable.
+  var-descend : ℕ → ℕ → ℕ
+  var-descend ϕ x = if ϕ Nat.≤ᵇ x then suc x else x
+
+  -- Descend a variable underneath pattern variables.
+  pattern-descend : ℕ → Pattern → (Pattern × ℕ)
+  patterns-descend : ℕ → Args Pattern → (Args Pattern × ℕ)
+
+  pattern-descend ϕ (con c ps) =
+    let (ps' , ϕ') = patterns-descend ϕ ps
+    in (con c ps' , ϕ')
+  pattern-descend ϕ (dot t)    = (dot t) , ϕ
+  pattern-descend ϕ (var x)    = var (var-descend ϕ x) , suc ϕ
+  pattern-descend ϕ (lit l)    = (lit l) , ϕ
+  pattern-descend ϕ (proj f)   = (proj f) , ϕ
+  pattern-descend ϕ (absurd x) = absurd (var-descend ϕ x) , suc ϕ
+
+  patterns-descend ϕ ((arg i p) ∷ ps) =
+    let (p' , ϕ') = pattern-descend ϕ p
+        (ps' , ϕ'') = patterns-descend ϕ' ps
+    in (arg i p ∷ ps' , ϕ'')
+  patterns-descend ϕ []       =
+    [] , ϕ
 
   -- Helper for constructing applications of 'cong'
   `cong : Term → Term → Term
@@ -85,6 +95,7 @@ private
   endpoints : Term → TC (Term × Term)
   endpoints goal@(def x (lvl ∷ tp ∷ (arg _ e0) ∷ (arg _ e1) ∷ [])) =
     if x Name.≡ᵇ (quote _≡_) then return (e0 , e1) else not-equality-error goal 
+  endpoints (meta m args) = blockOnMeta m
   endpoints goal = not-equality-error goal 
 
 ----------------------------------------------------------------------
@@ -110,7 +121,7 @@ private
   anti-unify ϕ (var x args) (var y args') with x Nat.≡ᵇ y | anti-unify-args ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ uargs
-  ... | true  | just uargs = var x uargs
+  ... | true  | just uargs = var (var-descend ϕ x) uargs
   anti-unify ϕ (con c args) (con c' args') with c Name.≡ᵇ c' | anti-unify-args ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ []
@@ -178,7 +189,9 @@ private
     nothing
   
   anti-unify-clause ϕ (clause Γ pats t) (clause Δ pats' t') =
-    Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (clause Γ pats (anti-unify (ϕ + patterns-bindings pats) t t'))
+    Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats')
+      let (upats , ϕ') = patterns-descend ϕ pats in
+      (clause Γ upats (anti-unify ϕ' t t'))
   anti-unify-clause ϕ (absurd-clause Γ pats) (absurd-clause Δ pats') =
     Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (absurd-clause Γ pats)
   anti-unify-clause ϕ _ _ =
@@ -203,7 +216,22 @@ macro
     -- programmer expects them to be in, so normalising buys us
     -- nothing.
     withNormalisation false $ do
-      goal ← inferType hole
+      goal ← reduce hole >>= inferType 
       (e0 , e1) ← endpoints goal
       let f = anti-unify 0 e0 e1
       unify (`cong f eq) hole
+
+
+open Eq.≡-Reasoning
+open import Data.Nat.Properties
+
+example : ∀ (m n : ℕ) → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
+example m n eq = begin
+    suc (suc (m + 0)) + m
+  ≡⟨ rw (+-identityʳ m) ⟩
+    suc (suc m) + m
+  ≡⟨ rw eq ⟩
+    suc (suc n) + n
+  ≡˘⟨ rw (+-identityʳ n) ⟩
+    suc (suc n) + (n + 0)
+  ∎

From e20fc5924f799d0ab677ad7f0495367bd1157afe Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Wed, 15 Dec 2021 21:26:04 -0800
Subject: [PATCH 06/11] Remove accidental inclusion of testing code

---
 src/Tactic/Rewrite.agda | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
index 3d4f7af0aa..b37f0d5176 100644
--- a/src/Tactic/Rewrite.agda
+++ b/src/Tactic/Rewrite.agda
@@ -220,18 +220,3 @@ macro
       (e0 , e1) ← endpoints goal
       let f = anti-unify 0 e0 e1
       unify (`cong f eq) hole
-
-
-open Eq.≡-Reasoning
-open import Data.Nat.Properties
-
-example : ∀ (m n : ℕ) → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
-example m n eq = begin
-    suc (suc (m + 0)) + m
-  ≡⟨ rw (+-identityʳ m) ⟩
-    suc (suc m) + m
-  ≡⟨ rw eq ⟩
-    suc (suc n) + n
-  ≡˘⟨ rw (+-identityʳ n) ⟩
-    suc (suc n) + (n + 0)
-  ∎

From 0f2fd19cbf500d3de44cc8753b11a2f5a607bd31 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 16 Dec 2021 09:30:08 -0800
Subject: [PATCH 07/11] =?UTF-8?q?Add=20`=5F=E2=89=A1=E1=B5=87=5F`=20to=20`?=
 =?UTF-8?q?Reflection.Literal`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 src/Reflection/Literal.agda | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Reflection/Literal.agda b/src/Reflection/Literal.agda
index 6d7cc492e2..4bd0915e47 100644
--- a/src/Reflection/Literal.agda
+++ b/src/Reflection/Literal.agda
@@ -8,6 +8,7 @@
 
 module Reflection.Literal where
 
+open import Data.Bool.Base as Bool using (Bool; true; false)
 import Data.Char as Char
 import Data.Float as Float
 import Data.Nat as ℕ
@@ -102,3 +103,6 @@ meta x ≟ char x₁ = no (λ ())
 meta x ≟ string x₁ = no (λ ())
 meta x ≟ name x₁ = no (λ ())
 meta x ≟ meta x₁ = Dec.map′ (cong meta) meta-injective (x Meta.≟ x₁)
+
+_≡ᵇ_ : Literal → Literal → Bool
+l ≡ᵇ l′ = Dec.isYes (l ≟ l′)

From de3d20a1b3d9bf93fe41cccd52d947013e9addcb Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 16 Dec 2021 09:30:51 -0800
Subject: [PATCH 08/11] Style changes to `Tactic.Rewrite`

---
 src/Tactic/Rewrite.agda | 144 +++++++++++++++++-----------------------
 1 file changed, 62 insertions(+), 82 deletions(-)

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
index b37f0d5176..d322bcd9d7 100644
--- a/src/Tactic/Rewrite.agda
+++ b/src/Tactic/Rewrite.agda
@@ -48,6 +48,7 @@ open import Reflection.AlphaEquality        as Alpha
 open import Reflection.Argument             as Arg
 open import Reflection.Argument.Information as ArgInfo
 open import Reflection.Argument.Visibility  as Visibility
+open import Reflection.Literal              as Literal
 open import Reflection.Meta                 as Meta
 open import Reflection.Name                 as Name
 open import Reflection.Term                 as Term
@@ -60,43 +61,41 @@ open import Reflection.TypeChecking.Monad.Syntax
 
 private
   -- Descend past a variable.
-  var-descend : ℕ → ℕ → ℕ
-  var-descend ϕ x = if ϕ Nat.≤ᵇ x then suc x else x
+  varDescend : ℕ → ℕ → ℕ
+  varDescend ϕ x = if ϕ Nat.≤ᵇ x then suc x else x
 
   -- Descend a variable underneath pattern variables.
-  pattern-descend : ℕ → Pattern → (Pattern × ℕ)
-  patterns-descend : ℕ → Args Pattern → (Args Pattern × ℕ)
-
-  pattern-descend ϕ (con c ps) =
-    let (ps' , ϕ') = patterns-descend ϕ ps
-    in (con c ps' , ϕ')
-  pattern-descend ϕ (dot t)    = (dot t) , ϕ
-  pattern-descend ϕ (var x)    = var (var-descend ϕ x) , suc ϕ
-  pattern-descend ϕ (lit l)    = (lit l) , ϕ
-  pattern-descend ϕ (proj f)   = (proj f) , ϕ
-  pattern-descend ϕ (absurd x) = absurd (var-descend ϕ x) , suc ϕ
-
-  patterns-descend ϕ ((arg i p) ∷ ps) =
-    let (p' , ϕ') = pattern-descend ϕ p
-        (ps' , ϕ'') = patterns-descend ϕ' ps
+  patternDescend : ℕ → Pattern → Pattern × ℕ
+  patternsDescend : ℕ → Args Pattern → Args Pattern × ℕ
+
+  patternDescend ϕ (con c ps) = map₁ (con c) (patternsDescend ϕ ps)
+  patternDescend ϕ (dot t)    = dot t , ϕ
+  patternDescend ϕ (var x)    = var (varDescend ϕ x) , suc ϕ
+  patternDescend ϕ (lit l)    = lit l , ϕ
+  patternDescend ϕ (proj f)   = proj f , ϕ
+  patternDescend ϕ (absurd x) = absurd (varDescend ϕ x) , suc ϕ
+
+  patternsDescend ϕ ((arg i p) ∷ ps) =
+    let (p' , ϕ') = patternDescend ϕ p
+        (ps' , ϕ'') = patternsDescend ϕ' ps
     in (arg i p ∷ ps' , ϕ'')
-  patterns-descend ϕ []       =
+  patternsDescend ϕ []       =
     [] , ϕ
 
   -- Helper for constructing applications of 'cong'
   `cong : Term → Term → Term
-  `cong f eq = def (quote cong) (4 ⋯⟅∷⟆ vArg (lam visible (abs "ϕ" f)) ∷ 2 ⋯⟅∷⟆ vArg eq ∷ [])
+  `cong f eq = def (quote cong) (4 ⋯⟅∷⟆ vArg (vLam "ϕ" f) ∷ 2 ⋯⟅∷⟆ vArg eq ∷ [])
 
   -- Construct an error when the goal is not 'x ≡ y' for some 'x' and 'y'.
-  not-equality-error : ∀ {A : Set} Term → TC A
-  not-equality-error goal = typeError (strErr "Cannot rewrite a goal that is not equality: " ∷ termErr goal ∷ [])
+  notEqualityError : ∀ {A : Set} Term → TC A
+  notEqualityError goal = typeError (strErr "Cannot rewrite a goal that is not equality: " ∷ termErr goal ∷ [])
 
   -- Extract out both endpoints of an equality type.
   endpoints : Term → TC (Term × Term)
   endpoints goal@(def x (lvl ∷ tp ∷ (arg _ e0) ∷ (arg _ e1) ∷ [])) =
-    if x Name.≡ᵇ (quote _≡_) then return (e0 , e1) else not-equality-error goal 
+    if x Name.≡ᵇ (quote _≡_) then return (e0 , e1) else notEqualityError goal 
   endpoints (meta m args) = blockOnMeta m
-  endpoints goal = not-equality-error goal 
+  endpoints goal = notEqualityError goal 
 
 ----------------------------------------------------------------------
 -- Anti-Unification
@@ -113,93 +112,74 @@ private
 ----------------------------------------------------------------------
 
 private
-  anti-unify : ℕ → Term → Term → Term
-  anti-unify-args : ℕ → Args Term → Args Term → Maybe (Args Term)
-  anti-unify-clauses : ℕ → Clauses → Clauses → Maybe Clauses
-  anti-unify-clause : ℕ → Clause → Clause → Maybe Clause
+  antiUnify : ℕ → Term → Term → Term
+  antiUnifyArgs : ℕ → Args Term → Args Term → Maybe (Args Term)
+  antiUnifyClauses : ℕ → Clauses → Clauses → Maybe Clauses
+  antiUnifyClause : ℕ → Clause → Clause → Maybe Clause
   
-  anti-unify ϕ (var x args) (var y args') with x Nat.≡ᵇ y | anti-unify-args ϕ args args'
+  antiUnify ϕ (var x args) (var y args') with x Nat.≡ᵇ y | antiUnifyArgs ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ uargs
-  ... | true  | just uargs = var (var-descend ϕ x) uargs
-  anti-unify ϕ (con c args) (con c' args') with c Name.≡ᵇ c' | anti-unify-args ϕ args args'
+  ... | true  | just uargs = var (varDescend ϕ x) uargs
+  antiUnify ϕ (con c args) (con c' args') with c Name.≡ᵇ c' | antiUnifyArgs ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ []
   ... | true  | just uargs = con c uargs
-  anti-unify ϕ (def f args) (def f' args') with f Name.≡ᵇ f' | anti-unify-args ϕ args args'
+  antiUnify ϕ (def f args) (def f' args') with f Name.≡ᵇ f' | antiUnifyArgs ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | just uargs = var ϕ []
   ... | true  | just uargs = def f uargs
-  anti-unify ϕ (lam v (abs s t)) (lam _ (abs _ t')) =
-    lam v (abs s (anti-unify (suc ϕ) t t'))
-  anti-unify ϕ (pat-lam cs args) (pat-lam cs' args') with anti-unify-clauses ϕ cs cs' | anti-unify-args ϕ args args'
+  antiUnify ϕ (lam v (abs s t)) (lam _ (abs _ t')) =
+    lam v (abs s (antiUnify (suc ϕ) t t'))
+  antiUnify ϕ (pat-lam cs args) (pat-lam cs' args') with antiUnifyClauses ϕ cs cs' | antiUnifyArgs ϕ args args'
   ... | nothing  | _       = var ϕ []
   ... | _        | nothing = var ϕ []
   ... | just ucs | just uargs = pat-lam ucs uargs
-  anti-unify ϕ (Π[ s ∶ arg i a ] b) (Π[ _ ∶ arg _ a' ] b') =
-    Π[ s ∶ arg i (anti-unify ϕ a a') ] anti-unify (suc ϕ) b b'
-  anti-unify ϕ (sort (set t)) (sort (set t')) =
-    sort (set (anti-unify ϕ t t'))
-  anti-unify ϕ (sort (lit n)) (sort (lit n')) with n Nat.≡ᵇ n'
+  antiUnify ϕ (Π[ s ∶ arg i a ] b) (Π[ _ ∶ arg _ a' ] b') =
+    Π[ s ∶ arg i (antiUnify ϕ a a') ] antiUnify (suc ϕ) b b'
+  antiUnify ϕ (sort (set t)) (sort (set t')) =
+    sort (set (antiUnify ϕ t t'))
+  antiUnify ϕ (sort (lit n)) (sort (lit n')) with n Nat.≡ᵇ n'
   ... | true  = sort (lit n)
   ... | false = var ϕ []
-  anti-unify ϕ (sort (prop t)) (sort (prop t')) =
-    sort (prop (anti-unify ϕ t t'))
-  anti-unify ϕ (sort (propLit n)) (sort (propLit n')) with n Nat.≡ᵇ n'
+  antiUnify ϕ (sort (propLit n)) (sort (propLit n')) with n Nat.≡ᵇ n'
   ... | true  = sort (propLit n)
   ... | false = var ϕ []
-  anti-unify ϕ (sort (inf n)) (sort (inf n')) with n Nat.≡ᵇ n'
+  antiUnify ϕ (sort (inf n)) (sort (inf n')) with n Nat.≡ᵇ n'
   ... | true  = sort (inf n)
   ... | false = var ϕ []
-  anti-unify ϕ (sort unknown) (sort unknown) =
+  antiUnify ϕ (sort unknown) (sort unknown) =
     sort unknown
-  anti-unify ϕ (lit (nat n)) (lit (nat n')) with n Nat.≡ᵇ n'
-  ... | true  = lit (nat n)
+  antiUnify ϕ (lit l) (lit l') with l Literal.≡ᵇ l'
+  ... | true  = lit l
   ... | false = var ϕ []
-  anti-unify ϕ (lit (word64 n)) (lit (word64 n')) with Word.toℕ n Nat.≡ᵇ Word.toℕ n'
-  ... | true  = lit (word64 n)
-  ... | false = var ϕ []
-  anti-unify ϕ (lit (float x)) (lit (float x')) with x Float.≡ᵇ x'
-  ... | true  = lit (float x)
-  ... | false = var ϕ []
-  anti-unify ϕ (lit (char c)) (lit (char c')) with Char.toℕ c Nat.≡ᵇ Char.toℕ c'
-  ... | true  = lit (char c)
-  ... | false = var ϕ []
-  anti-unify ϕ (lit (string s)) (lit (string s')) with s String.≡ᵇ s'
-  ... | true = lit (string s)
-  ... | false = var ϕ []
-  anti-unify ϕ (lit (name x)) (lit (name x')) with x Name.≡ᵇ x'
-  ... | true  = lit (name x)
-  ... | false = var ϕ []
-  anti-unify ϕ (lit (meta x)) (lit (meta x')) with x Meta.≡ᵇ x'
-  ... | true = lit (meta x)
-  ... | false = var ϕ []
-  anti-unify ϕ (meta x args) (meta x' args') with x Meta.≡ᵇ x' | anti-unify-args ϕ args args'
+  antiUnify ϕ (meta x args) (meta x' args') with x Meta.≡ᵇ x' | antiUnifyArgs ϕ args args'
   ... | _     | nothing    = var ϕ []
   ... | false | _          = var ϕ []
   ... | true  | just uargs = meta x uargs
-  anti-unify ϕ unknown unknown = unknown
-  anti-unify ϕ _ _ = var ϕ []
+  antiUnify ϕ unknown unknown = unknown
+  antiUnify ϕ _ _ = var ϕ []
   
-  anti-unify-args ϕ (arg i t ∷ args) (arg _ t' ∷ args') =
-    Maybe.map (arg i (anti-unify ϕ t t') ∷_) (anti-unify-args ϕ args args')
-  anti-unify-args ϕ [] [] =
+  antiUnifyArgs ϕ (arg i t ∷ args) (arg _ t' ∷ args') =
+    Maybe.map (arg i (antiUnify ϕ t t') ∷_) (antiUnifyArgs ϕ args args')
+  antiUnifyArgs ϕ [] [] =
     just []
-  anti-unify-args ϕ _ _ =
+  antiUnifyArgs ϕ _ _ =
     nothing
   
-  anti-unify-clause ϕ (clause Γ pats t) (clause Δ pats' t') =
-    Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats')
-      let (upats , ϕ') = patterns-descend ϕ pats in
-      (clause Γ upats (anti-unify ϕ' t t'))
-  anti-unify-clause ϕ (absurd-clause Γ pats) (absurd-clause Δ pats') =
-    Maybe.when (Γ =α=-Telescope Δ ∧ pats =α=-ArgsPattern pats') (absurd-clause Γ pats)
-  anti-unify-clause ϕ _ _ =
+  antiUnifyClause ϕ (clause Γ pats t) (clause Δ pats' t') =
+    Maybe.when ((Γ =α= Δ) ∧ (pats =α= pats'))
+      let (upats , ϕ') = patternsDescend ϕ pats
+      in clause Γ upats (antiUnify ϕ' t t')
+  antiUnifyClause ϕ (absurd-clause Γ pats) (absurd-clause Δ pats') =
+    Maybe.when ((Γ =α= Δ) ∧ (pats =α= pats')) $
+      absurd-clause Γ pats
+  antiUnifyClause ϕ _ _ =
     nothing
   
-  anti-unify-clauses ϕ (c ∷ cs) (c' ∷ cs') =
-    Maybe.ap (Maybe.map _∷_ (anti-unify-clause ϕ c c')) (anti-unify-clauses ϕ cs cs')
-  anti-unify-clauses ϕ _ _ =
+  antiUnifyClauses ϕ (c ∷ cs) (c' ∷ cs') =
+    Maybe.ap (Maybe.map _∷_ (antiUnifyClause ϕ c c')) (antiUnifyClauses ϕ cs cs')
+  antiUnifyClauses ϕ _ _ =
     just []
 
 
@@ -218,5 +198,5 @@ macro
     withNormalisation false $ do
       goal ← reduce hole >>= inferType 
       (e0 , e1) ← endpoints goal
-      let f = anti-unify 0 e0 e1
+      let f = antiUnify 0 e0 e1
       unify (`cong f eq) hole

From 82ab790c794cb70423e3ae1c409c561b88948099 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 16 Dec 2021 11:31:31 -0800
Subject: [PATCH 09/11] Rename `Tactic.Rewrite.rw` to `Tactic.Rewrite.cong!`

---
 src/Tactic/Rewrite.agda | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
index d322bcd9d7..cb29100db4 100644
--- a/src/Tactic/Rewrite.agda
+++ b/src/Tactic/Rewrite.agda
@@ -11,11 +11,11 @@
 -- example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
 -- example m n eq = begin
 --     suc (suc (m + 0)) + m
---   ≡⟨ rw (+-identityʳ m) ⟩
+--   ≡⟨ cong! (+-identityʳ m) ⟩
 --     suc (suc m) + m
---   ≡⟨ rw eq ⟩
+--   ≡⟨ cong! eq ⟩
 --     suc (suc n) + n
---   ≡˘⟨ rw (+-identityʳ n) ⟩
+--   ≡˘⟨ cong! (+-identityʳ n) ⟩
 --     suc (suc n) + (n + 0)
 --   ∎
 ------------------------------------------------------------------------
@@ -190,6 +190,8 @@ private
 macro
   rw : Term → Term → TC ⊤
   rw eq hole =
+  cong! : Term → Term → TC ⊤
+  cong! eq hole =
     -- NOTE: We avoid doing normalisation here as this tactic
     -- is mainly meant for equational reasoning. In that context,
     -- the endpoints are already specified in the form that the

From 9f8b601e54ef067904dd4544aed2dd2e365562a3 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Thu, 16 Dec 2021 11:35:46 -0800
Subject: [PATCH 10/11] Fix implicits not being instantiated by `cong!`

---
 src/Tactic/Rewrite.agda | 66 ++++++++++++++++++++++++++---------------
 1 file changed, 42 insertions(+), 24 deletions(-)

diff --git a/src/Tactic/Rewrite.agda b/src/Tactic/Rewrite.agda
index cb29100db4..a2e64e74db 100644
--- a/src/Tactic/Rewrite.agda
+++ b/src/Tactic/Rewrite.agda
@@ -82,20 +82,39 @@ private
   patternsDescend ϕ []       =
     [] , ϕ
 
-  -- Helper for constructing applications of 'cong'
-  `cong : Term → Term → Term
-  `cong f eq = def (quote cong) (4 ⋯⟅∷⟆ vArg (vLam "ϕ" f) ∷ 2 ⋯⟅∷⟆ vArg eq ∷ [])
-
   -- Construct an error when the goal is not 'x ≡ y' for some 'x' and 'y'.
   notEqualityError : ∀ {A : Set} Term → TC A
   notEqualityError goal = typeError (strErr "Cannot rewrite a goal that is not equality: " ∷ termErr goal ∷ [])
 
-  -- Extract out both endpoints of an equality type.
-  endpoints : Term → TC (Term × Term)
-  endpoints goal@(def x (lvl ∷ tp ∷ (arg _ e0) ∷ (arg _ e1) ∷ [])) =
-    if x Name.≡ᵇ (quote _≡_) then return (e0 , e1) else notEqualityError goal 
-  endpoints (meta m args) = blockOnMeta m
-  endpoints goal = notEqualityError goal 
+  record EqualityGoal : Set where
+    constructor equals
+    field
+      level : Term
+      type  : Term
+      lhs   : Term
+      rhs   : Term
+
+  destructEqualityGoal : Term → TC EqualityGoal
+  destructEqualityGoal goal@(def (quote _≡_) (lvl ∷ tp ∷ lhs ∷ rhs ∷ [])) =
+    return $ equals (unArg lvl) (unArg tp) (unArg lhs) (unArg rhs)
+  destructEqualityGoal (meta m args) =
+    blockOnMeta m
+  destructEqualityGoal goal =
+    notEqualityError goal
+
+  -- Helper for constructing applications of 'cong'
+  `cong : ∀ {a} {A : Set a} {x y : A} → EqualityGoal → Term → x ≡ y → TC Term
+  `cong {a = a} {A = A} {x = x} {y = y} eqGoal f x≡y = do
+    -- NOTE: We apply all implicit arguments here to ensure that using
+    -- equality proofs with implicits don't lead to unsolved metavariable
+    -- errors.
+    let open EqualityGoal eqGoal
+    eq ← quoteTC x≡y
+    `a ← quoteTC a
+    `A ← quoteTC A
+    `x ← quoteTC x
+    `y ← quoteTC y
+    return $ def (quote cong) $ `a ⟅∷⟆ `A ⟅∷⟆ level ⟅∷⟆ type ⟅∷⟆ vLam "ϕ" f ⟨∷⟩ `x ⟅∷⟆ `y ⟅∷⟆ eq ⟨∷⟩ []
 
 ----------------------------------------------------------------------
 -- Anti-Unification
@@ -159,14 +178,14 @@ private
   ... | true  | just uargs = meta x uargs
   antiUnify ϕ unknown unknown = unknown
   antiUnify ϕ _ _ = var ϕ []
-  
+
   antiUnifyArgs ϕ (arg i t ∷ args) (arg _ t' ∷ args') =
     Maybe.map (arg i (antiUnify ϕ t t') ∷_) (antiUnifyArgs ϕ args args')
   antiUnifyArgs ϕ [] [] =
     just []
   antiUnifyArgs ϕ _ _ =
     nothing
-  
+
   antiUnifyClause ϕ (clause Γ pats t) (clause Δ pats' t') =
     Maybe.when ((Γ =α= Δ) ∧ (pats =α= pats'))
       let (upats , ϕ') = patternsDescend ϕ pats
@@ -176,7 +195,7 @@ private
       absurd-clause Γ pats
   antiUnifyClause ϕ _ _ =
     nothing
-  
+
   antiUnifyClauses ϕ (c ∷ cs) (c' ∷ cs') =
     Maybe.ap (Maybe.map _∷_ (antiUnifyClause ϕ c c')) (antiUnifyClauses ϕ cs cs')
   antiUnifyClauses ϕ _ _ =
@@ -188,17 +207,16 @@ private
 ----------------------------------------------------------------------
 
 macro
-  rw : Term → Term → TC ⊤
-  rw eq hole =
-  cong! : Term → Term → TC ⊤
-  cong! eq hole =
+  cong! : ∀ {a} {A : Set a} {x y : A} → x ≡ y → Term → TC ⊤
+  cong! x≡y hole =
     -- NOTE: We avoid doing normalisation here as this tactic
     -- is mainly meant for equational reasoning. In that context,
-    -- the endpoints are already specified in the form that the
-    -- programmer expects them to be in, so normalising buys us
-    -- nothing.
+    -- 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 ← reduce hole >>= inferType 
-      (e0 , e1) ← endpoints goal
-      let f = antiUnify 0 e0 e1
-      unify (`cong f eq) hole
+      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

From a0be964831ba5008a390a4fbde91b173c4d40143 Mon Sep 17 00:00:00 2001
From: Reed Mullanix <reedmullanix@gmail.com>
Date: Tue, 21 Dec 2021 13:10:50 +0000
Subject: [PATCH 11/11] Add `README.Tactic.Rewrite`

---
 CHANGELOG.md               |   5 ++
 README/Tactic/Rewrite.agda | 139 +++++++++++++++++++++++++++++++++++++
 2 files changed, 144 insertions(+)
 create mode 100644 README/Tactic/Rewrite.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d61111a7f2..240562b7db 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -548,6 +548,11 @@ New modules
   Reflection.AlphaEquality
   ```
 
+* `cong!` tactic for deriving arguments to `cong`
+  ```
+  Tactic.Rewrite
+  ```
+
 * Various system types and primitives:
   ```
   System.Clock.Primitive
diff --git a/README/Tactic/Rewrite.agda b/README/Tactic/Rewrite.agda
new file mode 100644
index 0000000000..d96c9231a5
--- /dev/null
+++ b/README/Tactic/Rewrite.agda
@@ -0,0 +1,139 @@
+{-# OPTIONS --without-K --safe #-}
+module README.Tactic.Rewrite where
+
+open import Data.Nat
+open import Data.Nat.Properties
+
+open import Relation.Binary.PropositionalEquality as Eq
+import Relation.Binary.Reasoning.Preorder as PR
+
+open import Tactic.Rewrite using (cong!)
+
+----------------------------------------------------------------------
+-- Usage
+----------------------------------------------------------------------
+
+-- When performing large equational reasoning proofs, it's quite 
+-- common to have to construct sophisticated lambdas to pass
+-- into 'cong'. This can be extremely tedious, and can bog down
+-- large proofs in piles of boilerplate. The 'cong!' tactic
+-- simplifies this process by synthesizing the appropriate call
+-- to 'cong' by inspecting both sides of the goal.
+--
+-- This is best demonstrated with a small example. Consider
+-- the following proof:
+
+verbose-example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
+verbose-example m n eq =
+  let open Eq.≡-Reasoning in
+  begin
+    suc (suc (m + 0)) + m
+  ≡⟨ cong (λ ϕ → suc (suc (ϕ + m))) (+-identityʳ m) ⟩
+    suc (suc m) + m
+  ≡⟨ cong (λ ϕ → suc (suc (ϕ + ϕ))) eq ⟩
+    suc (suc n) + n
+  ≡˘⟨ cong (λ ϕ → suc (suc (n + ϕ))) (+-identityʳ n) ⟩
+    suc (suc n) + (n + 0)
+  ∎
+
+-- The calls to 'cong' add a lot of boilerplate, and also
+-- clutter up the proof, making it more difficult to read.
+-- We can simplify this by using 'cong!' to deduce those
+-- lambdas for us.
+
+succinct-example : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
+succinct-example m n eq =
+  let open Eq.≡-Reasoning in
+  begin
+    suc (suc (m + 0)) + m
+  ≡⟨ cong! (+-identityʳ m) ⟩
+    suc (suc m) + m
+  ≡⟨ cong! eq ⟩
+    suc (suc n) + n
+  ≡˘⟨ cong! (+-identityʳ n) ⟩
+    suc (suc n) + (n + 0)
+  ∎
+
+----------------------------------------------------------------------
+-- Limitations
+----------------------------------------------------------------------
+
+-- The 'cong!' tactic can handle simple cases, but will
+-- struggle when presented with equality proofs like
+-- 'm + n ≡ n + m' or 'm + (n + o) ≡ (m + n) + o'.
+--
+-- The reason behind this is that this tactic operates by simple
+-- anti-unification; it examines both sides of the equality goal
+-- 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.
+
+----------------------------------------------------------------------
+-- Unit Tests
+----------------------------------------------------------------------
+
+module LiteralTests
+  (assumption : 48 ≡ 42)
+  (f : ℕ → ℕ → ℕ → ℕ)
+  where
+
+  test₁ : 40 + 2 ≡ 42
+  test₁ = cong! refl
+  
+  test₂ : 48 ≡ 42 → 42 ≡ 48
+  test₂ eq = cong! (sym eq)
+  
+  test₃ : (f : ℕ → ℕ) → f 48 ≡ f 42 
+  test₃ f = cong! assumption
+  
+  test₄ : (f : ℕ → ℕ → ℕ) → f 48 48 ≡ f 42 42
+  test₄ f = cong! assumption
+
+  test₅ : f 48 45 48 ≡ f 42 45 42
+  test₅ = cong! assumption
+
+module LambdaTests
+  (assumption : 48 ≡ 42)
+  where
+
+  test₁ : (λ x → x + 48) ≡ (λ x → x + 42)
+  test₁ = cong! assumption
+
+  test₂ : (λ x y z → x + (y + 48 + z)) ≡ (λ x y z → x + (y + 42 + z))
+  test₂ = cong! assumption
+
+module HigherOrderTests
+  (f g : ℕ → ℕ)
+  where
+
+  test₁ : f ≡ g → ∀ n → f n ≡ g n
+  test₁ eq n = cong! eq
+
+  test₂ : f ≡ g → ∀ n → f (f (f n)) ≡ g (g (g n))
+  test₂ eq n = cong! eq
+ 
+module EquationalReasoningTests where
+
+  test₁ : ∀ m n → m ≡ n → suc (suc (m + 0)) + m ≡ suc (suc n) + (n + 0)
+  test₁ m n eq =
+    let open Eq.≡-Reasoning in
+    begin
+      suc (suc (m + 0)) + m
+    ≡⟨ cong! (+-identityʳ m) ⟩
+      suc (suc m) + m
+    ≡⟨ cong! eq ⟩
+      suc (suc n) + n
+    ≡˘⟨ cong! (+-identityʳ n) ⟩
+      suc (suc n) + (n + 0)
+    ∎
+
+  test₂ : ∀ m n → m ≡ n → suc (m + m) ≤ suc (suc (n + n))
+  test₂ m n eq =
+    let open PR ≤-preorder in
+    begin
+      suc (m + m)
+    ≡⟨ cong! eq ⟩
+      suc (n + n)
+    ∼⟨ ≤-step ≤-refl ⟩
+      suc (suc (n + n))
+    ∎