search

katydid / regex-derivatives-coq

Apache License 2.0
21 stars 7 forks source link

a template to create an or_lang semi ring #157

Closed awalterschulze closed 3 years ago

awalterschulze commented 3 years ago

Review, but DO NOT MERGE This requires https://github.com/awalterschulze/regex-reexamined-coq/pull/156 to merge this. Let me worry about doing it in the right order.

This creates a template for an or_lang semi ring. It is not as powerful as a orb semi ring, probably because I can't think how we would be able to prove decidable forall b1 b2:lang, lang_eq b1 b2 = true -> b1 = b2. But otherwise it helps for some proofs.

When everything is uncommented and the proofs are admitted, the semi ring does help to prove the proofs that have tactics that are commented.

awalterschulze commented 3 years ago

Discussed offline: merging now and will post review