feat: product of FLTS

[fmontesi]

This PR introduces the product of two FLTS and refactors DA.prod to use that definition and its theorems (currently only one).

[ctchou]

I think the following expression is prettier:

def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
  toFLTS := da1.toFLTS.prod da2.toFLTS
  start := (da1.start, da2.start)

Also, could you restore the API DA.prod_mtr_eq by instantiating LTS.prod_mtr_eq? It is better that proofs at the Language-level can appeal only to theorems in Automata, rather than going all the way to FLTS or LTS.

[chenson2018]

Yes, it is stylistically preferable to use where. The only common exception is when there is a single constructor and you can write := ⟨...⟩. I don't think with for a single constructor justifies a deviation either.

[fmontesi]

I agree in normal cases, but when it's about extending a construction defined above in the structure hierarchy (as in this case), I find the with-style very clear: it's 'whatever prod for flts does, plus this extra bit'.

I struggle to read and understand the toFLTS field in the where-style at a glance, because I have to think about the implementation detail of how lean deals with structure extension. Do you find it intuitive?

[fmontesi]

I agree in normal cases, but when it's about extending a construction defined above in the structure hierarchy (as in this case), I find the with-style very clear: it's 'whatever prod for flts does, plus this extra bit'.

I struggle to read and understand the toFLTS field in the where-style at a glance, because I have to think about the implementation detail of how lean deals with structure extension. Do you find it intuitive?

[ctchou]

Well, I personally find the where syntax more intuitive, exactly because it lists the fields as they appear in the definition of the structure. Here the toFLTS follows directly from the fact that DA is an extension of FLTS. I was actually surprised that the with syntax works here. The examples in:

https://lean-lang.org/theorem_proving_in_lean4/Structures-and-Records/#objects

gave me the impression that with is used to modify the value of a field in the structure on the LHS of the with. But here the LHS of with is an FLTS which doesn't even have a start field.

An alternative here is to use DA.mk or even ⟨ ...⟩, since we have only two fields and their types are clear from their expressions.

[chenson2018]

I do find the where much easier to read intuitively versus the elaboration for with using structures of different types. If this were modifying a structure with a same type, I would agree that it is clearer to use a record update syntax.

[fmontesi]

Thanks for the comments. I yield and will convert. :-) It does look a bit more palatable after your comments.

[ctchou]

I have the impression that we should now be using ↦ instead of => in this case, but I'm not entirely sure about that.

[chenson2018]

I remembered vaguely there was a Zulip thread on this topic, then realized it was you who asked this question last year!

There's a split of opinions, and I don't have a strong opinion either way. I'd say author discretion.

[fmontesi]

I remember a linter giving me trouble with ↦ in the past, but if it's ok now I'm fine with either. Also, => is what's used outside of mathlib.

But if you both like ↦, I wouldn't be against adopting it as cslib convention. I think => is suboptimal as ASCII for 'maps to' anyway, since it looks more like the logical implication symbol.

[chenson2018]

Yes, it is stylistically preferable to use where. The only common exception is when there is a single constructor and you can write := ⟨...⟩. I don't think with for a single constructor justifies a deviation either.

[fmontesi]

Comments integrated.

[chenson2018]

LGTM, thanks! I think this will be the first PR where testing runs in the merge queue.