Stream: Constructive reals & analysis

Topic: Integers in reals


view this post on Zulip Bas Spitters (Aug 17 2020 at 11:33):

There is a theory for rationals within the reals. Is there a similar theory and hints database for the integers?
https://coq.inria.fr/library/Coq.QArith.Qreals.html
@Vincent Semeria ?

view this post on Zulip Bas Spitters (Aug 17 2020 at 11:49):

Found it, but the rewrite database seems to be absent:
https://github.com/coq/coq/blob/master/theories/Reals/RIneq.v

view this post on Zulip Vincent Semeria (Aug 17 2020 at 11:55):

I have never used hints or proof automation. What do you want to do with those theorems in RIneq ?

view this post on Zulip Bas Spitters (Aug 17 2020 at 12:19):

In general, to write proofs in Coq with the convenient of proving theorems on paper.


Last updated: Feb 06 2023 at 07:03 UTC