Skip to content

[ refactor ] Data.List.Relation.Binary.Sublist.Propositional.Properties #2808

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

[ refactor ] Data.List.Relation.Binary.Sublist.Propositional.Properties #2808

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
dd76391
refactor: see #2525
jamesmckinna Aug 13, 2025
ea227ae
refactor: make intensional equality extensional
jamesmckinna Aug 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,17 @@ Additions to existing modules
≟-≢ : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
```

* In `Data.List.Relation.Binary.Sublist.Propositional.Properties`:
```agda
lookup≗Any-resp-⊆ : lookup xs⊆ys ≗ Any-resp-⊆ {P = P} xs⊆ys
```

* In `Data.List.Relation.Binary.Sublist.Setoid.Properties`:
```agda
All-resp-⊆ : (P Respects _≈_) → (All P) Respects _⊇_
Any-resp-⊆ : (P Respects _≈_) → (Any P) Respects _⊆_
```

* In `Data.Nat.Properties`:
```agda
≟-≢ : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
Expand Down
4 changes: 2 additions & 2 deletions src/Data/List/Relation/Binary/Sublist/Propositional.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ open import Relation.Binary.Bundles using (Preorder; Poset)
open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder)
open import Relation.Binary.Definitions using (Antisymmetric)
open import Relation.Binary.PropositionalEquality.Core
using (subst; _≡_; refl)
using (resp; _≡_; refl)
open import Relation.Binary.PropositionalEquality.Properties
using (setoid; isEquivalence)
open import Relation.Unary using (Pred)
Expand All @@ -40,7 +40,7 @@ open SetoidSublist (setoid A) public
module _ {p} {P : Pred A p} where

lookup : ∀ {xs ys} → xs ⊆ ys → Any P xs → Any P ys
lookup = SetoidSublist.lookup (setoid A) (subst _)
lookup = SetoidSublist.lookup (setoid A) (resp _)

------------------------------------------------------------------------
-- Relational properties
Expand Down
33 changes: 23 additions & 10 deletions src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ private

module _ {A : Set a} where
open SetoidProperties (setoid A) public
hiding (map⁺; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc)
hiding (map⁺; All-resp-⊆; Any-resp-⊆; ⊆-trans-idˡ; ⊆-trans-idʳ; ⊆-trans-assoc)

------------------------------------------------------------------------
-- Relationship between _⊆_ and Setoid._⊆_
Expand Down Expand Up @@ -103,17 +103,17 @@ map⁺ f = SetoidProperties.map⁺ (setoid _) (setoid _) (cong f)
------------------------------------------------------------------------
-- Relationships to other predicates

module _ {P : Pred A ℓ} where

-- All P is a contravariant functor from _⊆_ to Set.

All-resp-⊆ : {P : Pred A ℓ} → (All P) Respects _⊇_
All-resp-⊆ [] [] = []
All-resp-⊆ (_ ∷ʳ p) (_ ∷ xs) = All-resp-⊆ p xs
All-resp-⊆ (refl ∷ p) (x ∷ xs) = x ∷ All-resp-⊆ p xs
All-resp-⊆ : (All P) Respects _⊇_
All-resp-⊆ = SetoidProperties.All-resp-⊆ (setoid _) (≡.resp P)

-- Any P is a covariant functor from _⊆_ to Set.

Any-resp-⊆ : {P : Pred A ℓ} → (Any P) Respects _⊆_
Any-resp-⊆ = lookup
Any-resp-⊆ : (Any P) Respects _⊆_
Any-resp-⊆ = SetoidProperties.Any-resp-⊆ (setoid _) (≡.resp P)

------------------------------------------------------------------------
-- Functor laws for All-resp-⊆
Expand All @@ -137,14 +137,22 @@ All-resp-⊆-trans {τ = [] } ([] ) [] = refl
------------------------------------------------------------------------
-- Functor laws for Any-resp-⊆ / lookup

lookup≗Any-resp-⊆ : ∀ {P : Pred A ℓ} (xs⊆ys : xs ⊆ ys) →
lookup xs⊆ys ≗ Any-resp-⊆ {P = P} xs⊆ys
lookup≗Any-resp-⊆ (y ∷ʳ xs⊆ys) = cong there ∘ lookup≗Any-resp-⊆ xs⊆ys
lookup≗Any-resp-⊆ (x ∷ xs⊆ys) (here px) = refl
lookup≗Any-resp-⊆ (x ∷ xs⊆ys) (there p) = cong there (lookup≗Any-resp-⊆ xs⊆ys p)

-- First functor law: identity.

Any-resp-⊆-refl : ∀ {P : Pred A ℓ} →
Any-resp-⊆ ⊆-refl ≗ id {A = Any P xs}
Any-resp-⊆-refl (here p) = refl
Any-resp-⊆-refl (there i) = cong there (Any-resp-⊆-refl i)

lookup-⊆-refl = Any-resp-⊆-refl
lookup-⊆-refl : ∀ {P : Pred A ℓ} →
lookup ⊆-refl ≗ id {A = Any P xs}
lookup-⊆-refl p = trans (lookup≗Any-resp-⊆ ⊆-refl p) (Any-resp-⊆-refl p)

-- Second functor law: composition.

Expand All @@ -156,7 +164,12 @@ Any-resp-⊆-trans {τ = _ ∷ _} (_ ∷ τ′) (there i) = cong there (Any-
Any-resp-⊆-trans {τ = refl ∷ _} (_ ∷ τ′) (here _) = refl
Any-resp-⊆-trans {τ = [] } [] ()

lookup-⊆-trans = Any-resp-⊆-trans
lookup-⊆-trans : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} (τ′ : ys ⊆ zs) →
lookup {P = P} (⊆-trans τ τ′) ≗ lookup τ′ ∘ lookup τ
lookup-⊆-trans ys⊆zs p =
trans (lookup≗Any-resp-⊆ (⊆-trans _ ys⊆zs) p)
(trans (Any-resp-⊆-trans ys⊆zs p)
(lookup≗Any-resp-⊆ ys⊆zs (lookup _ p)))

------------------------------------------------------------------------
-- The `lookup` function for `xs ⊆ ys` is injective.
Expand All @@ -167,7 +180,7 @@ lookup-⊆-trans = Any-resp-⊆-trans
lookup-injective : ∀ {P : Pred A ℓ} {τ : xs ⊆ ys} {i j : Any P xs} →
lookup τ i ≡ lookup τ j → i ≡ j
lookup-injective {τ = _ ∷ʳ _} = lookup-injective ∘′ there-injective
lookup-injective {τ = x≡y ∷ _} {here _} {here _} = cong here ∘′ subst-injective x≡y ∘′ here-injective
lookup-injective {τ = refl ∷ _} {here _} {here _} = cong here ∘′ here-injective
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This change now makes the comment right after it not make sense?

-- Note: instead of using subst-injective, we could match x≡y against refl on the lhs.
-- However, this turns the following clause into a non-strict match.
lookup-injective {τ = _ ∷ _} {there _} {there _} = cong there ∘′ lookup-injective ∘′ there-injective
Expand Down
28 changes: 24 additions & 4 deletions src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,18 +12,20 @@ open import Relation.Binary.Bundles using (Setoid)
module Data.List.Relation.Binary.Sublist.Setoid.Properties
{c ℓ} (S : Setoid c ℓ) where

open import Data.List.Base hiding (_∷ʳ_)
open import Data.List.Base hiding (_∷ʳ_; lookup)
open import Data.List.Properties using (++-identityʳ)
open import Data.List.Relation.Unary.Any using (Any)
open import Data.List.Relation.Unary.All using (All; tabulateₛ)
open import Data.List.Relation.Unary.All
using (All; []; _∷_; tabulateₛ)
import Data.Maybe.Relation.Unary.All as Maybe
open import Data.Nat.Base using (ℕ; _≤_; _≥_)
import Data.Nat.Properties as ℕ
open import Data.Product.Base using (∃; _,_; proj₂)
open import Function.Base
open import Function.Bundles using (_⇔_; _⤖_)
open import Level
open import Relation.Binary.Definitions using () renaming (Decidable to Decidable₂)
open import Relation.Binary.Definitions
using (_Respects_) renaming (Decidable to Decidable₂)
import Relation.Binary.Properties.Setoid as SetoidProperties
open import Relation.Binary.PropositionalEquality.Core as ≡
using (_≡_; refl; sym; cong; cong₂)
Expand All @@ -42,7 +44,8 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
as HeteroProperties
import Data.List.Membership.Setoid as SetoidMembership

open Setoid S using (_≈_; trans) renaming (Carrier to A; refl to ≈-refl)
open Setoid S using (_≈_; trans)
renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym)
open SetoidEquality S using (_≋_; ≋-refl; ≋-reflexive; ≋-setoid)
open SetoidSublist S hiding (map)
open SetoidProperties S using (≈-preorder)
Expand Down Expand Up @@ -106,6 +109,23 @@ module _ (≈-assoc : ∀ {w x y z} (p : w ≈ x) (q : x ≈ y) (r : y ≈ z)
⊆-trans-assoc [] [] [] = refl


------------------------------------------------------------------------
-- Relationships to other predicates

module _ {P : Pred A p} (resp : P Respects _≈_) where

-- All P is a contravariant functor from _⊆_ to Set.

All-resp-⊆ : (All P) Respects _⊇_
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The name says the opposite of the property?!?!?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The name is legacy, back-ported from Propositional. But I agree, it's maybe idiotic to have retained it.

All-resp-⊆ [] [] = []
All-resp-⊆ (_ ∷ʳ p) (x ∷ xs) = All-resp-⊆ p xs
All-resp-⊆ (x≈y ∷ p) (x ∷ xs) = resp (≈-sym x≈y) x ∷ All-resp-⊆ p xs

-- Any P is a covariant functor from _⊆_ to Set.

Any-resp-⊆ : (Any P) Respects _⊆_
Any-resp-⊆ = lookup resp

------------------------------------------------------------------------
-- Reasoning over sublists
------------------------------------------------------------------------
Expand Down