Skip to content
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.

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

Add left- and right- Pointwise congruence for _++_ on List #2426

Merged
merged 4 commits into from
Aug 14, 2024

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Jul 2, 2024

Fixes #1131

NB: no CHANGELOG (yet), but adds:

  • to Data.List.Relation.Binary.Pointwise
  ++⁺ʳ : Reflexive R   xs  Pointwise R ys zs  Pointwise R (xs ++ ys) (xs ++ zs)
  ++⁺ˡ : Reflexive R  Pointwise R ws xs   zs  Pointwise R (ws ++ zs) (xs ++ zs)
  • to Data.List.Relation.Binary.Equality.Setoid
  ++⁺ʳ :  xs {ys zs}  ys ≋ zs  xs ++ ys ≋ xs ++ zs
  ++⁺ˡ :  {ws xs}  ws ≋ xs   zs  ws ++ zs ≋ xs ++ zs

Issue:

  • the originating issue is 4 years old... (and should we have a policy on pruning such things?)
  • arguably, such lemmas (at least: the second pair) should be automatically derivable as ∙-congʳ and ∙-congˡ for the (Is)Magma structure/bundle defined on List in Add the Setoid-based Monoid on (List, [], _++_) #2393 ...
  • so it's possible (desirable?) that we mark this PR as status:duplicate and not merge after all (except perhaps the first pair of lemmas?)

UPDATED: added CHANGELOG, and revised the types of lemmas in response to @JacquesCarette 's comments below.

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Jul 4, 2024

Thanks @MatthewDaggitt : any opinions on the discussion points at the top?
Also: did not use LeftCongruent or RightCongruent for the lemma statements, but/and probably should have...? (Except that there then would have been the usual implicit/explicit quantification mismatch?)

Copy link
Contributor

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

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

While it would be nice to derive these through automation, we're kind of far from that. Let's have a full-featured library now, and worry about that later. So I'm all for merging this in.

src/Data/List/Relation/Binary/Pointwise.agda Outdated Show resolved Hide resolved
@MatthewDaggitt
Copy link
Contributor

the #1131 is 4 years old... (and should we have a policy on pruning such things?)

I'm happy for old issues to still float around if they haven't been solved.

so it's possible (desirable?) that we mark this PR as status:duplicate and not merge after all (except perhaps the first pair of lemmas?)

I think better that they exist first. We can then always refactor the implementation later.

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Jul 27, 2024

Have now added revised types for the new lemmas, and note the following:

  • ++⁺ʳ now has a type corresponding to the explicitly quantified version of Algebra.Definitions.LeftCongruent
  • ++⁺ˡ now has a type corresponding to the explicitly quantified version of Algebra.Definitions.RightCongruent
    (and explicit because "_++_ can't infer its arguments"... at least in the first case)

Which nomenclature/notation should be taken as canon? (Potential issue: I think that the use(s) of left/right superscript annotations in the Data.List.Relation* hierarchy are opposite to those of the Algebra.* congruence properties... sigh)

Barring the resolution of this question, I think this is (should be! ;-)) good to go now.

@MatthewDaggitt
Copy link
Contributor

Which nomenclature/notation should be taken as canon? (Potential issue: I think that the use(s) of left/right superscript annotations in the Data.List.Relation* hierarchy are opposite to those of the Algebra.* congruence properties... sigh)

Sigh as well. I think it's better to be consistent within Data.List.Relation...

@jamesmckinna
Copy link
Contributor Author

Which nomenclature/notation should be taken as canon? (Potential issue: I think that the use(s) of left/right superscript annotations in the Data.List.Relation* hierarchy are opposite to those of the Algebra.* congruence properties... sigh)

Sigh as well. I think it's better to be consistent within Data.List.Relation...

Ok, I'll leave the names as is, but v3.0 or hypothetical-rewrite to correct this inconsistency... one day?

@jamesmckinna
Copy link
Contributor Author

@JacquesCarette are you now happy with the revisions to this?

@JacquesCarette JacquesCarette added this pull request to the merge queue Aug 13, 2024
Merged via the queue into agda:master with commit a6da449 Aug 14, 2024
2 checks passed
@jamesmckinna jamesmckinna deleted the issue1131 branch December 22, 2024 13:00
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Add left and right versions of ++⁺ for pointwise relations
3 participants