From b176ea4d798313db67adee34970ae732b1b2979e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 1 Apr 2026 12:24:38 +0100 Subject: [PATCH 1/3] [ fix ] #2865 for `Data.Tree.AVL{.Indexed}.Relation.Unary.Any` --- CHANGELOG.md | 10 +++++++ .../Tree/AVL/Indexed/Relation/Unary/Any.agda | 30 +++++++++++++++---- src/Data/Tree/AVL/Relation/Unary/Any.agda | 28 +++++++++++++---- 3 files changed, 57 insertions(+), 11 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 99dea4e749..27c3441ac7 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -397,6 +397,16 @@ Additions to existing modules showAtPrecision : ℕ → ℚᵘ → String ``` +* In `Data.Tree.AVL.Relation.Indexed.Unary.Any`: + ```agda + satisfiable ↦ satisfiable⁺ + ``` + +* In `Data.Tree.AVL.Relation.Unary.Any`: + ```agda + satisfiable ↦ satisfiable⁺ + ``` + * In `Data.Vec.Properties`: ```agda map-removeAt : ∀ (f : A → B) (xs : Vec A (suc n)) (i : Fin (suc n)) → diff --git a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda index c81599da2a..b215d5b672 100644 --- a/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda +++ b/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda @@ -80,7 +80,7 @@ lookupKey = key ∘′ lookup -- If any element satisfies P, then P is satisfied. -satisfied : Any P t → ∃ P +satisfied : Any P t → Satisfiable P satisfied (here p) = -, p satisfied (left p) = satisfied p satisfied (right p) = satisfied p @@ -109,8 +109,26 @@ any? P? (leaf _) = no λ () any? P? (node kv l r bal) = map′ fromSum toSum (P? kv ⊎? any? P? l ⊎? any? P? r) -satisfiable : ∀ {k l u} → l <⁺ [ k ] → [ k ] <⁺ u → - Satisfiable (P ∘ (k ,_)) → - Satisfiable {A = Tree V l u 1} (Any P) -satisfiable {k = k} lb ub sat = node (k , proj₁ sat) (leaf lb) (leaf ub) ∼0 - , here (proj₂ sat) +satisfiable⁺ : ∀ {k l u} → l <⁺ [ k ] → [ k ] <⁺ u → + Satisfiable (P ∘ (k ,_)) → + Satisfiable {A = Tree V l u 1} (Any P) +satisfiable⁺ {k = k} lb ub sat = node (k , proj₁ sat) (leaf lb) (leaf ub) ∼0 + , here (proj₂ sat) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +satisfiable = satisfiable⁺ +{-# WARNING_ON_USAGE satisfiable +"Warning: satisfiable was deprecated in v2.4. +Please use satisfiable⁺ instead. Moreover, +the name satisfied will be renamed in v3.0 +to satisfiable, so users should refactor +as soon as they can." +#-} diff --git a/src/Data/Tree/AVL/Relation/Unary/Any.agda b/src/Data/Tree/AVL/Relation/Unary/Any.agda index 5efc9363a3..77577708bc 100644 --- a/src/Data/Tree/AVL/Relation/Unary/Any.agda +++ b/src/Data/Tree/AVL/Relation/Unary/Any.agda @@ -56,9 +56,9 @@ lookup (tree p) = AVLₚ.lookup p lookupKey : Any P t → Key lookupKey (tree p) = AVLₚ.lookupKey p --- If any element satisfies P, then P is satisfied. +-- If any element satisfies P, then P is satisfiable. -satisfied : Any P t → ∃ P +satisfied : Any P t → Satisfiable P satisfied (tree p) = AVLₚ.satisfied p ------------------------------------------------------------------------ @@ -67,6 +67,24 @@ satisfied (tree p) = AVLₚ.satisfied p any? : Decidable P → Decidable (Any {V = V} P) any? P? (tree p) = map′ tree (λ where (tree p) → p) (AVLₚ.any? P? p) -satisfiable : (k : Key) → Satisfiable (P ∘ (k ,_)) → Satisfiable (Any {V = V} P) -satisfiable k sat = Product.map tree tree - $ AVLₚ.satisfiable Indexed.⊥⁺<[ k ] Indexed.[ k ]<⊤⁺ sat +satisfiable⁺ : (k : Key) → Satisfiable (P ∘ (k ,_)) → Satisfiable (Any {V = V} P) +satisfiable⁺ k sat = Product.map tree tree + $ AVLₚ.satisfiable⁺ Indexed.⊥⁺<[ k ] Indexed.[ k ]<⊤⁺ sat + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +satisfiable = satisfiable⁺ +{-# WARNING_ON_USAGE satisfiable +"Warning: satisfiable was deprecated in v2.4. +Please use satisfiable⁺ instead. Moreover, +the name satisfied will be renamed in v3.0 +to satisfiable, so users should refactor +as soon as they can." +#-} From 4493267a1d530fcd70380dd1af5f75e791614ede Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 1 Apr 2026 12:59:35 +0100 Subject: [PATCH 2/3] refactor: knock-off the other instances --- CHANGELOG.md | 15 +++++++++++++++ src/Data/List/Relation/Unary/First.agda | 24 +++++++++++++++++++++--- src/Data/Maybe/Relation/Unary/Any.agda | 24 +++++++++++++++++++++--- src/Data/Vec/Relation/Unary/Any.agda | 24 +++++++++++++++++++++--- 4 files changed, 78 insertions(+), 9 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 27c3441ac7..e9cc6d180a 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -313,6 +313,16 @@ Additions to existing modules filter-swap : filter P? ∘ filter Q? ≗ filter Q? ∘ filter P? ``` +* In `Data.List.Relation.Unary.First`: + ```agda + satisfiable ↦ satisfiable⁺ + ``` + +* In `Data.Maybe.Relation.Unary.Any`: + ```agda + satisfiable ↦ satisfiable⁺ + ``` + * In `Data.Nat.Divisibility`: ```agda m∣n⇒m^o∣n^o : ∀ o → m ∣ n → m ^ o ∣ n ^ o @@ -461,6 +471,11 @@ Additions to existing modules padRight m≤n x (updateAt xs i f) ``` +* In `Data.Vec.Relation.Unary.Any`: + ```agda + satisfiable ↦ satisfiable⁺ + ``` + * In `Relation.Binary.Construct.Add.Extrema.NonStrict`: ```agda ≤±-respˡ-≡ : _≤±_ Respectsˡ _≡_ diff --git a/src/Data/List/Relation/Unary/First.agda b/src/Data/List/Relation/Unary/First.agda index ee0311d527..b418ae33ff 100644 --- a/src/Data/List/Relation/Unary/First.agda +++ b/src/Data/List/Relation/Unary/First.agda @@ -78,11 +78,11 @@ module _ {p q} {P : Pred A p} {Q : Pred A q} where index-satisfied [ qx ] = qx index-satisfied (_ ∷ pqxs) = index-satisfied pqxs - satisfied : ∀ {xs} → First P Q xs → ∃ Q + satisfied : ∀ {xs} → First P Q xs → Satisfiable Q satisfied pqxs = -, index-satisfied pqxs - satisfiable : Satisfiable Q → Satisfiable (First P Q) - satisfiable (x , qx) = List.[ x ] , [ qx ] + satisfiable⁺ : Satisfiable Q → Satisfiable (First P Q) + satisfiable⁺ (x , qx) = List.[ x ] , [ qx ] ------------------------------------------------------------------------ -- Decidability results @@ -105,3 +105,21 @@ module _ {q} {Q : Pred A q} where toAny : ∀ {p} {P : Pred A p} → First P Q ⊆ Any Q toAny [ qx ] = here qx toAny (_ ∷ pqxs) = there (toAny pqxs) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +satisfiable = satisfiable⁺ +{-# WARNING_ON_USAGE satisfiable +"Warning: satisfiable was deprecated in v2.4. +Please use satisfiable⁺ instead. Moreover, +the name satisfied will be renamed in v3.0 +to satisfiable, so users should refactor +as soon as they can." +#-} diff --git a/src/Data/Maybe/Relation/Unary/Any.agda b/src/Data/Maybe/Relation/Unary/Any.agda index b35d033588..2c9f0658f2 100644 --- a/src/Data/Maybe/Relation/Unary/Any.agda +++ b/src/Data/Maybe/Relation/Unary/Any.agda @@ -38,7 +38,7 @@ module _ {a p} {A : Set a} {P : Pred A p} where map : ∀ {q} {Q : Pred A q} → P ⊆ Q → Any P ⊆ Any Q map f (just px) = just (f px) - satisfied : ∀ {x} → Any P x → ∃ P + satisfied : ∀ {x} → Any P x → Satisfiable P satisfied (just p) = -, p ------------------------------------------------------------------------ @@ -72,5 +72,23 @@ module _ {a p} {A : Set a} {P : Pred A p} where irrelevant : Irrelevant P → Irrelevant (Any P) irrelevant P-irrelevant (just p) (just q) = cong just (P-irrelevant p q) - satisfiable : Satisfiable P → Satisfiable (Any P) - satisfiable P-satisfiable = Product.map just just P-satisfiable + satisfiable⁺ : Satisfiable P → Satisfiable (Any P) + satisfiable⁺ P-satisfiable = Product.map just just P-satisfiable + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 2.4 + +satisfiable = satisfiable⁺ +{-# WARNING_ON_USAGE satisfiable +"Warning: satisfiable was deprecated in v2.4. +Please use satisfiable⁺ instead. Moreover, +the name satisfied will be renamed in v3.0 +to satisfiable, so users should refactor +as soon as they can." +#-} diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index 157d275cf9..0e07039e02 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -77,12 +77,30 @@ any? : Decidable P → ∀ {n} → Decidable (Any P {n}) any? P? [] = no λ() any? P? (x ∷ xs) = Dec.map′ fromSum toSum (P? x ⊎? any? P? xs) -satisfiable : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n}) -satisfiable (x , p) {zero} = x ∷ [] , here p -satisfiable (x , p) {suc n} = Product.map (x ∷_) there (satisfiable (x , p)) +satisfiable⁺ : Satisfiable P → ∀ {n} → Satisfiable (Any P {suc n}) +satisfiable⁺ (x , p) {zero} = x ∷ [] , here p +satisfiable⁺ (x , p) {suc n} = Product.map (x ∷_) there (satisfiable⁺ (x , p)) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. any = any? {-# WARNING_ON_USAGE any "Warning: any was deprecated in v1.4. Please use any? instead." #-} + +-- Version 2.4 + +satisfiable = satisfiable⁺ +{-# WARNING_ON_USAGE satisfiable +"Warning: satisfiable was deprecated in v2.4. +Please use satisfiable⁺ instead. Moreover, +the name satisfied will be renamed in v3.0 +to satisfiable, so users should refactor +as soon as they can." +#-} From edac0c4f2b3f1113c21bcfb24cf9c35bb97c2996 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 1 Apr 2026 13:01:57 +0100 Subject: [PATCH 3/3] fix: name --- src/Data/Vec/Relation/Unary/Any.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda index 0e07039e02..2b45526a61 100644 --- a/src/Data/Vec/Relation/Unary/Any.agda +++ b/src/Data/Vec/Relation/Unary/Any.agda @@ -66,7 +66,7 @@ lookup : Any P xs → A lookup {xs = xs} p = Vec.lookup xs (index p) -- If any element satisfies P, then P is satisfied. -satisfied : Any P xs → ∃ P +satisfied : Any P xs → Satisfiable P satisfied (here px) = _ , px satisfied (there pxs) = satisfied pxs