Skip to content

[ refactor ] Simplify Data.List.Relation.Binary.Lex.NonStrict.<-asymmetric #2679

@jamesmckinna

Description

@jamesmckinna
Contributor

Current version:

    <-asymmetric : IsEquivalence _≈_  _≼_ Respects₂ _≈_ 
                   Antisymmetric _≈_ _≼_  Asymmetric _<_
    <-asymmetric eq resp antisym  =
      Strict.<-asymmetric sym (Conv.<-resp-≈ _ _ eq resp)
                        (Conv.<-asym _≈_ _ antisym)
                        where open IsEquivalence eq

only uses the sym : Symmetric _≈_ property from IsEquivalence, so this lemma is unnecessarily restrictive.

Suggest: refactor to streamline the type (breaking), unless we regard the above as a bug?

More generally, it seems as though the List and Vec versions of Lex might benefit from a more thorough reorganisation/refactoring to simplify their (common, but different!) structure and dependencies, but I'm still looking at this cf. #2671

Activity

jmougeot

jmougeot commented on Mar 19, 2025

@jmougeot
Contributor

I tried to make the change, but it actually requires a deeper modification since Conv.<-resp-≈ relies on transitivity:
<-respʳ-≈ sym trans respʳ, <-respˡ-≈ trans respˡ.

This is absolutely necessary in the function:

<-asymmetric : Symmetric _≈_ → _≺_ Respects₂ _≈_ → Asymmetric _≺_ → Asymmetric _<_ <-asymmetric sym resp as = asym where irrefl : Irreflexive _≈_ _≺_ irrefl = asym⇒irr resp sym as ...

We could change IsEquivalence to PartialEquivalence, but I don’t think we would gain anything from it.

jamesmckinna

jamesmckinna commented on Mar 19, 2025

@jamesmckinna
ContributorAuthor

Thanks @jmougeot for the fine-grained analysis!
In fact, looking also at the Vec versions of these properties, where care is taken to distinguish IsPartialEquivalence from IsEquivalence, I do think the change is worth it. But after your efforts on #2671 I'm very much of the opinion that we should try to do a wholesale reorganisation of Lex for each of List and Vec, to try to identify, as far as possible, a 'common' API. cf. #2682 etc.

Not only that, but the artificial bundling of sym and trans as an instance of IsPartialEquivalence just seems to make the dependency structure unnecessarily complicated, rather than, in the structure/bundle deployment of various lemmas about these relations, appealing directly to the relevant properties at hand. This is the case in each of the cases (List, Vec and even Product) of Data.*.Relation.Binary.Lex.*Strict...

jmougeot

jmougeot commented on Mar 26, 2025

@jmougeot
Contributor

IsPartialEquivalence isn’t used a lot. Would it be worth changing the dependency?

IsPartialEquivalence.txt

jamesmckinna

jamesmckinna commented on Mar 26, 2025

@jamesmckinna
ContributorAuthor

IsPartialEquivalence isn’t used a lot. Would it be worth changing the dependency?

I think that that is a separate question, and... perhaps a case of PR-creep, if I understand you correctly. But that doesn't mean that IsPartialEquiavlence won't be used more in future (see #2677 for example), and certainly I wouldn't consider updating the Construct.* modules... precisely because of the design of the existing hierarchy...

But this PR is really more about trying to identify a 'common' API for the lexicographic ordering(s) on Vec and List, and with that, the emphasis seems more to be about the 'atomic' properties such as Symmetric etc.

jamesmckinna

jamesmckinna commented on Mar 28, 2025

@jamesmckinna
ContributorAuthor

Closing now in favour of the wider scope of #2687

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

      Development

      No branches or pull requests

        Participants

        @jamesmckinna@jmougeot

        Issue actions

          [ refactor ] Simplify `Data.List.Relation.Binary.Lex.NonStrict.<-asymmetric` · Issue #2679 · agda/agda-stdlib