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 support for explicitly Finite non-implications #702

Merged
merged 1 commit into from
Oct 21, 2024

Conversation

vlad902
Copy link
Contributor

@vlad902 vlad902 commented Oct 21, 2024

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

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
@teorth
Copy link
Owner

teorth commented Oct 21, 2024

Am merging this for now but one should do some further checks once more implications are converted to Finite to see if anything breaks.

@teorth teorth merged commit c03f75d into teorth:main Oct 21, 2024
1 check passed
codyroux pushed a commit to codyroux/equational_theories that referenced this pull request Oct 21, 2024
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
teorth pushed a commit that referenced this pull request Oct 25, 2024
#702 added support for Finite non-implications, this add support for
Finite implications as well. I update the extract_implications script to
always default to 'non-finite' results, and I've verified that the
outputs of `lake exe extract_implications` outputs for every subcommand
match what they were prior to this change, despite marking a number of
Finite results with `@[equational_result]` in this change [modulo the
two non-finite theorems I added the attribute to as well.]

Note that reviewing by commit might be slightly easier, as the first and
last commits are a trivial update and a simple refactor.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants