[Merged by Bors] - chore: fix some Set defeq abuse, golf
#6114
Conversation
| @@ -92,7 +92,7 @@ theorem evalFrom_of_append (start : σ) (x y : List α) : | |||
| #align DFA.eval_from_of_append DFA.evalFrom_of_append | |||
|
|
|||
| /-- `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/mathlib#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.
|
Thanks! bors merge |
github-actions
bot
added
ready-to-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. |
bors
bot
changed the title
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.