Stream: math-comp analysis

Topic: lra

view this post on Zulip Bas Spitters (Jul 14 2020 at 15:10):

How well is lia supported in math-comp analysis? Should one expect the same support as for the stdlib?

view this post on Zulip Karl Palmskog (Jul 14 2020 at 15:37):

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

view this post on Zulip Bas Spitters (Jul 14 2020 at 15:52):

There do not seem to be any reals in there:
https://github.com/pi8027/mczify/blob/master/theories/zify.v

view this post on Zulip Karl Palmskog (Jul 14 2020 at 16:12):

well, lia doesn't handle reals anyway, so you may want to change topic...

view this post on Zulip Michael Soegtrop (Jul 14 2020 at 16:57):

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.

view this post on Zulip Michael Soegtrop (Jul 14 2020 at 16:58):

The original reason for having zify was afaik to be able to handle goals in nat, but it was considerably extended since then.

view this post on Zulip Bas Spitters (Jul 14 2020 at 19:33):

@Karl Palmskog Apologies, yes, I meant lra.

view this post on Zulip Karl Palmskog (Jul 14 2020 at 20:04):

this [lra in MathComp] might be a good question for Frederic Besson, but I think he is best reached by email

view this post on Zulip Bas Spitters (Jul 14 2020 at 20:36):

@Frédéric Besson ?

view this post on Zulip Karl Palmskog (Jul 14 2020 at 20:49):

right

view this post on Zulip Kazuhiko Sakaguchi (Jul 14 2020 at 21:05):

coq/coq#10982 is needed to use lra and nra for the rational/real operators in MathComp.

view this post on Zulip Kazuhiko Sakaguchi (Jul 14 2020 at 21:08):

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.)

view this post on Zulip Bas Spitters (Jul 14 2020 at 21:14):

That apparently depends on a change in the interface of:
https://github.com/pi8027/mczify

view this post on Zulip Kazuhiko Sakaguchi (Jul 14 2020 at 21:44):

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

Last updated: Oct 13 2024 at 01:02 UTC