如何在Dafny中证明方差（cov(x,x)）非负？

问题描述 #

需要在Dafny中证明variance(x)（即cov(x,x)）≥0，其中协方差定义为：

cov(x,y) = 1/N * Σ{i=1到N} (x_i - x_mean) * (y_i - y_mean)
其中N是序列x、y的元素个数，x_mean是x的均值，y_mean是y的均值。

已定义的协方差相关函数 #

// 计算序列所有元素的和
function method sum_seq(s: seq<real>): (res: real)
  ensures (forall i :: 0 <= i < |s| ==> s[i] >= 0.0) ==> res >= 0.0
  decreases s;
{
  if s == [] then 0.0 else s[0] + sum_seq(s[1..])
}

// 计算序列的均值
function method mean_fun(s: seq<real>): (res: real) 
  requires |s| >= 1;
  decreases |s|;
  ensures (forall i :: 0 <= i < |s| ==> s[i] >= 0.0) ==> res >= 0.0
{
    sum_seq(s) / (|s| as real)
}
   
// 构造序列：每个元素为原序列元素减去给定均值m
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 {:fuel 2} product(a: seq<real>, b: seq<real>): real
  requires |a| == |b|
{
  if |a| == 0 then 0.0
  else a[0] * b[0] + product(a[1..], b[1..])
}

// 协方差函数：乘积和除以元素个数
function cov(x: seq<real>, y: seq<real>): (res: 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)
{
  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)
} 

当前尝试的问题 #

为证明cov(a,a)≥0，我尝试编写引理covarianceItself_positive但无法直接验证，转而试图证明product(construct_list(a, mean_fun(a)), construct_list(a, mean_fun(a))) ≥ 0，并编写了引理productItself_positive，但遇到两个问题：

• Dafny提示计算步骤不成立；
• 递归验证容易卡住，不确定思路是否正确。

当前的引理代码：

lemma productItself_positive(a: seq<real>)
   requires |a| >= 1
   requires forall i :: 0 <= i < |a| ==> a[i] >= 0.0
   ensures product(construct_list(a, mean_fun(a)), construct_list(a, mean_fun(a))) >= 0.0  
{
    if (|a|==1){
        assert product(construct_list(a, mean_fun(a)), construct_list(a, mean_fun(a))) >= 0.0;
    } 
    else {
        calc >= {
            product(construct_list(a, mean_fun(a)), construct_list(a, mean_fun(a)));
            {
              assert forall x:real :: forall y:real :: (x>=0.0 && y>=0.0) ==> (x*y>=0.0);
              assert forall x:real :: forall y:real :: (x>=0.0 && y>=0.0) ==> (x+y>=0.0);

              assert construct_list(a, mean_fun(a))[0] * construct_list(a, mean_fun(a))[0] >= 0.0;
              productItself_positive(a[1..]);
              // assert product(a[1..],a[1..]) >= 0.0; // 无限循环

            }
            // 此处步骤无法通过验证
            0.0;
        }
    } 
} 

解决方案 #

核心问题是原思路的递归逻辑错误：construct_list(a, mean_fun(a))[1..]并不等于construct_list(a[1..], mean_fun(a[1..]))（因为子序列的均值和原序列的均值不同），因此不能直接递归调用子序列的productItself_positive。

正确的思路是先证明任意序列的自乘积（product(s,s)）是非负的，因为它本质是序列元素的平方和，而平方数非负，和也非负。之后直接将该结论应用到construct_list(a, mean_fun(a))这个序列上即可。

修正后的引理代码 #

// 引理：任意序列的自乘积（元素平方和）非负
lemma product_self_nonnegative(s: seq<real>)
  requires |s| >= 0
  ensures product(s, s) >= 0.0
{
  if |s| == 0 {
    assert product(s, s) == 0.0;
  } else {
    // 递归调用子序列
    product_self_nonnegative(s[1..]);
    // 展开product的定义
    calc >= {
      product(s, s);
      // 根据product的定义展开
      s[0] * s[0] + product(s[1..], s[1..]);
      {
        // 平方数非负，子序列的自乘积也非负，两者之和非负
        assert s[0] * s[0] >= 0.0;
        assert product(s[1..], s[1..]) >= 0.0;
      }
      0.0 + 0.0;
      0.0;
    }
  }
}

// 引理：自协方差（方差）非负
lemma covariance_self_nonnegative(a: seq<real>)
  requires |a| >= 1
  ensures cov(a, a) >= 0.0
{
  let centered := construct_list(a, mean_fun(a));
  // 应用自乘积非负的引理
  product_self_nonnegative(centered);
  // 协方差是自乘积除以元素个数（正实数），非负数除以正数仍非负
  calc >= {
    cov(a, a);
    product(centered, centered) / (|a| as real);
    {
      assert product(centered, centered) >= 0.0;
      assert (|a| as real) > 0.0;
    }
    0.0 / (|a| as real);
    0.0;
  }
}

解释 #

1. product_self_nonnegative引理：直接针对product(s,s)进行递归证明，利用平方数非负、非负数之和非负的性质，递归子序列的结论即可完成证明，逻辑清晰且不会卡住。
2. covariance_self_nonnegative引理：先构造中心化序列centered，应用上述引理得到其自乘积非负，再结合“非负数除以正实数仍非负”的性质，直接推导出协方差非负。

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