Are Dafny "reals" really "real"

Question

I want to prove statements about derivatives and limits, but I failed to make progress, so I wondered whether Dafny's real type actually coincides with the real numbers.

Dafny's documentation states:

Dafny supports numeric types of two kinds, integer-based, which includes the basic type int of all integers, and real-based, which includes the basic type real of all real numbers

So I assume that I can prove all statements about (values of type) real that I could prove about real numbers.

As far as I understand, Dafny itself doesn't specify the axioms of real numbers. It transpiles to boogie, which in turn relies on SMT solvers, usually z3. z3 points to SMT-Lib's Reals theory, which states "real closed field" axioms, which I hope are the basis of z3 and thereby boogie and Dafny reals.

Based on these I tried

lemma all_positive_elements_have_a_square_root(x: real)
  requires x >= 0.0
  ensures exists root: real :: x == root * root
{}

But it fails to verify. I won't put in more effort, because - not knowing the axioms - I don't know how to help the verifier.

I tried to convince myself that z3 reals fare better:

$ cat /tmp/reals.z3 
(declare-const x Real)
(assert (= (* x x) 2.0))
(check-sat)
(get-model)
$ z3 /tmp/reals.z3 
sat
(
  (define-fun x () Real
    (root-obj (+ (^ x 2) (- 2)) 1))
)

What is `root-object` in z3 with Real theory? explains the meaning of this output and it indeed shows that z3 can prove the existence of a real number with the desired property, which does not follow from ordered field axioms alone.

Dafny, again, fails to verify this:

lemma sqrt2_exists()
  ensures exists root: real :: 2.0 == root * root
{}

So is there a way to make use of the fact that Dafny reals or not just rationals, i.e. have completeness?

Update: I'd like to clarify that even though it may pedantic, I am not looking for answers that work around the actual question. Defining functions like sqrt axiomatic (without body) or proving lemmas about passed in variables that, by precondition, are irrational can be useful workarounds for many use cases, but they don't answer the question whether Dafny's reals deserve their name.

Of course these answers might help others that are less pedantic :)

Furthermore, if the answer is "It is theoretically possible, but nobody has ever done it.", then I would appreciate some detail as to why it is so hard. Why is proving 1 + 1 == 2 trivial while proving exists root: real :: 2 == root * root is hard, even though both follow almost immediately from z3's axioms and z3 has no trouble proving them?

Answer 1

I am not certain how to verify that statement. However, Dafny can reason about real numbers.

function div(x: real, y: real): (z: real)
    requires y != 0.0
{
    x/y
}

lemma sqrt(x: real, y: real) 
    requires x > 0.0
    requires y > 0.0 && y*y ==x
{
    assert div(x, y) == y;
    var sq :| sq != 0.0 && div(x, sq) == sq;
}

It seems like the standard approach is to require it's existence as an axiom and Dafny accepts it.

One implementation

As for defining derivatives, that will be a good bit of work. I implemented some basic definition and examples of limits of sequences here. If you can extend it all the way to derivatives I'd be interested to see it.