Dafny cannot prove that 'a^2<=b^2*c^2' implies 'a<=b*c' for reals greater than 0

Question

I want to test the following property in Dafny: a^2<=b^2*c^2 implies a<=b*c. It automatically checks this for (positive) integer numbers:

lemma powersVSsquares_integers(a:int, b:int, c:int)
   requires a>=0 && b>=0 && c>= 0
   ensures (a*a <= b*b*c*c) ==> (a<=b*c)
   {}

Now, I want to test this for real numbers, so I try:

lemma powersVSsquares_reals(a:real, b:real, c:real)
   requires a>=0.0 && b>=0.0 && c>=0.0
   ensures (a*a <= b*b*c*c) ==> (a<=b*c)
   {}

But Dafny cannot prove this. Thus, I start with the case where a>=1.0 & b>=1.0 & c>=1.0:

lemma powersVSsquares_reals1(a:real, b:real, c:real)
   requires (a>=1.0 && b>=1.0 && c>=1.0)
   ensures (a*a <= b*b*c*c) ==> (a<=b*c)
   {
     assert a <= (b*b*c*c)/a;
   }

But not even assert a <= (b*b*c*c)/a; can be proven. So I have no idea on how to deal with this prove.

Can anyone provide lemma powersVSsquares_reals proven in Dafny? Can this be done without defining a symbolic square root function?

Answer 1

I think you will need some axioms of the reals that are not readily available in Dafny.

lemma increase(a: real, b: real, x: real)
  requires x > 0.0
  requires a > b
  ensures a * x > b * x
{
}


lemma zero(a: real)
  requires a*a == 0.0
  ensures a == 0.0
{
  if a != 0.0 {
    if a > 0.0 {
      increase(a, 0.0, a);
      assert false;
    } else if a < 0.0 {
      increase(-a, 0.0, -a);
      assert false;
    }
  }
}

Then you can use these axioms to do a regular proof. Here I choose the style of a proof by contradiction

lemma powersVSsquares_reals(a:real, b:real, c:real)
   requires a>=0.0 && b>=0.0 && c>=0.0
   ensures (a*a <= (b*b)*(c*c)) ==> (a<=b*c)
   {
  if a*a <= (b*b)*(c*c) {
    if a == 0.0 {
      return;
    }
    if b == 0.0 || c == 0.0 {
      zero(a);
      return;
    }
    assert a*a <= (b*c)*(b*c);
    if a > (b*c) {
      assert b * c > 0.0;
      increase(a, b*c, b*c);
      assert a * (b*c) > (b * c) * (b*c);
      assert a > 0.0;
      increase(a, b*c, a);
      assert a * a > (b * c) * a;
      assert a * a > (b * c) * (b*c);
      assert false;
    }
    assert a<=b*c;
  }
}