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.

Sign up for GitHub

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

Jump to bottom

Codyroux/boolean ring #708

Open
wants to merge 69 commits into
base: main
Choose a base branch
from
Open

Codyroux/boolean ring #708

wants to merge 69 commits into from
+2,065 −2

Conversation

codyroux
Copy link
Contributor

@codyroux codyroux commented Oct 22, 2024 •
edited by github-actions bot
Loading

Tie the knot from the excellent work from @jjtowery: prove that a certain messy equation is exactly what is needed for a Boolean Algebra. The proof is in 3 steps:

  1. Prove that the complicated equation (equation 345169) implies the three original laws put forth by Sheffer in "A set of five independent postulates for Boolean algebras, with application to logical constants". Done by @jjtowery
  2. Prove that those 3 laws imply the structure of a "boolean ring", roughly following that paper. Done by myself.
  3. Prove that a "boolean ring" is a boolean algebra (in particular, define the order and prove that it is a nice lattice). Also done by myself, following the excellent wikipedia article: https://en.wikipedia.org/wiki/Boolean_algebra_(structure).

Closes #354

jjtowery and others added 21 commits October 10, 2024 02:14
@jjtowery
Sheffer
35dbc4d
@jjtowery
Automated proofs
6d86b73
@jjtowery
Add potential proof strategy for le_trans.
599c5a2
@jjtowery
Do it properly.
a0c9b6c
@codyroux
Add a purely equational definition for boolean rings.
db067ad
@codyroux
Merge branch 'main' of https://github.com/teorth/equational_theories …
d4209cf 
…into codyroux/boolean-ring
@Command-Master @codyroux
LINEAR: Formalize the proof of 1117 !=> 2441 (teorth#695)
43e92d1 
The construction can be simplified to `ℤ`, using floor division and
multiplication by 2.

Closes teorth#691
@Command-Master @codyroux
AD_HOC: Formalize the proof of 1437 !=> 4269 (teorth#696)
140149e 
null

Closes teorth#690
@teorth @codyroux
Update conjectures (teorth#697)
f0242b6 
Incorporated recent progress on outstanding equations
@teorth @codyroux
add 1518 conjecture (teorth#698)
4c8988d
@codyroux
Remove the assumption of associativity in boolean rings. A bit tough!
5868cfb
@fpvandoorn @codyroux
fix: typo (teorth#700)
6bee721
@vlad902 @codyroux
Add a blueprint correction from Zoltan (teorth#699)
025495c 
A correction from Zoltan as noted here
teorth#649 (comment)
@teorth @codyroux
add conjecture, link to finite magma constructions (teorth#703)
bd455e2
@teorth @codyroux
add commentary (teorth#704)
a652897 
also update some older commentary with new progress
@vlad902 @codyroux
Add support for explicitly Finite non-implications (teorth#702)
056d0df 
As discussed in [1], I add support to the @[equational_result] attribute
to parse non-implication theorems with Finite typeclasses. I then add
support to `extract_implications` to specify `--finite-only` to limit
results to finite non-implications.

In addition, I also add some additional checking to @[equational_result]
as previously it would silently mis-parse theorems with the Finite
typeclass.

This was tested by generating `extract_implications` closure/unknowns
results before and after this change. When I included finite
non-implications (not in this change), the results correctly showed them
with `--finite-only`, while the results without `--finite-only` did not
change and match the results prior to this change.

[1]
https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/Proposal.3A.20Add.20Finite.20typeclasses.20to.20non-implications/near/477933508
@vlad902 @codyroux
Make Equation Explorer faster (teorth#705)
1841f78 
Cuts ~2.5s off the load time for me locally.

I verified that the stats line-up by comparing CSVs before/after (this
change optimizes stats calculation)
@codyroux
Whew, the Sheffer laws imply the boolean algebra laws.
bc0e9a8
@codyroux
Merge branch 'main' of https://github.com/jjtowery/equational_theories …
0d892c4 
…into codyroux/boolean-ring
@codyroux
Tie the knot with Equation345169: it defines a boolean algebra, for a…
9cf410d 
…ny inhabited sort.
@codyroux
Merge branch 'main' of https://github.com/teorth/equational_theories …
f20ac42 
…into codyroux/boolean-ring
@codyroux codyroux mentioned this pull request Oct 22, 2024
Open
@Shreyas4991
Copy link
Collaborator

Please use Mathlib's Boolean rings. I don't see why we need to re-invent that wheel

@Shreyas4991
Copy link
Collaborator

awaiting-author

@Shreyas4991 Shreyas4991 self-requested a review October 22, 2024 10:51
@pitmonticone pitmonticone added the awaiting-author Reviewers and maintainers are awaiting the author's response or fixes in response to review comments label Oct 22, 2024
@codyroux
Copy link
Contributor Author

codyroux commented Oct 22, 2024 •
edited
Loading

Ugh I could have sworn I checked. BooleanRing isn't referenced from BooleanAlgebra for some reason.

However the definition I wrote is "minimal" in the sense that it derives a number of things, including associativity, from a smaller set of equations. This is convenient when one is trying to prove that something is a BooleanRing, in particular a Magma satisfying Sheffer's axioms. Note also that the Mathlib one doesn't ask for commutativity (though it is easily derivable).

Worth noting that the join in my definition is just . + . rather than the (more standard) x + y + x * y from Mathlib. Both are used in different contexts, though the one in the Sheffer paper is the former.

However it's probably less work to show that the thing I defined is actually a Boolean ring proper than do the whole construction with \leq.

So what next? I could either:

  1. Just rename BooleanRing to something else, like MinimalBooleanAlg or something. I can do that today.
  2. Prove that this structure is actually a BooleanRing, (it is, it is if one redefines addition). I can't do this today.
  3. Eliminate the use of the intermediate structure, "inlining" the proof of associativity. This is a bit tedious and obscures the paper proof a bit IMHO, but whatever. Also can't do this today. Maybe Thursday?

Thoughts?

@codyroux
Copy link
Contributor Author

codyroux commented Oct 22, 2024 via email

@Shreyas4991
Copy link
Collaborator

Shreyas4991 commented Oct 22, 2024 •
edited
Loading

Ugh I could have sworn I checked. BooleanRing isn't referenced from BooleanAlgebra for some reason.

However the definition I wrote is "minimal" in the sense that it derives a number of things, including associativity, from a smaller set of equations. This is convenient when one is trying to prove that something is a BooleanRing, in particular a Magma satisfying Sheffer's axioms. Note also that the Mathlib one doesn't ask for commutativity (though it is easily derivable).

Worth noting that the join in my definition is just . + . rather than the (more standard) x + y + x * y from Mathlib. Both are used in different contexts, though the one in the Sheffer paper is the former.

However it's probably less work to show that the thing I defined is actually a Boolean ring proper than do the whole construction with \leq.

So what next? I could either:

1. Just rename `BooleanRing` to something else, like `MinimalBooleanAlg` or something. I can do that today.

2. Prove that this structure is actually a `BooleanRing`, (it is). I can't do this today.

3. Eliminate the use of the intermediate structure, "inlining" the proof of associativity. This is a bit tedious and obscures the paper proof a bit IMHO, but whatever. Also can't do this today. Maybe Thursday?

Thoughts?

I prefer option 3. I know it is tedious, but it minimises duplication. If you did keep the whole booleanring structure as is, you would still have a lot to explain regarding how this definition compares with Mathlib's and why we don't use it. For syntactic meta-theories the answer is clear, we always want to start with a blank slate with the weakest required equalities and implications. For specific models of the theory, this doesn't apply.

Take your time.

Also @teorth : any thoughts on this?

@codyroux
Copy link
Contributor Author

I take it "That's what Sheffer's paper and https://en.wikipedia.org/wiki/Boolean_algebra_(structure) do" is not a justification? I do agree that calling it a ring was a mistake, and probably the + and * symbols need to be renamed.

@Shreyas4991
Copy link
Collaborator

Have we sorted out the issue of mathlib compatibility?

@pitmonticone
Copy link
Collaborator

Thank you @codyroux and @jjtowery for your contributions!

I have golfed and formatted Sheffer.lean and ShefferAlgebra.lean.

I leave the rest of the review to @Shreyas4991.

@codyroux
Copy link
Contributor Author

Thanks a bunch @pitmonticone! Things are looking nice IMHO, but I'm not sure whether Mathlib has additional criteria I've overlooked.

@jjtowery
Copy link
Contributor

jjtowery commented Nov 12, 2024 •
edited
Loading

Speaking of mathlib compatibility, seems like mathlib decided to replace sup and inf with max and min, so I made a pull request to you @codyroux to fix that.
Other than this, the other 'not-mathlib-compatible' thing would be the theorem naming, but that's only important if we were actually trying to commit to mathlib. Otherwise, with @pitmonticone fixing the formatting, and that I fixed the issue of duplicating the BooleanRing definition, this should be all good now.

@codyroux
Copy link
Contributor Author

Merged, let's see what the CI says.

@Shreyas4991
Copy link
Collaborator

@codyroux : you were planning for some part of this to be PR'ed to mathlib right?

@codyroux
Copy link
Contributor Author

I certainly wasn't originally thinking this, but I guess it'd be nice. I'm looking at the naming conventions right now.

@Shreyas4991
Copy link
Collaborator

@codyroux : I will wait for you to ping me here before reviewing/merging the LR

@codyroux
Copy link
Contributor Author

codyroux commented Dec 8, 2024

I've been on vacation, and sick, haven't forgotten about this but will need a bit more time.

@codyroux
Copy link
Contributor Author

codyroux commented Jan 2, 2025

@Shreyas4991 I'm ready!

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

@Shreyas4991 Shreyas4991 Awaiting requested review from Shreyas4991

Assignees
No one assigned
Labels
awaiting-author Reviewers and maintainers are awaiting the author's response or fixes in response to review comments
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

BOOLEAN: Prove Theorem 5.8 (Sheffer stroke axiom)
8 participants
@codyroux @Shreyas4991 @teorth @jjtowery @pitmonticone @Command-Master @fpvandoorn @vlad902