feat: prove that regular languages are closed under concatenation

[ctchou]

In this patch we prove that regular languages are closed under concatenation, by leveraging the results already proved about the infinite executions of the automata concatenation construction in NA/Concat.lean. In order to do so, we introduce the notion of a "total LTS", which means that the LTS has a next state for any given starting state and label, and a "LTS.totalize" construction that converts any LTS into a total LTS by adding a sink state and transitions from all states to the sink state. Then the notion of "total" and the "totalize" construction are generalized to NA. By "totalizing" NA's, we can extend any finite execution of a NA into an infinite execution and thus re-use the results already proved for infinite executions.

The same technique can be applied to NA/Loop.lean to prove that regular languages are closed under the Kleene star; see PR #241.

[chenson2018]

I'm going to leave review of LTS to Fabrizio, but I've left a few comments.

[chenson2018]

My comments have been addressed, but still leaving LTS to be reviewed.

[fmontesi]

There's a class LTS.LeftTotal in LTS/Basic.lean that I wrote for this kind of stuff, so I'd like to discuss the design choice of adding LTS.Total. One important difference is that I've used an existential:

class LTS.LeftTotal (lts : LTS State Label) where
  left_total : ∀ s μ, ∃ s', lts.Tr s μ s'

So I guess this would make some of the constructions noncomputable -- by contrast, LTS.Total is a witness from which we can build things! In particular, can't we noncomputably get the next function just from knowing that an LTS is LeftTotal?

Is there an example from mathlib we can refer to for this discussion maybe?

It might make sense to have both LeftTotal and Total. However, I'd probably change the name of the latter, since in mathlib people seem to stick to left total for this kind of things. I don't have a good proposal yet.

[chenson2018]

To clarify, you are wondering if these are valuable to both have around? You can write:

instance (lt : LTS.Total lts) :  LTS.LeftTotal lts where
  left_total s μ := ⟨lt.next s μ, lt.total s μ⟩

noncomputable def LTS.leftTotal_total [inst : LTS.LeftTotal lts] : LTS.Total lts where
  next s μ := Classical.choose (inst.left_total s μ)
  total s μ :=  Classical.choose_spec (inst.left_total s μ)

So if you don't care about the computability aspect, it seems they can be consolidated.

[ctchou]

I completely missed "LTS.LeftTotal". Sorry! (By the way, shouldn't it be "RightTotal"?). Anyway, I chose the name "total" by following the standard notion of a relation or function being "total" or "partial": https://en.wikipedia.org/wiki/Total_relation.

Actually I started with using an existential quantifier as in LTS.LeftTotal. But then the need to define LTS.makeωTr and prove LTS.Total.ωTr_exists made me realize that an explicit witness is much easier to work with. Furthermore, when we do an actual proof of existence (such as finConcat_total in NA/Concat.lean), we will typically present an explicit witnesses anyway. This is analogous to assuming a type to be Inhabited vs assuming it to be Nonempty. The former is easier to use, because it provides an explicit witness, and the typical proof of a type being nonempty is to present a witness.

[fmontesi]

@ctchou Heh, funny thing: I had originally called it total too, but in mathlib they follow the 'left total' terminology. (Which makes sense, because you can also be concerned about right totality in general.)

@chenson2018 I expect them both to be useful, exactly because of what @ctchou wrote. I'm just wondering what we should call them, because having LeftTotal for the 'declarative' version and Total for the 'constructive' version is really confusing naming. Hence my wondering of whether there's a similar case in mathlib, to see if we can get some inspiration.

Just to give an example without caring too much about elegant names, the current Total could be called ProofOfLeftTotal (blergh!) or LeftTotalWitness. I hope we can come up with something better...? :-)

An observation: Total is basically equivalent to having an FLTS flts and showing that flts.toLTS.Tr is a sub-relation of lts.Tr. For any FLTS, .toLTS.Tr is always LeftTotal, so left-totality follows. I'm not sure if this observation is already useful, just wanted to point it out. Might lead to some theorems.

[ctchou]

I find mathlib's use of "left" and "right" regarding relations is really unfortunate, because in the "constructive" versions of those notions the witness is for the opposite side. Here's my proposal:

• We rename LTS.LeftTotal to LTS.Total and turn it into a Prop. "Total" is a completely standard terminology in this context.
• We provide LTS.chooseFLTS using Classical.choose and prove what is now LTS.Total.total. The rest of my code will be changed to use LTS.chooseFLTS.
• We will not have LTS.RightTotal, but we can define LTS.reverse to reverse an LTS. This can come in handy in, for example, formalizing Brzozowski's algorithm: https://en.wikipedia.org/wiki/DFA_minimization#Brzozowski's_algorithm

How do you think about the above?

[fmontesi]

I like it, modulo the fact that I'd keep totality a class instead of turning it into a Prop, since that's our current practice for similar properties. Or do you have a place where having it as a class is particularly inconvenient?

Full reasoning on terminology, etc., below -- some nuances might be important now or later.

In the context of relations, they made the most reasonable/immediate choice: it's pretty standard terminology for relations, otherwise there's no established way to name all interesting classes. When one can commit to being interested only in left-totality, saying 'total' is perfectly fine because that's the default meaning, but that's not good in general.
See p. 3 of https://homepages.hass.rpi.edu/heuveb/Teaching/Logic/CompLogic/Web/Handouts/SetsRelationsFunctions.pdf and https://en.wikipedia.org/wiki/Total_relation#:~:text=For%20relations%20R%20where%20x,that%20relation%20to%20something%20else.%22

However, in this discussion, we can consider also the glossary of transition systems. In this context, people are typically only interested in:

• Left totality. What we're discussing here. We could just call it 'total' (the standard default) or 'complete' (inspired by what people typically say in automata theory for 'complete' transition function). I'm ok with either.
• Right uniqueness. In LTS land, this is definitely called 'deterministic LTS'. In fact, I've already called it as such in LTS.Deterministic.

So we can either:

1. If you're ok with keeping LTS.Deterministic to talk also about automata -- so you'd get that a 'Deterministic' NA means that it's right-unique, which is sometimes what people mean but not always because some works use it to mean that there's a corresponding complete DA iirc -- then I think it's ok to rename LeftTotal to Total (or Complete, if you prefer it? do they say the same in graphs?).
2. Otherwise, if we risk having confusion, I'd keep LeftTotal and rename Deterministic to RightUnique.

Assuming (1) is ok (my preference), I'd suggest that we rename LeftTotal to Total, but keeping it as a class, and then:

-- In LTS/Basic.lean
noncomputable def LTS.chooseFLTS [inst : LTS.Total lts] : FLTS State Label [...]

theorem LTS.chooseFLTS_tr [LTS.Total lts] (s : State) (μ : Label) : lts.Tr s μ (lts.chooseFLTS s μ) := [...]

-- In FLTS/FLTSToLTS.lean.
instance (flts : FLTS State Label) : LTS.Total (flts.toLTS) where [...]

[ctchou]

Let's stick with the names Total and Deterministic. I'll update my code and have you review it.