From d6989bc74fd003c67f1ea6e86964c512f240ba30 Mon Sep 17 00:00:00 2001 From: Thomas Lopatic Date: Sun, 31 Mar 2024 19:01:44 +0000 Subject: [PATCH 1/4] Disallow meta variables in goals - they break anti-unification. --- src/Tactic/Cong.agda | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 0259191800..0451f06315 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -31,12 +31,13 @@ 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 Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong) @@ -54,6 +55,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 @@ -113,8 +115,6 @@ private destructEqualityGoal : Term → TC EqualityGoal destructEqualityGoal goal@(def (quote _≡_) (lvl ∷ tp ∷ lhs ∷ rhs ∷ [])) = pure $ equals (unArg lvl) (unArg tp) (unArg lhs) (unArg rhs) - destructEqualityGoal (meta m args) = - blockOnMeta m destructEqualityGoal goal = notEqualityError goal @@ -132,6 +132,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 ∷ [] } + + disallowMetas : Term → TC ⊤ + disallowMetas t with traverseTerm actions (0 , []) t + ... | [] = pure tt + ... | xs@(_ ∷ _) = blockTC (blockerAll (List.map blockerMeta xs)) + ------------------------------------------------------------------------ -- Anti-Unification -- @@ -235,6 +250,7 @@ macro -- so normalising buys us nothing. withNormalisation false $ do goal ← inferType hole + disallowMetas goal eqGoal ← destructEqualityGoal goal let uni = λ lhs rhs → do let cong-lam = antiUnify 0 lhs rhs From bec1fedbc5b5bab7e2057592b02da08a23baded0 Mon Sep 17 00:00:00 2001 From: Thomas Lopatic Date: Mon, 1 Apr 2024 10:10:30 +0000 Subject: [PATCH 2/4] Postpone checking for metas. --- src/Tactic/Cong.agda | 38 ++++++++++++++++++++++++++++---------- 1 file changed, 28 insertions(+), 10 deletions(-) diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 0451f06315..89afaeece0 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -38,8 +38,10 @@ 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. @@ -104,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 @@ -115,6 +127,8 @@ private destructEqualityGoal : Term → TC EqualityGoal destructEqualityGoal goal@(def (quote _≡_) (lvl ∷ tp ∷ lhs ∷ rhs ∷ [])) = pure $ equals (unArg lvl) (unArg tp) (unArg lhs) (unArg rhs) + destructEqualityGoal (meta m args) = + blockOnMeta m destructEqualityGoal goal = notEqualityError goal @@ -142,8 +156,8 @@ private actions : Actions actions = record defaultActions { onMeta = λ _ x → x ∷ [] } - disallowMetas : Term → TC ⊤ - disallowMetas t with traverseTerm actions (0 , []) t + blockOnMetas : Term → TC ⊤ + blockOnMetas t with traverseTerm actions (0 , []) t ... | [] = pure tt ... | xs@(_ ∷ _) = blockTC (blockerAll (List.map blockerMeta xs)) @@ -250,14 +264,18 @@ macro -- so normalising buys us nothing. withNormalisation false $ do goal ← inferType hole - disallowMetas goal 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 + catchTC + -- When using ⌞_⌟ with ≡⟨ ... ⟨, (uni term) fails and + -- (uni symTerm) succeeds. + (catchTC (uni term) (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 From c825187ced500caa0740ac68a5714f3e6892fb78 Mon Sep 17 00:00:00 2001 From: Thomas Lopatic Date: Fri, 5 Apr 2024 11:06:05 +0000 Subject: [PATCH 3/4] CHANGELOG entry, unit tests, code tweak. --- CHANGELOG.md | 6 ++++-- doc/README/Tactic/Cong.agda | 32 ++++++++++++++++++++++++++++++++ src/Tactic/Cong.agda | 8 ++++---- 3 files changed, 40 insertions(+), 6 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 469c926af8..ef6f89c87e 100644 --- a/CHANGELOG.md +++ b/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 `_%_`. diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda index f6adfe9f9f..aa7fe019ff 100644 --- a/doc/README/Tactic/Cong.agda +++ b/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 + ∎ diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index 89afaeece0..dd04d2e0d8 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -271,10 +271,10 @@ macro let term = makeTerm lhs rhs let symTerm = makeTerm rhs lhs let uni = _>>= flip unify hole - catchTC - -- When using ⌞_⌟ with ≡⟨ ... ⟨, (uni term) fails and - -- (uni symTerm) succeeds. - (catchTC (uni term) (uni symTerm)) $ do + -- 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. From 03050df32cccfc2b519228a584d1136d2dea3918 Mon Sep 17 00:00:00 2001 From: Thomas Lopatic Date: Sun, 7 Apr 2024 11:42:10 +0000 Subject: [PATCH 4/4] Move blockOnMetas to a new Reflection.TCM.Utilities module. --- doc/README/Tactic/Cong.agda | 1 + src/Reflection/TCM/Utilities.agda | 33 +++++++++++++++++++++++++++++++ src/Tactic/Cong.agda | 21 +++----------------- 3 files changed, 37 insertions(+), 18 deletions(-) create mode 100644 src/Reflection/TCM/Utilities.agda diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda index aa7fe019ff..01365aee96 100644 --- a/doc/README/Tactic/Cong.agda +++ b/doc/README/Tactic/Cong.agda @@ -164,6 +164,7 @@ module EquationalReasoningTests where ∎ module MetaTests where + test₁ : ∀ m n o → .⦃ _ : NonZero o ⦄ → (m + n) / o ≡ (n + m) / o test₁ m n o = let open ≤-Reasoning in diff --git a/src/Reflection/TCM/Utilities.agda b/src/Reflection/TCM/Utilities.agda new file mode 100644 index 0000000000..d61db6350e --- /dev/null +++ b/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 ∷ [] } diff --git a/src/Tactic/Cong.agda b/src/Tactic/Cong.agda index dd04d2e0d8..80cc7ec6d4 100644 --- a/src/Tactic/Cong.agda +++ b/src/Tactic/Cong.agda @@ -31,13 +31,12 @@ 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 (⊤; tt) +open import Data.Unit.Base using (⊤) 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) @@ -60,6 +59,7 @@ 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. @@ -146,21 +146,6 @@ 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 --