Another tweak to cong!

CHANGELOG.md

@@ -426,5 +426,7 @@ Additions to existing modules
   WeaklyDecidable : Pred A ℓ → Set _
   ```
 
-* `Tactic.Cong` now provides a marker function, `⌞_⌟`, for user-guided
-  anti-unification. See README.Tactic.Cong for details.
+* Enhancements to `Tactic.Cong` - see `README.Tactic.Cong` for details.
+  - Provide a marker function, `⌞_⌟`, for user-guided anti-unification.
+  - Improved support for equalities between terms with instance arguments,
+    such as terms that contain `_/_` or `_%_`.

doc/README/Tactic/Cong.agda

@@ -3,6 +3,7 @@
 module README.Tactic.Cong where
 
 open import Data.Nat
+open import Data.Nat.DivMod
 open import Data.Nat.Properties
 
 open import Relation.Binary.PropositionalEquality
@@ -161,3 +162,34 @@ module EquationalReasoningTests where
     ≤⟨ n≤1+n _ ⟩
       suc (suc (n + n))
     ∎
+
+module MetaTests where
+  test₁ : ∀ m n o → .⦃ _ : NonZero o ⦄ → (m + n) / o ≡ (n + m) / o
+  test₁ m n o =
+    let open ≤-Reasoning in
+    begin-equality
+      ⌞ m + n ⌟ / o
+     ≡⟨ cong! (+-comm m n) ⟩
+      (n + m) / o
+    ∎
+
+  test₂ : ∀ m n o p q r → .⦃ _ : NonZero o ⦄ → .⦃ _ : NonZero p ⦄ →
+          .⦃ _ : NonZero q ⦄ → p ≡ q ^ r → (m + n) % o % p ≡ (n + m) % o % p
+  test₂ m n o p q r eq =
+    let
+      open ≤-Reasoning
+      instance q^r≢0 = m^n≢0 q r
+    in
+    begin-equality
+      (m + n) % o % p
+     ≡⟨ %-congʳ eq ⟩
+      ⌞ m + n ⌟ % o % q ^ r
+     ≡⟨ cong! (+-comm m n) ⟩
+      ⌞ n + m ⌟ % o % q ^ r
+     ≡⟨ cong! (+-comm m n) ⟨
+      ⌞ m + n ⌟ % o % q ^ r
+     ≡⟨ cong! (+-comm m n) ⟩
+      (n + m) % o % q ^ r
+     ≡⟨ %-congʳ eq ⟨
+      (n + m) % o % p
+    ∎

src/Tactic/Cong.agda

@@ -31,14 +31,17 @@ 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.Unit.Base            using (⊤; tt)
 open import Data.Word.Base   as Word  using (toℕ)
 open import Data.Product.Base         using (_×_; map₁; _,_)
+open import Effect.Applicative        using (RawApplicative; mkRawApplicative)
+open import Function                  using (flip; case_of_)
 
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
+open import Relation.Nullary.Decidable.Core            using (yes; no)
 
 -- 'Data.String.Properties' defines this via 'Dec', so let's use the
 -- builtin for maximum speed.
@@ -54,6 +57,7 @@ open import Reflection.AST.Literal              as Literal
 open import Reflection.AST.Meta                 as Meta
 open import Reflection.AST.Name                 as Name
 open import Reflection.AST.Term                 as Term
+import Reflection.AST.Traversal                 as Traversal
 
 open import Reflection.TCM.Syntax
 
@@ -102,6 +106,16 @@ private
   notEqualityError : ∀ {A : Set} Term → TC A
   notEqualityError goal = typeError (strErr "Cannot rewrite a goal that is not equality: " ∷ termErr goal ∷ [])
 
+  unificationError : ∀ {A : Set} → TC Term → TC Term → TC A
+  unificationError term symTerm = do
+    term' ← term
+    symTerm' ← symTerm
+    -- Don't show the same term twice.
+    let symErr = case term' Term.≟ symTerm' of λ where
+      (yes _) → []
+      (no _) → strErr "\n" ∷ termErr symTerm' ∷ []
+    typeError (strErr "cong! failed, tried:\n" ∷ termErr term' ∷ symErr)
+
   record EqualityGoal : Set where
     constructor equals
     field
@@ -132,6 +146,21 @@ private
     `y ← quoteTC y
     pure $ def (quote cong) $ `a ⟅∷⟆ `A ⟅∷⟆ level ⟅∷⟆ type ⟅∷⟆ vLam "ϕ" f ⟨∷⟩ `x ⟅∷⟆ `y ⟅∷⟆ eq ⟨∷⟩ []
 
+  module _ where
+    private
+      applicative : ∀ {ℓ} → RawApplicative {ℓ} λ _ → List Meta
+      applicative = mkRawApplicative (λ _ → List Meta) (λ _ → []) _++_
+
+      open Traversal applicative
+
+      actions : Actions
+      actions = record defaultActions { onMeta = λ _ x → x ∷ [] }
+
+    blockOnMetas : Term → TC ⊤
+    blockOnMetas t with traverseTerm actions (0 , []) t
+    ... | []         = pure tt
+    ... | xs@(_ ∷ _) = blockTC (blockerAll (List.map blockerMeta xs))
+
 ------------------------------------------------------------------------
 -- Anti-Unification
 --
@@ -236,12 +265,17 @@ macro
     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 makeTerm = λ lhs rhs → `cong eqGoal (antiUnify 0 lhs rhs) x≡y
       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)
+      let term = makeTerm lhs rhs
+      let symTerm = makeTerm rhs lhs
+      let uni = _>>= flip unify hole
+      -- When using ⌞_⌟ with ≡⟨ ... ⟨, (uni term) fails and
+      -- (uni symTerm) succeeds.
+      catchTC (uni term) $
+        catchTC (uni symTerm) $ do
+          -- If we failed because of unresolved metas, restart.
+          blockOnMetas goal
+          -- If we failed for a different reason, show an error.
+          unificationError term symTerm