无法在Dafny中证明实数乘积等于1的简单性质，求问题解析

我无法证明一个简单的实数性质：当0≤a≤1 ∧ 0≤b≤1 ∧ -1≤c≤1时，若a*b*c==1，则必然有a=1 ∧ b=1 ∧ c=1。

第一次尝试 #

我先写了如下Dafny代码：

lemma threepowers(a:real,b:real,c:real)
   requires 0.0<=a<=1.0 && 0.0<=b<=1.0 && -1.0<=c<=1.0
   ensures a*b*c==1.0 ==> a==1.0 && b==1.0 && c==1.0
   {
     if (a<1.0 || b<1.0 || c<1.0){
       assert a*b*c < 1.0;
     }
   }

但代码中的断言验证失败。

分情况证明的尝试 #

于是我改用分情况证明的思路（仅展示部分情况）：

lemma threepowers(a:real,b:real,c:real)
   requires 0.0<=a<=1.0 && 0.0<=b<=1.0 && -1.0<=c<=1.0
   ensures a*b*c==1.0 ==> a==1.0 && b==1.0 && c==1.0
   {
     if (a==1.0){
       if ((b == 1.0 && c!=1.0)||(b != 1.0 && c==1.0)){
         assert a*b*c!=1.0;
       }
       else if (b != 1.0 && c!=1.0){
         assert a*b*c!=1.0;
       }
     }
   }

但Dafny依然无法验证：当b和c均不等于1（结合前置条件可知它们小于1）时，乘积a*b*c不等于1。

调用Z3的尝试 #

我还尝试直接调用Z3证明全称量词的版本：

lemma threepowers(a:real,b:real,c:real)
   requires 0.0<=a<=1.0 && 0.0<=b<=1.0 && -1.0<=c<=1.0
   ensures a*b*c==1.0 ==> a==1.0 && b==1.0 && c==1.0
   {
     assert forall x:real :: forall y:real :: forall z:real :: (0.0<=x<1.0) || (0.0<=y<1.0) || (-1.0<=z<1.0) ==> (x*y*z<1.0);
   }

结果还是无法证明该性质。

我到底忽略了什么基本问题？

内容的提问来源于stack exchange，提问作者Theo Deep