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

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.

For `ssrnat`

and `ssrint`

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

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.

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

Théo Winterhalter said:

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

Good luck !

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

However, this preprocessing mechanism cannot be applied to the abstract interfaces for (real) numbers such as `realType`

anyway. It works only for concrete ones.

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: ?

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

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: Feb 05 2023 at 07:03 UTC