Stream: math-comp analysis

Topic: Recommended way to use MC+reals?

view this post on Zulip Karl Palmskog (Aug 17 2020 at 20:17):

So is the recommended way to use reals with MathComp to require-import reals from Analysis and do:

Variable R : realType.

or directly use R type from stdlib? or something else?

view this post on Zulip Reynald Affeldt (Aug 18 2020 at 01:02):

In Rstruct.v, R is endowed with a realType structure.

view this post on Zulip Reynald Affeldt (Aug 18 2020 at 01:02):

So realType lemmas should be usable with R.

view this post on Zulip Karl Palmskog (Aug 18 2020 at 08:33):

indeed both approaches (R-from-stdlib-with-realType vs abstract-realType) are possible/feasible, but what are the tradeoffs? For example, with reals/realType, isn't it easier to use the bool comparison operators?

view this post on Zulip Reynald Affeldt (Aug 18 2020 at 12:26):

in both cases bool comparison operators are available I think; tradeoffs may depend on your application: thanks to the hierarchy below realType you can state lemmas with the right abstract type but you might also lose field/lra tactics on the other hand (as of today)

Last updated: Aug 19 2022 at 20:03 UTC