How well is lia supported in math-comp analysis? Should one expect the same support as for the stdlib?
hmm, I think you need https://github.com/pi8027/mczify? Shouldn't it be the same as for any other MathComp use? Maybe mczify needs additional extension for dealing with reals via
There do not seem to be any reals in there:
lia doesn't handle reals anyway, so you may want to change topic...
mczify is for integer arithmetic only - it converts goals in various integer types (say nat) with various definitions of relational operators to a goal in Z, which lia can solve. Afaik something similar for lra does not exist.
The original reason for having zify was afaik to be able to handle goals in nat, but it was considerably extended since then.
@Karl Palmskog Apologies, yes, I meant lra.
this [lra in MathComp] might be a good question for Frederic Besson, but I think he is best reached by email
@Frédéric Besson ?
coq/coq#10982 is needed to use
nra for the rational/real operators in MathComp.
Since Farkas' lemma holds for any totally ordered field (
realFieldType in MathComp), should
lra be also applicable for any
realFieldType? (Theoretically speaking, I guess so.)
That apparently depends on a change in the interface of:
Yes. But without appropriate support on the zify (rify?) side, it is not doable.
Last updated: Feb 05 2023 at 08:28 UTC