[Merged by Bors] - chore: fix some Set defeq abuse, golf#6114
[Merged by Bors] - chore: fix some Set defeq abuse, golf#6114
Set defeq abuse, golf#6114Conversation
|
|
||
| /-- `M.accepts` is the language of `x` such that `M.eval x` is an accept state. -/ | ||
| def accepts : Language α := fun x => M.eval x ∈ M.accept | ||
| def accepts : Language α := {x | M.eval x ∈ M.accept} |
There was a problem hiding this comment.
This is still a defeq abuse because Language and Set are not interchangeable.
leanprover-community/mathlib3#18451 had a path to resolve this, but was more trouble that I cared to deal with.
Having said that, this change is certainly not harmful, so fine to leave it
There was a problem hiding this comment.
They are not interchangeable but Language is defined as Set, not _ → Prop, so this is a step in the right direction. The proper fix would be to introduce Language.mk.
There was a problem hiding this comment.
Set.up is pretty much exactly that function, as SetSemiring has all the same instances as Language.
eric-wieser
left a comment
There was a problem hiding this comment.
I didn't look at the CategoryTheory files but the rest look fine.
|
Thanks! bors merge |
- Use `{x | p x}` instead of `fun x ↦ p x` to define a set here and there.
- Golf some proofs.
- Replace `Con.ker_apply_eq_preimage` with `Con.ker_apply`. The old version used to abuse definitional equality between `Set M` and `M → Prop`.
- Fix `Submonoid.mk*` lemmas to use `⟨_, _⟩`, not `⟨⟨_, _⟩, _⟩`.
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Set defeq abuse, golfSet defeq abuse, golf
- Use `{x | p x}` instead of `fun x ↦ p x` to define a set here and there.
- Golf some proofs.
- Replace `Con.ker_apply_eq_preimage` with `Con.ker_apply`. The old version used to abuse definitional equality between `Set M` and `M → Prop`.
- Fix `Submonoid.mk*` lemmas to use `⟨_, _⟩`, not `⟨⟨_, _⟩, _⟩`.
{x | p x}instead offun x ↦ p xto define a set here and there.Con.ker_apply_eq_preimagewithCon.ker_apply. The old version used to abuse definitional equality betweenSet MandM → Prop.Submonoid.mk*lemmas to use⟨_, _⟩, not⟨⟨_, _⟩, _⟩.I found these while trying to make
Seta one-field structure. While I'm not sure that I'll complete that other refactor, these changes seem good to me in any case.