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

Refactor Data.List.Relation.Binary.Permutation.*, part I #2333

Merged
merged 42 commits into from
Sep 28, 2024

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Mar 28, 2024

Part I of a project to fix #1354

Highlights of the refactoring, cf. #2317 :

  • Definitions don't change, so this is a 'conservative' first go, non-breaking for v2.1
  • Additions to each of Propositional and Setoid and their Properties reconcile, more or less, the shared parts of the API
  • Remove appeals to 'buggy' PermutationReasoning additional syntax Parsing problems with the PermutationReasoning combinators in Data.List.Relation.Binary.Permutation.Propositional #2319
  • General tidying up: variables etc.
  • Equivalence in Propositional of the relation and the Setoid (setoid _) instance
  • Refactor Propositional.product-↭ in that spirit
  • Setoid changes the proof of ↭-trans in terms of new lemmas ↭-transˡ-≋ and ↭-transʳ-≋; with them a sharpening of the analysis in split via a new lemma ↭-split (purely structural; no WF-induction required)
  • Move to Homogeneous, and deprecation in Setoid, of steps; towards removing legacy cruft now rendered obsolete by the above analysis
  • (BUG?) steps is deprecated in Setoid, but doesn't trigger the WARNING_ON_USAGE when the qualified-imported module Permutation S is opened in Properties
  • Final tidy up of BagAndSetEquality finishing off refactoring begun in Refactor Data.List.Relation.Binary.BagAndSetEquality #2321

Not done, but could be:

  • refactor Setoid.Properties into Core and derived
  • ditto. for Propositional, and then rederived via the Setoid (setoid _) instance (eg even the drop... properties can be derived from those in Setoid)

Won't do:

@MatthewDaggitt
Copy link
Contributor

Generally looks good though! The drastic reduction in proof length is pretty great!

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Mar 28, 2024

@MatthewDaggitt I think that's all of your review comments handled now! But leaving certain one of the conversations unresolved until you're happy... ;-)

Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

Other than that looks great!

src/Data/List/Relation/Binary/Permutation/Homogeneous.agda Outdated Show resolved Hide resolved
Comment on lines +48 to +55
↭-refl : Reflexive _↭_
↭-refl = refl

↭-prep : ∀ x → xs ↭ ys → x ∷ xs ↭ x ∷ ys
↭-prep = prep

↭-swap : ∀ x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
↭-swap = swap
Copy link
Member

Choose a reason for hiding this comment

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

As always I am going to be annoying and complain that I don't like prefixed
names because users can either use the short names or import the module
qualified if they need to manually disambiguate.

The same goes for split being renamed to ↭-split (although in that case
the name split is already pretty poor IMO).

Copy link
Contributor Author

@jamesmckinna jamesmckinna Apr 6, 2024

Choose a reason for hiding this comment

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

@gallais I don't find the comment annoying!
What I find annoying is the the abstraction failure when explicitly exporting constructors from an inductive definition which should remain (externally, to clients) abstract, IMHO (cf. z<s in Data.Nat.Base, and 0<1+n in Data.Nat.Properties, not that I/we are entirely consistent in enforcing this...)
Since this is also part of a greater project of refactoring Permutation towards completing #1761 / #1354 I wanted to make sure that in Properties, references to the constructors were abstracted on those lines before proceeding further.

As regards ↭-split, this is not a renaming of split, but a significant generalisation which permits a much improved proof of dropMiddleElement... so a cognate name change is needed to reflect the 'better' typing! As for giving it a better name, I'm open to suggestions!

@jamesmckinna
Copy link
Contributor Author

Modulo @gallais 's comment, and my (attempted) rebuttal, I think that this is good to go @MatthewDaggitt unless there are review comments of yours that you are not happy have been dealt with...?

@jamesmckinna
Copy link
Contributor Author

At some point, the merge conflict resolution (probably thanks to me) went wrong, so fixing things now...

@JacquesCarette JacquesCarette modified the milestones: v2.1, v2.2 Jun 5, 2024
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Sep 3, 2024

Resolving latest round of merge conflicts exposed some issues with CHANGELOG (incl. a bug in that for #2418 ), which I've attempted to correctly rectify, but until this is merged, they'll probably go round and round in circles... sigh.

Meanwhile, there are still the (potentially) unresolved comments form @gallais about naming/synonyms for constructors, but I think these can be postponed until subsequent parts of this overall plan to revise/reform Permutation get implemented?

@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Sep 8, 2024

Hmmm.... fixing the merge conflict may need a bit more thought. UPDATED: I think that works now... Nope, something seems to have gone wrong somewhere. The product/All NonZero lemmas seem to have got bumped out of place? Hopefully fixed now!

jamesmckinna and others added 3 commits September 9, 2024 10:21
Deleted spurious attribution of the lemmas in `Data.List.Properties` about `product` to `Data.List.Relation.Unary.All.Properties`. Hope this fixes things now!
@MatthewDaggitt MatthewDaggitt added this pull request to the merge queue Sep 28, 2024
Merged via the queue into agda:master with commit 45a46f7 Sep 28, 2024
2 checks passed
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.

Reimplement Permutation.Propositional in terms of Permutation.Setoid
4 participants