search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

adding associativity solver #432

Closed onestruggler closed 1 month ago

onestruggler commented 1 month ago

the solver solves the assoc equivalence automatically. E.g.,

(m ∘ l) ∘ (k ∘ j ∘ i ∘ h ∘ g) ∘ f ∘ (e ∘ d ∘ c) ∘ b ∘ a ≈ m ∘ (l ∘ k) ∘ (j ∘ i ∘ h) ∘ ((((g ∘ f) ∘ e) ∘ d) ∘ c) ∘ b ∘ a

onestruggler commented 1 month ago

Categories.Tactic.Category already has it. Sorry for my bad pull request.

Just curious, why the SqrtRig repo didn't use this tactic. I saw many manually associativity proof there.

JacquesCarette commented 1 month ago

(I'm not 100% sure what repo you mean by 'SqrtRig'? Do you mean SqrtPi ?)

If that's so then mainly it's because I got used to doing them this way in agda-categories where we don't want to rely too much on tactics. But for application code like that, it would make sense to shift.

And no worries: all contributions welcome, even if they turn out to be redundant in the end.

onestruggler commented 1 month ago

Sorry for my typo. Yes, I mean SqrtPi.

Thanks for the explanation. It makes sense to keep SqrtPi less dependent.

I am working on proving more circuit equations in SqrtPi, mainly the ones proved in your paper but not in Agda. Some cases involve many associativity and rewritings. So, I also have some code for automating rewriting. I will make a pull request to SqrtPi soon after I finish proving some equations showing its usability.

Thanks for the kind words and encouragement. Also sorry in advance for my ugly code to be seen to you and other reviewers.

From: Jacques Carette @.> Sent: Friday, August 9, 2024 7:33 PM To: agda/agda-categories @.> Cc: Xiaoning Bian @.>; State change @.> Subject: Re: [agda/agda-categories] adding associativity solver (PR #432)

CAUTION: The Sender of this email is not from within Dalhousie.

(I'm not 100% sure what repo you mean by 'SqrtRig'? Do you mean SqrtPihttps://github.com/JacquesCarette/SqrtPi ?)

If that's so then mainly it's because I got used to doing them this way in agda-categories where we don't want to rely too much on tactics. But for application code like that, it would make sense to shift.

And no worries: all contributions welcome, even if they turn out to be redundant in the end.

— Reply to this email directly, view it on GitHubhttps://github.com/agda/agda-categories/pull/432#issuecomment-2277744636, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AE3BG3TTWKYZXPNKHZWQ7NDZQSSGZAVCNFSM6AAAAABMGY2NGCVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDENZXG42DINRTGY. You are receiving this because you modified the open/close state.Message ID: @.***>