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 `lra`

, though

There do not seem to be any reals in there:

https://github.com/pi8027/mczify/blob/master/theories/zify.v

well, `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 ?

right

coq/coq#10982 is needed to use `lra`

and `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:

https://github.com/pi8027/mczify

Yes. But without appropriate support on the zify (rify?) side, it is not doable.

Last updated: Sep 28 2023 at 11:01 UTC