Looking for code style review

Stream: new members

[Igor Shimanogov]

Hi! I got interested in Lean recently and decided to practice formalizing Schützenberger theorem, since formal language theory is in scarce in mathlib. Currently, having fun working towards it, but here are my concerns:

1. Is it even a good idea to contribute it to mathlib if I succeed at proving?
2. Is it okay to ask here for a quick code reviews? I want it to be as idiomatic as possible, and I feel myself always misnaming various things :)

[Daniel Weber]

Welcome! Contributing it to Mathlib would be great, and feel free to ask here for code review

[Igor Shimanogov]

So, I started with defining syntactic monoid of a language:
https://gist.github.com/MrSumato/a2d726198d67d26e1fee4264e85f5793

Is there anything incorrect about this code? Any comments on improvements? Also, it seems kinda strange that there is no anything like setOf_eq_iff in mathlib.

[Kyle Miller]

That's docs#Set.ext_iff

theorem setOf_eq_iff  {p q: α → Prop} : {x : α | p x} = {x : α | q x} ↔ (∀x, p x ↔ q x) :=
  Set.ext_iff

though I'm slightly misusing definitions. This is better:

theorem setOf_eq_iff  {p q: α → Prop} : {x : α | p x} = {x : α | q x} ↔ (∀x, p x ↔ q x) := by
  simp [Set.ext_iff]

The simp? tactic shows it's finishing it off by rewriting with docs#Set.mem_setOf_eq

[Igor Shimanogov]

Oh, thx, I see! Fixed it in the gist. What about remaining part? Are namings correct?

[Daniel Weber]

This is mostly stylistic, but syn_eq_is_eq can be shortened to

instance syn_eq_is_eq : Equivalence (SynEquiv L) where
  refl _ := rfl
  symm h := h.symm
  trans h1 h2 := h1.trans h2

something like equivalence_synEquiv might be a more descriptive name (or, as it's an instance, you could also forgo giving it any name)