Stream: coq-community devs & users

Topic: Weak lemmas from regexp-Brzozowski


view this post on Zulip Karl Palmskog (Nov 25 2021 at 12:18):

@Christian Doczkal what do you think of the following quite weak lemmas from regexp-Brzozowski, are they possibly worth adding to reglang? I guess they are mostly just restating the meaning of dot, compl, residual.

Lemma in_dot u : (u \in dot) = (size u == 1).
Proof. by []. Qed.

Lemma in_compl L v : (v \in compl L) = (v \notin L).
Proof. by []. Qed.

Lemma residualE x L u : (u \in residual x L) = (x :: u \in L).
Proof. by []. Qed.

view this post on Zulip Christian Doczkal (Nov 25 2021 at 14:03):

Yes, sure, feel free to add/move them to reglang. I suppose that, like other in_ lemmas in mathcomp, they are mainly useful in their right-to-left direction. For consistency, the last one should probably be named in_residual, right?

view this post on Zulip Karl Palmskog (Nov 25 2021 at 14:05):

Right. OK, then I will do a PR with in_residual and friends.

view this post on Zulip Karl Palmskog (Nov 25 2021 at 15:03):

sigh, the Reglang CI failed due to Alpine Linux network error


Last updated: Feb 05 2023 at 15:03 UTC