add definition and result about regexp derivatives

[palmskog]

Derivation is in my view a basic operation on regular expressions and should be included in the library. Here is a port of the basic definitions and results from regexp-Brzozowski. To avoid the (cons-based) residual definition from language.v being shadowed, I rename the cat-based residual definition in dfa.v to residual_cat.

[chdoc]

The naming collision is indeed unfortunate. However, I don't think that cat is the right is the right disambiguation here. If I understand correctly, the two definitions differ along two axes: one is whether they take the residual with respect to a character or a word, the other is that residual applies to decidable languages only.

[palmskog]

@chdoc sure, there are two different differences. But what do you suggest instead of residual_cat then? I'd be fine with residual_lang (as opposed to dlang) or residual_lang_cat.

[chdoc]

@chdoc sure, there are two different differences. But what do you suggest instead of residual_cat then? I'd be fine with residual_lang (as opposed to dlang) or residual_lang_cat.

I don't think there's any really great option, but I would prefer residual_lang over residual_cat.

[palmskog]

@chdoc renaming done - so OK to merge now?

The CI issues are due to some issues with the Nix Toolbox, I disabled the failing configuration here, but CI will only stop failing when this PR is merged.