Skip to content

refactor: review Kleene algebra axioms#35963

Open
Parcly-Taxel wants to merge 10 commits intoleanprover-community:masterfrom
Parcly-Taxel:kleene-axioms
Open

refactor: review Kleene algebra axioms#35963
Parcly-Taxel wants to merge 10 commits intoleanprover-community:masterfrom
Parcly-Taxel:kleene-axioms

Conversation

@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

@Parcly-Taxel Parcly-Taxel commented Mar 2, 2026

Derive

one_add_mul_kstar (a : α) : 1 + a * a∗ = a∗
one_add_kstar_mul (a : α) : 1 + a∗ * a = a∗

which is Proposition 2 in Kozen's 1994 paper.

We also remove the bot and bot_le fields in IdemSemiring, since the remaining axioms already show 0 ≤ a for all a.

@Parcly-Taxel Parcly-Taxel added the t-algebra Algebra (groups, rings, fields, etc) label Mar 2, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 2, 2026

PR summary cd57315234

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance (priority := 100) IdemSemiring.toCanonicallyOrderedAdd : CanonicallyOrderedAdd α
+ instance (priority := 100) IdemSemiring.toIsOrderedAddMonoid : IsOrderedAddMonoid α
+ one_add_kstar_mul
+ one_add_mul_kstar
- instance (priority := 100) IdemSemiring.toCanonicallyOrderedAdd :
- instance (priority := 100) IdemSemiring.toIsOrderedAddMonoid :
- instance (priority := 100) IdemSemiring.toOrderBot [IdemSemiring α] : OrderBot α
-+-+ instIdemSemiring

You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Copy link
Copy Markdown
Collaborator

@vihdzp vihdzp left a comment

Choose a reason for hiding this comment

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

This looks reasonable to me, but I'm not an expert in this area, so I won't give explicit approval.

@dagurtomas dagurtomas added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 12, 2026
@dagurtomas dagurtomas removed their assignment Mar 12, 2026
@Parcly-Taxel Parcly-Taxel removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 13, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

6 participants