Another tweak to cong! (#2340)

* Disallow meta variables in goals - they break anti-unification.

* Postpone checking for metas.

* CHANGELOG entry, unit tests, code tweak.

* Move blockOnMetas to a new Reflection.TCM.Utilities module.

Author: uncle-betty

CHANGELOG.md

@@ -458,5 +458,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,35 @@ 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/Reflection/TCM/Utilities.agda

@@ -0,0 +1,33 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Reflection utilities
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Reflection.TCM.Utilities where
+
+open import Data.List using (List; []; _∷_; _++_; map)
+open import Data.Unit using (⊤; tt)
+open import Effect.Applicative using (RawApplicative; mkRawApplicative)
+open import Function using (case_of_)
+open import Reflection.AST.Meta using (Meta)
+open import Reflection.AST.Term using (Term)
+open import Reflection.TCM using (TC; pure; blockTC; blockerAll; blockerMeta)
+
+import Reflection.AST.Traversal as Traversal
+
+blockOnMetas : Term → TC ⊤
+blockOnMetas t =
+  case traverseTerm actions (0 , []) t of λ where
+    []         → pure tt
+    xs@(_ ∷ _) → blockTC (blockerAll (map blockerMeta xs))
+  where
+  applicative : ∀ {ℓ} → RawApplicative {ℓ} (λ _ → List Meta)
+  applicative = mkRawApplicative (λ _ → List Meta) (λ _ → []) _++_
+
+  open Traversal applicative
+
+  actions : Actions
+  actions = record defaultActions { onMeta = λ _ x → x ∷ [] }

src/Tactic/Cong.agda

@@ -37,8 +37,10 @@ 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 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,8 +56,10 @@ 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
+open import Reflection.TCM.Utilities
 
 -- Marker to keep anti-unification from descending into the wrapped
 -- subterm.
@@ -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
@@ -236,12 +250,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