Stream: Coq users

Topic: How to compute with rational numbers?


view this post on Zulip Ignat Insarov (Jun 17 2021 at 15:04):

I want to use Coq.QArith to compute something. Here is my code: <https://gist.github.com/kindaro/92a7d53a4c9a4297417310dcf0a599b7>. I cannot destruct or eliminate the proof of existence of the number I want to have computed. What do?

view this post on Zulip Gaëtan Gilbert (Jun 17 2021 at 15:06):

use { (x: ℚ) | e₂ = Root 2 x} instead of ∃ (x: ℚ), e₂ = Root 2 x

view this post on Zulip Ignat Insarov (Jun 17 2021 at 15:08):

It works, thanks! Why does one work but not the other?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2021 at 15:16):

https://coq.inria.fr/doc/language/core/inductive.html#the-match-with-end-construction

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2021 at 15:16):

in particular the paragraph about Prop


Last updated: Jan 29 2023 at 06:02 UTC