Stream: math-comp analysis

Topic: Proving inequalities about R

view this post on Zulip Théo Winterhalter (Feb 18 2021 at 13:39):

Hi everyone,
This is a pretty naive question and you might have had it several times already. Are there facilities to help prove inequalities on mathcomp-analysis reals? It seems lra doesn't apply and I guess it's to be expected.
Thanks. :)

view this post on Zulip Marie Kerjean (Feb 18 2021 at 14:59):

This could be relevant to mathcomp and the whole order.v file, as mathcomp-analysis reals are just instances of mathcomp types. The file was implemented by @Kazuhiko Sakaguchi I think, you might have more answers by going in the mathcomp users thread.

view this post on Zulip Kazuhiko Sakaguchi (Feb 18 2021 at 15:05):

For ssrnat and ssrint, mczify does the job. But reals are not supported for now. https://github.com/math-comp/mczify

view this post on Zulip Bas Spitters (Feb 18 2021 at 15:07):

There is the work by Russell and Cezary on computing with classical reals which should be possible to get to work with math-comp too.
https://jfr.unibo.it/article/download/1411/932/2827
It may require some work though. Coq_interval may be helpful too.

view this post on Zulip Théo Winterhalter (Feb 18 2021 at 15:09):

Ok, I'll keep doing things by hand then. Thanks. :blush:

view this post on Zulip Marie Kerjean (Feb 18 2021 at 15:11):

Théo Winterhalter said:

Ok, I'll keep doing things by hand then. Thanks. :blush:

Good luck !

view this post on Zulip Kazuhiko Sakaguchi (Feb 18 2021 at 15:29):

@Théo Winterhalter Another thing you can do for now is showing your interest in this PR. https://github.com/coq/coq/pull/10982

view this post on Zulip Kazuhiko Sakaguchi (Feb 18 2021 at 15:32):

However, this preprocessing mechanism cannot be applied to the abstract interfaces for (real) numbers such as realType anyway. It works only for concrete ones.

view this post on Zulip Théo Winterhalter (Feb 18 2021 at 15:36):

Kazuhiko Sakaguchi said:

Théo Winterhalter Another thing you can do for now is showing your interest in this PR. https://github.com/coq/coq/pull/10982

By reacting with :+1: ?

view this post on Zulip Kazuhiko Sakaguchi (Feb 18 2021 at 15:38):

@Théo Winterhalter Or you may comment if you want. :smile:

view this post on Zulip Théo Winterhalter (Feb 18 2021 at 15:50):

Kazuhiko Sakaguchi said:

Théo Winterhalter Or you may comment if you want. :smile:

Wouldn't that add noise? If you still think I should I don't mind writing "Thanks for doing this!" or something like this. :smile:

Last updated: Sep 26 2023 at 12:02 UTC