Skip to content

[Merged by Bors] - fix(ModelTheory): make some defs into abbrevs#6171

Closed
ChrisHughes24 wants to merge 1 commit intomasterfrom
ModelTheory-def-abbrev
Closed

[Merged by Bors] - fix(ModelTheory): make some defs into abbrevs#6171
ChrisHughes24 wants to merge 1 commit intomasterfrom
ModelTheory-def-abbrev

Conversation

@ChrisHughes24
Copy link
Copy Markdown
Member

@ChrisHughes24 ChrisHughes24 commented Jul 27, 2023 •
edited
Loading

Formula is currently an abbreviation for BoundedFormula. There were some definitions like not which were defined on both BoundedFormula and Formula, and I have made the Formula versions into abbrev so there is no need to duplicate simp lemmas.

A concrete advantage of this PR is that the following lemma is proved by simp with the lemma Formula.realize_not where it wasn't before.

example (φ : L.Formula α) (v : α → M) :
    Formula.Realize (∼ φ) v ↔ ¬φ.Realize v := by
  simp

Open in Gitpod

@ADedecker
Copy link
Copy Markdown
Member

ADedecker commented Aug 2, 2023

Is there a reason not to delete the simp lemmas that you are talking about in this PR? E.g FirstOrder.Language.Formula.realize_not if I understand correctly?

Otherwise LGTM

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Aug 2, 2023

✌️ ChrisHughes24 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Aug 2, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Aug 2, 2023

The issue is that the simp lemmas didn't trigger because there were two definitions of not on Formula, both BoundedFormula.not and Formula.not, which are equal, and since Formula is reducible it's easy to end up with the wrong one. So the lemmas stand, but I did make a mistake in my description and I should have written Formula.realize_not instead of Sentence.realize_not

@ChrisHughes24
Copy link
Copy Markdown
Member Author

ChrisHughes24 commented Aug 2, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 2, 2023
@ADedecker
Copy link
Copy Markdown
Member

ADedecker commented Aug 2, 2023

Ah right I understand now. Thanks!

bors bot pushed a commit that referenced this pull request Aug 2, 2023
@ChrisHughes24
fix(ModelTheory): make some defs into abbrevs (#6171)
56d44fc
@bors
Copy link
Copy Markdown

bors bot commented Aug 2, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title fix(ModelTheory): make some defs into abbrevs [Merged by Bors] - fix(ModelTheory): make some defs into abbrevs Aug 2, 2023
@bors bors bot closed this Aug 2, 2023
@bors bors bot deleted the ModelTheory-def-abbrev branch August 2, 2023 16:24
kim-em pushed a commit that referenced this pull request Aug 3, 2023
@ChrisHughes24 @kim-em
fix(ModelTheory): make some defs into abbrevs (#6171)
283325a
kim-em pushed a commit that referenced this pull request Aug 3, 2023
@ChrisHughes24 @kim-em
fix(ModelTheory): make some defs into abbrevs (#6171)
434544d
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@ChrisHughes24 @kim-em
fix(ModelTheory): make some defs into abbrevs (#6171)
fc06746
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@ChrisHughes24 @ADedecker