@Christian Doczkal what are your thoughts on this being merged: https://github.com/coq-community/reglang/compare/shepherdson-zify
This removes use of omega in favor of
zify. However, this can currently only be done in a way that supports either:
The branch takes the first option, but the diff needed for the second is quite simple.
Hmm, my thought would be to wait for Coq-8.13 which should (fingers crossed) include a variant of
lia that can deal natively with boolean relations. See Issue #14, which I created a mere 7h ago :laughter_tears:
well, I had the branch lying around since February, and also 8.13 might be a 6-9 months away.
Yes, but I also don't see a reason to rush to remove omega, in particular if it requires adding a new file (
zify.v) that's a trimmed down version of a file from mathcomp if I understand correctly. What's your rationale for this?
it doesn't live in MathComp currently, but here: https://github.com/pi8027/mczify --- it's trimmed down because I don't want it to depend on mathcomp-algebra, etc.
in any case, this was an experiment mainly to investigate whether I could easily switch to just
lia everywhere in my projects, so not a big deal for me to wait for 8.13 w.r.t. RegLang.
also, I think
scrush from CoqHammer (seemingly current top dog of Coq FOL-oriented automation) could now work quite well in MC projects via
zify in this way
Last updated: Jun 06 2023 at 23:01 UTC