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.

Answer 2

You can prove the existence of square roots in Dafny using other axioms rather than just asserting their existence. Using some of the definitions in the original realAnalysis file I linked you can define them as the least upper bound of the reals squared that are less than the number.

In this case we need to call only 1 axiom, CompletenessAxiomUpper, which basically asserts that if given a bounded set of reals, which is not empty, then there exists a supremum.

The calculations get a bit gnarly in one case and require a few lemmas to verify.

//https://proofwiki.org/wiki/Existence_of_Square_Roots_of_Positive_Real_Number
lemma sqrtExists(r: real)
    requires r > 0.0
    ensures exists y :: r == y * y
{
    if r == 1.0 {
        assert r == r*r;
    }else{
    var S := iset x | x*x < r ;
    assert upperBound(S, r+1.0);
    forall x | x in S 
        ensures x < r+1.0
    {}

    forall y | y > r+1.0
        ensures y*y !in S
    {
        var r' := r +1.0;
        assert r' > 1.0;
        assert y > 1.0;
        assert y > r';
    }
    assert 0.0 in S;
    assert forall x :: x in S ==> x < r+1.0;
    CompletenessAxiomUpper(S,r+1.0);
    var u :| sup(S, u);
    if u*u > r {
        ArchimedeanPrinciple((u*u-r)/(2.0*u));
        var n: pos :| 1.0/(n as real) < (u*u-r)/(2.0*u);
        var u' := (u-1.0/(n as real));
        assert u' == sub(u,1.0/(n as real));
        assume upperBound(S, u');
        assert false;
    }
    if u*u < r {
        assert upperBound(S, u);
        assert u in S;
        if u < 0.0 {
            assert !upperBound(S, u);
            assert false;
        }else if u > 0.0 {
            assert (r-u*u)/(4.0*u) > 0.0;
            ArchimedeanPrinciple((r-u*u)/(4.0*u));
            ArchimedeanPrinciple(2.0*u);
            var na: pos :| 1.0 / (na as real) < ((r-u*u)/(4.0*u));
            var nb: pos :| 1.0 / (nb as real) < (2.0*u);
            var n := if na > nb then na else nb;
            NaturalFraction(n, nb);
            NaturalFraction(n, na);
            var nf := 1.0 / (n as real);
            assert nf > 0.0;
            assert 1.0 / (n as real) < 2.0*u;
            assert nf < 2.0*u;
            assert 1.0 / (n as real) < ((r-u*u)/(4.0*u));
            var u' := u+1.0/(n as real);
            calc {
                u'*u';
                (u+1.0/(n as real))*(u+1.0/(n as real));
                u*u+(2.0*u/(n as real))+(1.0/((n as real )*(n as real)));
            }
            calc {
                nf * nf;
                (1.0/((n as real )*(n as real)));
            }
            calc {
                nf * 2.0*u;
                (2.0*u/(n as real));
            }
            multLte(nf,2.0*u,nf);
            assert nf * nf < nf *(2.0*u);
            assert (1.0/((n as real )*(n as real))) < (2.0*u/(n as real));
            assert u*u+(2.0*u/(n as real))+(1.0/((n as real )*(n as real))) < u*u+(2.0*u/(n as real))+(2.0*u/(n as real));
            calc {
                (2.0*u/(n as real))+(2.0*u/(n as real));
                (4.0*u/(n as real));
            }
            assert r-u*u > (4.0*u/(n as real)) by {
                assert 1.0 / (n as real) < ((r-u*u)/(4.0*u));
                assert (n as real) >= 1.0;
                calc {
                1.0 / (n as real) < ((r-u*u)/(4.0*u));
                (4.0*u)* (1.0 / (n as real)) < (4.0*u)*((r-u*u)/(4.0*u));
                (4.0*u)* (1.0 / (n as real)) < (r-u*u);
                (4.0*u / (n as real)) < (r-u*u);
                }
            }
            assert u*u+(2.0*u/(n as real))+(2.0*u/(n as real)) <= u*u + (r - u*u);
            assert u' * u' < u*u+(2.0*u/(n as real))+(2.0*u/(n as real)) <=r ;
            assert u' * u' < r ;
            assert u' in S;
            assert false;
        }else if u == 0.0 {
            assert upperBound(S, 0.0);
            if r > 1.0 {
                assert 1.0 * 1.0 < r;
                assert 1.0 in S;
                assert false;
            }else {
                assert 0.0 < r < 1.0;
                var rs := r * r;
                smallerThanR(r,rs);
                assert rs in S;
                assert false;
            }
            assert false;
        }
    }
    
    assert u*u == r;
    }
}

https://github.com/hath995/Dafny4.4/blob/main/realAnalysis.dfy#L189 for the full definitions.

Answer 3

The following doesn't directly answer the question, so I'll not accept it. However it helped me in understanding a critical point about Dafny's real numbers.

Why shouldn't real be called rational or some other number system whose axioms/properties we can prove real to satisfy? Wouldn't that be more natural than to state that Dafny's reals are indeed real numbers even though this fact doesn't seem to be usable?

My answer: Adding completeness axioms doesn't lead to contradictions (I hope!). If we assume completeness of a hypothetical rational type, we would be able to derive false by using completeness to get a "rational square root of 2" and then show that square root of 2 is not a rational number.

The other way around, we can't prove that real is actually the set of rational numbers, because we can't prove that irrational numbers are not in real. E.g. we can't prove forall r: real :: exists p: nat, q: nat :: r == p as real / q as real.

So even though apparently we can't prove that real is the set of real numbers, we can't prove that it is the set of rational numbers either. Furthermore, assuming completeness (hopefully) doesn't lead to contradictions, so there is an argument that real resembles the real numbers more than the rational numbers.

That being said, I cannot rule out that we could add forall r: real :: exists p: nat, q: nat :: r == p as real / q as real as an axiom without being able to derive contradictions either.