feat: define BuchiCongruence and prove that it is a right congruence of finite index

[ctchou]

This PR defines the notion of a "right congruence", which is an equivalence relation between finite words that is preserved by concatenation on the right, and proves its basic properties:

• There is a natural deterministic automaton corresponding to each right congruence whose states are the equivalence classes of the congruence and whose transitions correspond to concatenation on the right of the input symbols.
• If a right congruence is of finite index, then each of its equivalence classes is a regular language.

Furthermore, this PR also defines a special type of right congruences introduced by J.R. Buchi to and proves that it is of finite index if the underlying Buchi automaton is finite-state. The purpose of Buchi congruence is to prove the closure of ω-regular languages under complementation. But more work will be needed before we reach that goal.

This PR depends on #249. The old PR #265 has been absorbed into this PR.

[ctchou]

Rebase on the current upstream/main.

[chenson2018]

Please take a look at the first commit that I just pushed. (This took me quite a while to think over, so please consider the differences carefully)

I used the following definition:

class RightCongruence (α : Type*) extends
  eq : Setoid (List α) , CovariantClass _ _ (fun x y => y ++ x) eq where

so there is no confusion about notation referring to the existing setoid instance for lists, and all of your proofs are the same with the exception of some arguments changing order.

I also made some changes related to where you were passing RightCongruence as an explicit paramater versus a typeclass paramater. A nice side effect is that using RightCongruence.eqvCls is a bit more succinct. Personally, I would prefer to do away with RightCongruence.QuotType and just write Quotient explicitly, but I am fine leaving it in this form where it is an abbrev used to infer the setoid when possible.

Lastly I removed the HasEquiv notation, which I don't think was doing what you intended, as this was on the setoid itself. I don't see anywhere this was used, but please clarify if you think this is still needed.

[ctchou]

@chenson2018 Your changes look good to me. I made one further change: I gave a name right_cov to the CovariantClass field of RightCongruence. One can imagine defining a LeftCongruence with a left_cov field and a (two-sided) Congruence with both left_cov and right_cov fields in the future.

Also, I will close #265 and merge it into this PR, because the changes you made impact both PR's.

[chenson2018]

This looks like a good change. Sorry about pushing changes here, but it was just too hard to see how different definitions worked out otherwise. I will review the rest of this PR once Fabrizio merges #249.