在Dafny中证明协方差不等式的问题及求证困境

问题背景 #

我尝试在Dafny中证明性质covariance(x,y) <= variance(x) * variance(y)（其中x和y为real类型）。首先有个疑问：证明该式与证明covariance(x,y) <= covariance(x,x) * covariance(y,y)是否等价？由于方差常以平方形式（sigma^2(x)）出现，让我感到困惑。根据维基百科，方差是协方差的特殊情况（当两个变量相同时），因此我认为二者是等价的。

我采用协方差的定义：cov(x,y)=(1/n)*summation(i from 1 to n){(x_i-mean(x))*(y_i-mean(y))}，并在Dafny中实现了相关计算函数：

function method covariance_fun(x:seq<real>, y:seq<real>):real
    requires |x| > 1 && |y| > 1;
    requires |x| == |y|;
    decreases |x|,|y|;
{
    summation(x,mean_fun(x),y,mean_fun(y)) / ((|x|-1) as real)
}

function method summation(x:seq<real>,x_mean:real,y:seq<real>,y_mean:real):real
  requires |x| == |y|;
  decreases |x|,|y|;
{
if x == [] then 0.0 
else ((x[0] - x_mean)*(y[0] - y_mean)) 
    + summation(x[1..],x_mean,y[1..],y_mean)
}

function method mean_fun(s:seq<real>):real
  requires |s| >= 1;
  decreases |s|;
{
    sum_seq(s) / (|s| as real)
}

function method sum_seq(s:seq<real>):real
  decreases s;
{
if s == [] then 0.0 else s[0] + sum_seq(s[1..])
}

第一次尝试：编写covariance_equality引理 #

我编写了如下引理，但无法自动证明，尝试反证法也未成功：

lemma covariance_equality (x: seq<real>, y:seq<real>)
    requires |x| > 1 && |y| > 1; //自定义条件
    requires |x| == |y|; //自定义条件
    requires forall elemX :: elemX in x ==> 0.0 < elemX; //自定义条件
    requires forall elemY :: elemY in y ==> 0.0 < elemY; //自定义条件
    ensures covariance_fun (x,y) <= covariance_fun(x,x) * covariance_fun (y,y);
    {}

反证法尝试的代码：

lemma covariance_equality (x: seq<real>, y:seq<real>)
    requires |x| > 1 && |y| > 1; //自定义条件
    requires |x| == |y|; //自定义条件
    requires forall elemX :: elemX in x ==> 0.0 < elemX; //自定义条件
    requires forall elemY :: elemY in y ==> 0.0 < elemY; //自定义条件
    ensures covariance_fun (x,y) <= covariance_fun(x,x) * covariance_fun (y,y);
    {

    if !(covariance_fun(x,y) < covariance_fun(x,x) * covariance_fun (y,y)) {

      //...
      assert !(forall elemX' :: elemX' in x ==> 0.0<elemX') && (forall elemY' :: elemY' in y ==> 0.0<elemY'); //若假设此条件，验证通过
      assert false;
    } 

}

第二次尝试：基于柯西-施瓦茨不等式重新定义 #

我发现该引理本质对应柯西-施瓦茨（Cauchy–Schwarz）不等式，于是重新定义协方差函数cov并编写引理cauchyInequality_usingCov，但仍然无法成立：

//计算序列的均值
function method mean_fun(s:seq<real>):real
  requires |s| >= 1;
  decreases |s|;
{
    sum_seq(s) / (|s| as real)
}

//从x构造序列a=[x[0]-x_mean, x[1]-x_mean...]
function construct_list (x:seq<real>, m:real) : (a:seq<real>)
  requires |x| >= 1
  ensures |x|==|a|
  {
    if |x| == 1 then [x[0]-m]
    else [x[0]-m] + construct_list(x[1..],m)
  }

//用内积计算协方差
function cov(x: seq<real>, y: seq<real>) : real
  requires |x| == |y|
  requires |x| >= 1
  ensures cov(x,y) == product(construct_list(x, mean_fun(x)),construct_list(y, mean_fun(y))) / (|x| as real) //若使用'(|x| as real)-1'会出现除零问题
{
  var x_mean := mean_fun(x);
  var y_mean := mean_fun(y);

  var a := construct_list(x, x_mean);
  var b := construct_list(y, y_mean);

  product(a,b) / (|a| as real)
}

//测试协方差的柯西不等式是否成立
lemma cauchyInequality_usingCov (x: seq<real>, y: seq<real>)
   requires |x| == |y|
   requires |x| >= 1
   requires forall i :: 0 <= i < |x| ==> x[i] >= 0.0 && y[i] >= 0.0
   ensures square(cov(x,y)) <= cov(x,x)*cov(y,y)
{
   CauchyInequality(x,y);
}
// 无法成立！

HelperLemma的问题 #

在证明HelperLemma时，我发现了反例：当a=1、b=1、z=1、x=0、y=0时，引理不成立。我不确定这个反例是否正确，现在寻求以下解答：

• 定义或代码是否存在错误？
• 如何证明原协方差不等式引理？
• 如何证明HelperLemma或确认其无法证明？

HelperLemma代码如下：

lemma HelperLemma(a: real, x: real, b: real, y: real, z: real)
  requires x >= 0.0 && y >= 0.0 //&& z >= 0.0
  requires square(z) <= x * y
  ensures a*a*x + b*b*y >= 2.0*a*b*z
  {
    assert square(z) == z*z;
    assert a*a*x + b*b*y >= 0.0; //a²x + b²y始终非负

    if ((a<0.0 && b>=0.0 && z>=0.0) || (a>=0.0 && b<0.0 && z>=0.0) || (a>=0.0 && b>=0.0 && z<0.0) || (a<0.0 && b<0.0 && z<0.0)) {
      assert 2.0*a*b*z <=0.0; //当乘积为负时，2abz ≤ 0
      assert a*a*x + b*b*y >= 2.0*a*b*z; //此时a²x + b²y必然大于等于2abz
    }

    if (a==0.0 || b==0.0 || z==0.0){
      assert a*a*x + b*b*y >= 2.0*a*b*z;
    }

    else if (a>=1.0 && b>=1.0 && z>= 1.0){
      assert a*a >= a;
      assert b*b >= b;

      assert a*a+b*b >= a*b;

      assert square(z) <= x * y;
      //sqrt_ineq(square(z),x*y);
      //assert square(z) == z*z;
      //sqrt_square(z);
      //assert sqrt(z) <= sqrt(x*y);
      //assert (x==0.0 || y == 0.0) ==> (x*y==0.0) ==> (square(z) <= 0.0) ==> z<=0.0;
      assert a*a*x + b*b*y >= 2.0*a*b*z;
      // 确实存在反例：a=1, b=1, z=1，此时右侧为2；取x=0、y=0，左侧为0，0<2，引理不成立
    }
  }

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