Stack Overflow
Stack Overflow

Questions tagged [real-number]

40 questions
13
votes
2 answers

Why are the real numbers axiomatized in Coq?

I was wondering whether Coq defined the real numbers as Cauchy sequences or Dedekind cuts, so I checked Coq.Reals.Raxioms and... none of these two. The real numbers are axiomatized, along with their operations (as Parameters and Axioms). Why is it…
V. Semeria
  • 3,128
  • 1
  • 10
  • 25
9
votes
2 answers

Real numbers in Coq

In https://www.cs.umd.edu/~rrand/vqc/Real.html#lab1 one can read: Coq's standard library takes a very different approach to the real numbers: An axiomatic approach. and one can find the following axiom: Axiom completeness : ∀E:R → Prop, …
Bruno
  • 95
  • 3
8
votes
2 answers

Delphi - how do you format a real number with leading zeros?

I need to format a real number with leading zeros in the whole number part prior to the decimal point. I know how to achieve this with integers, but the syntax for reals escapes me. Number := 1.234 ; SNumber := Format ('%2.3f', [Number]) ; This…
rossmcm
  • 5,493
  • 10
  • 55
  • 118
7
votes
1 answer

Floating Point Monotonic Property

I was reading a book (CSAPP) . In the book it is written that- floating point addition satisfies the following monotonicity property : if a>=b then (x + a) >= (x+b) for any value a,b and x other than NaN. This property of real (and integer)…
Danish Ahmed
  • 81
  • 2
7
votes
5 answers

What is the Regex for decimal numbers in Java?

I am not quite sure of what is the correct regex for the period in Java. Here are some of my attempts. Sadly, they all meant any character. String regex = "[0-9]*[.]?[0-9]*"; String regex = "[0-9]*['.']?[0-9]*"; String regex =…
Gian Alix
  • 79
  • 1
  • 1
  • 3
7
votes
2 answers

How is "less than" defined for real numbers in Coq?

I am just wondering how is the "less than" relationship defined for real numbers. I understand that for natural numbers (nat), < can be defined recursively in terms of one number being the (1+) successor S of another number. I heard that many things…
thor
  • 21,418
  • 31
  • 87
  • 173
5
votes
2 answers

Recovering implicit information from existentials in Coq

Suppose we have something like this: Suppose x is a real number. Show that if there is a real number y such that (y + 1) / (y - 2) = x, then x <> 1". If one formulates it in an obvious way: forall x : R, (exists y, ((y + 1) * / (y - 2)) = x) -> x <>…
JozkoJezko
  • 51
  • 2
5
votes
1 answer

How to auto prove simple inequality of real numbers in Coq?

Is there a way to automatically prove simple inequalities like 1/2 >= 0?, i.e. Require Export Coq.Reals.RIneq. Local Open Scope Z_scope. Local Open Scope R_scope. Example test: /2 >= 0. I haven't much experience with ring or field, and I am having…
thor
  • 21,418
  • 31
  • 87
  • 173
4
votes
0 answers

"Implicit" definition of the limit of a function in Coq

In Coq, we can formalize the concept of the limit of a function defined on R by defining a function lim of type (R -> R) -> R -> R -> Prop as follows: Require Import Coq.Reals.Reals. Open Scope R. Definition lim (f : R -> R) (c : R) (L : R) := …
Ben
  • 470
  • 1
  • 6
  • 18
4
votes
1 answer

Coquelicot library for basic undergraduate calculus

I have installed Coquelicot on top of mathcomp/SSreflect. I want to perform very basic real analysis with it even if I still do not master standard Coq. This is my first lemma : Definition fsquare (x : R) : R := x ^ 2. Lemma deriv_x2 : forall y,…
FZed
  • 520
  • 3
  • 10
3
votes
2 answers

How can I select only the real numbers from an array? (Python 3)

I want to find the vertical asymptote for: f=(3x^3 + 17x^2 + 6x + 1)/(2x^3 - x + 3) So I want to find the roots for (2x^3 - x + 3) so I wrote: import sympy as sy x = sy.Symbol('x', real=True) asym1 = sy.solve(2*x**3-x+3,x) for i in…
Shervin Rad
  • 460
  • 9
  • 21
3
votes
1 answer

Coq Reals and Ssreflect GRings

I'd like to use ssreflect's lemmas on the Reals defined in Coq.Reals.Raxioms. How do I do that? For example, I'd like to be able to use the add, mul, etc. operations defined for ssralg.GRing.Ring directly on variables of type Rdefintions.R and apply…
larsr
  • 5,447
  • 19
  • 38
3
votes
4 answers

checking if python object can be interpreted as real number [python]

I wrote the function in python: def is_number_like(x): try: int(x) + 1 except: return False return True is there any difference if I write float(x) or int(x)? Or could + 1 part be useful in some case? EDIT:…
Śmigło
  • 937
  • 8
  • 14
3
votes
1 answer

Stronger completeness axiom for real numbers in Coq

Here is the completeness axiom defined in the Coq standard library. Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m. Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m. Definition is_lub (E:R -> Prop)…
davik
  • 675
  • 5
  • 12
3
votes
1 answer

How do you translate the fractional part of a short real number as returned by the 8087 co-processor?

I've written a simple program that loads pi into the top of the register stack in the 8087, then it returns that constant into a short real memory variable. FLDPI ;load pi FSTP DWORD PTR shortReal ;store pi in memory, then pop…
bad
  • 939
  • 6
  • 18
1
2 3