Доказывая ковариационное неравенство в Дафни, использовать противоречие?
Я пытаюсь доказать в Дафни следующее свойство: covariance(x,y) <= variance(x) * variance(y), где x и y — это real.
Прежде всего, я хотел бы знать, правильно ли я интерпретирую ковариацию и дисперсию. Таким образом, я задаю следующий вопрос: прувинг covariance(x,y) <= variance(x) * variance(y) и прувинг covariance(x,y) <= covariance(x,x) * covariance(y,y) — это одно и то же? Я задаю этот вопрос, потому что дисперсия обычно имеет степень двойки (т. е. sigma^2(x)), что меня смущает.
Однако из https://en.wikipedia.org/wiki/Covariance я понимаю, что эта эквивалентность имеет место. Конкретно утверждается следующее: дисперсия — это частный случай ковариации, при котором две переменные идентичны.
Я также беру одно из определений ковариации по этой ссылке. Конкретно: cov(x,y)=(1/n)*summation(i from 1 to n){(x_i-mean(x))*(y_i-mean(y))}.
Таким образом, предполагая, что я должен доказать covariance(x,y) <= covariance(x,x) * covariance(y,y) и что ковариация определена, как указано выше, я проверяю следующую лемму в Дафни:
lemma covariance_equality (x: seq<real>, y:seq<real>)
requires |x| > 1 && |y| > 1; //my conditions
requires |x| == |y|; //my conditions
requires forall elemX :: elemX in x ==> 0.0 < elemX; //my conditions
requires forall elemY :: elemY in y ==> 0.0 < elemY; //my conditions
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; //my conditions
requires |x| == |y|; //my conditions
requires forall elemX :: elemX in x ==> 0.0 < elemX; //my conditions
requires forall elemY :: elemY in y ==> 0.0 < elemY; //my conditions
ensures covariance_fun (x,y) <= covariance_fun(x,x) * covariance_fun (y,y);
{
if !(covariance_fun(x,y) < covariance_fun(x,c) * covariance_fun (y,y)) {
//...
assert !(forall elemX' :: elemX' in x ==> 0.0<elemX') && (forall elemY' :: elemY' in y ==> 0.0<elemY'); //If we assume this, the proof is verified
assert false;
}
}
Мой главный вопрос: как я могу доказать эту лемму?
Чтобы у вас была вся информация, предлагаю функции, по которым складывается расчет ковариации. Во-первых, ковариационная функция выглядит следующим образом:
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)
}
Как видите, он выполняет суммирование, а затем делит на длину. Также обратите внимание, что функция суммирования получает среднее значение x и среднее значение y. Summation выглядит следующим образом:
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)
}
Как видите, он рекурсивно выполняет (x-mean(x))*(y-mean(y)) каждой позиции.
Что касается вспомогательных функций, mean_fun вычисляет среднее значение и выглядит следующим образом:
function method mean_fun(s:seq<real>):real
requires |s| >= 1;
decreases |s|;
{
sum_seq(s) / (|s| as real)
}
Обратите внимание, что здесь используется функция sum_seq, которая для заданной последовательности вычисляет сумму всех ее позиций. Он определяется рекурсивно:
function method sum_seq(s:seq<real>):real
decreases s;
{
if s == [] then 0.0 else s[0] + sum_seq(s[1..])
}
Теперь, со всеми этими ингредиентами, может ли кто-нибудь сказать мне (1), если я уже сделал что-то не так, и/или (2) как доказать лемму?
PS: Я искал, и эта лемма кажется неравенством Коши–Шварца, но до сих пор не знаю, как ее решить.
Уточняем ответ
Я буду (1) определять функцию конвариантности cov в терминах произведения, а затем (2) использовать это определение в новой лемме, которая должна быть верна.
Также обратите внимание, что я добавляю ограничение, что «x» и «y» не пусты, но вы можете изменить это
//calculates the mean of a sequence
function method mean_fun(s:seq<real>):real
requires |s| >= 1;
decreases |s|;
{
sum_seq(s) / (|s| as real)
}
//from x it constructs 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)
}
//covariance is calculated in terms of product
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) //if we do '(|x| as real)-1', then we can have a division by zero
//i.e., ensures cov(x,y) == product(a,b) / (|x| as real)
{
//if |a| == 1 then 0.0 //we do base case in '|a|==1' instead of '|a|==1', because we have precondition '|a| >= 1'
//else
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)
}
//Now, test that Cauchy holds for Cov
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);
}
\\IT DOES NOT HOLD!
Доказательство HelperLemma (не доказуемо?)
Пытаясь доказать HelperLemma, я обнаружил, что Дафни может доказать, что LHS a*a*x + b*b*y >= 2.0*a*b*z положителен.
Затем я начал доказывать разные случаи (я знаю, что это не лучшая процедура):
(1) Если один из a, b или z отрицательный (в то время как остальные положительные) или когда все три отрицательные; тогда RHS отрицательный
И когда RHS отрицателен, LHS больше или равен (поскольку LHS положителен).
(2) Если a, или b, или z равны 0, то RHS равно 0, поэтому LHS больше или равно.
(3) Если a>=1, b>=1 и z>=1, я пытался доказать это с помощью sqrt_ineq().
НО! Мы можем найти ПРОТИВОПРИМЕР.
С a=1, b=1, z=1 правая сторона равна 2; теперь выберите x как 0 и y как 0 (т.е. LHS=0). Поскольку 0<2, это контрпример.
Я прав? Если нет, то как я могу доказать эту лемму?
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*a*x + b*b*y is always positive
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; //2.0*a*b*z <= 0.0 is negative or 0 when product is negative
assert a*a*x + b*b*y >= 2.0*a*b*z; // When 2.0*a*b*z <= 0.0 is negative or 0, a*a*x + b*b*y is necessarily greater
}
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;
//INDEED: COUNTER EXAMPLE: a=1, b=1, z=1. Thus: RHS is 2; now, choose x to be 0 and y to be 0 (i.e., LHS=0). Since 0<2, this is a counter example.
}
}
Да, извините, covariance_indiv_fun(x) был альтернативой covariance_fun(x,x). Я исправляю это.
Ответы 1
Отредактировано после уточнения/исправления условия публикации.
Вот попытка сделать это в Дафни с помощью вычисления и индукции. Несколько замечаний по проверке
Поскольку сейчас стоит задача проверки, я предположил функцию sqrt и некоторые ее свойства. HelperLemma доказуема, если мы предполагаем некоторые свойства функции sqrt. В проверке есть два допущения, которые легко доказать.
function square(r: real) : real
ensures square(r) >= 0.0
{
r * r
}
function sqrt(r: real) : real
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..])
}
lemma sqrt_ineq(a: real, b: real)
requires a >= 0.0 && b >= 0.0
requires a <= b
ensures sqrt(a) <= sqrt(b)
lemma sqrt_square(a: real)
ensures sqrt(square(a)) == a
lemma CauchyBaseInequality(a1: real, a2: real, b1: real, b2: real)
ensures square(a1*b1 + a2*b2) <= (a1*a1 + a2*a2) * (b1*b1 + b2*b2)
{
calc <= {
square(a1*b1 + a2*b2) - (a1*a1 + a2*a2) * (b1*b1 + b2*b2);
a1*b1*a1*b1 + a2*b2*a2*b2 + 2.0*a1*b1*a2*b2 - a1*a1*b1*b1 - a1*a1*b2*b2 - a2*a2*b1*b1 - a2*a2*b2*b2;
2.0*a1*b1*a2*b2 - a1*a1*b2*b2 - a2*a2*b1*b1;
- square(a1*b2 - a2*b1);
0.0;
}
}
lemma HelperLemma(a: real, x: real, b: real, y: real, z: real)
requires x >= 0.0 && y >= 0.0
requires square(z) <= x * y
ensures a*a*x + b*b*y >= 2.0*a*b*z
lemma CauchyInequality(a: seq<real>, b: seq<real>)
requires |a| == |b|
ensures square(product(a, b)) <= product(a, a) * product(b, b)
{
if |a| <= 2 {
if |a| == 2 {
CauchyBaseInequality(a[0], a[1], b[0], b[1]);
}
}
else {
var x, xs := a[0], a[1..];
var y, ys := b[0], b[1..];
calc >= {
product(a, a) * product(b, b) - square((product(a, b)));
(x*x + product(xs, xs))*(y*y + product(ys, ys)) - square(x*y + product(xs, ys));
x*x*y*y + y*y*product(xs, xs) + x*x*product(ys, ys) + product(xs, xs)*product(ys, ys)
- x*x*y*y - square(product(xs, ys)) - 2.0*x*y*product(xs, ys);
y*y*product(xs, xs) + x*x*product(ys, ys) + product(xs, xs) * product(ys, ys)
- square(product(xs, ys)) - 2.0*x*y*product(xs, ys);
{ CauchyInequality(xs, ys); }
y*y*product(xs, xs) + x*x*product(ys, ys) - 2.0*x*y*product(xs, ys);
{
CauchyInequality(xs, ys);
assume product(xs, xs) >= 0.0;
assume product(ys, ys) >= 0.0;
HelperLemma(y, product(xs, xs), x, product(ys, ys), product(xs, ys));
}
0.0;
}
}
}
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)
{
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);
assert cov(x, y) == product(a, b) / (|x| as real);
assert cov(x, x) == product(a, a) / (|x| as real);
assert cov(y, y) == product(b, b) / (|x| as real);
CauchyInequality(a, b);
}
Проверка вспомогательной леммы
function square(r: real): real
ensures square(r) >= 0.0
{
r * r
}
function abs(a: real) : real
ensures abs(a) >= 0.0
{
if a < 0.0 then -a else a
}
function sqrt(r: real): real
requires r >= 0.0
ensures square(sqrt(r)) == r && sqrt(r) >= 0.0
lemma sqrtIneq(a: real, b: real)
requires a >= 0.0 && b >= 0.0
requires a <= b
ensures sqrt(a) <= sqrt(b)
lemma sqrtLemma(a: real)
ensures sqrt(square(a)) == abs(a)
lemma sqrtMultiply(a: real, b: real)
requires a >= 0.0 && b >= 0.0
ensures sqrt(a*b) == sqrt(a) * sqrt(b);
lemma differenceLemma(a: real, b: real)
requires a >= abs(b)
ensures a - b >= 0.0 && a + b >= 0.0
{
}
lemma HelperLemma(a: real, x: real, b: real, y: real, z: real)
requires x >= 0.0 && y >= 0.0
requires square(z) <= x * y
ensures a*a*x + b*b*y >= 2.0*a*b*z
{
var sx := sqrt(x);
var sy := sqrt(y);
assert sx * sx == x;
assert sy * sy == y;
if (a >= 0.0 && b >= 0.0) || (a < 0.0 && b < 0.0) {
calc >= {
a*a*x + b*b*y - 2.0*a*b*z;
a*a*sx*sx + b*b*sy*sy - 2.0*a*b*sx*sy + 2.0*a*b*sx*sy - 2.0*a*b*z;
square(a*sx - b*sy) + 2.0*a*b*sx*sy - 2.0*a*b*z;
2.0*a*b*sx*sy - 2.0*a*b*z;
2.0*a*b*(sx*sy - z);
{
sqrtIneq(square(z), x * y);
assert sqrt(x * y) >= sqrt(square(z));
sqrtMultiply(x, y);
assert sx * sy >= sqrt(square(z));
sqrtLemma(z);
assert sx * sy >= abs(z);
differenceLemma(sx*sy, z);
assert sx*sy >= z;
}
0.0;
}
}
else {
calc >= {
a*a*x + b*b*y - 2.0*a*b*z;
a*a*sx*sx + b*b*sy*sy + 2.0*a*b*sx*sy - 2.0*a*b*sx*sy - 2.0*a*b*z;
square(a*sx + b*sy) - 2.0*a*b*sx*sy - 2.0*a*b*z;
- 2.0*a*b*sx*sy - 2.0*a*b*z;
- 2.0*a*b*(sx*sy + z);
{
sqrtIneq(square(z), x * y);
assert sqrt(x * y) >= sqrt(square(z));
sqrtMultiply(x, y);
assert sx * sy >= sqrt(square(z));
sqrtLemma(z);
assert sx * sy >= abs(z);
differenceLemma(sx*sy, z);
assert sx*sy >= -z;
}
0.0;
}
}
}
Хм.. как это возможно? Я должен упустить некоторые условия, как вы говорите. Это должно выполняться, согласно определению en.wikipedia.org/wiki/Cauchy%E2%80%93Schwarz_inequality в «R n-мерном пространстве»..
Ну, теперь, когда я снова смотрю на эту ссылку, кажется, что она должна быть pow(covariance_fun (x,y),2) <= covariance_fun(x,x) * covariance_fun (y,y), вы видите то же самое? Обратите внимание, что часть pow() — это covariance_fun (x,y)*covariance_fun (x,y). Спасибо за ответ!
Да, проверял гарантирует (covariance_fun (x,y)*covariance_fun (x,y)) <= covariance_fun(x,x) * covariance_fun (y,y); и тоже не держит.
Это выглядит правильно. Я изменил свой ответ, чтобы показать первоначальную попытку доказать это. Но я боюсь, что dafny/z3 не подходит для нелинейной арифметики по проверке действительных чисел.
Привет, большое спасибо за ответ! Тем не менее, я пытаюсь следовать ему, и в нем отсутствует много кода :( (1) я думаю, что метод square получает a и возвращает a*a; (2) я думаю, что product мой covariance_fun; (3) я думаю, sqrt вычисляет квадрат root, но я не знаю, как это реализовать (я нахожу пример только для натуральных чисел). свойство будет держать?Откуда вы знаете, что?Мне нужно больше информации!:) Еще раз спасибо!!
Еще раз спасибо! Я активно изучаю этот код, так как не могу его полностью понять. Вернусь. Большая проблема, с которой я сталкиваюсь, связана с реализацией: т. е. мы, конечно, можем доказать это символически (т. е. с символическим определением свойств функции квадратного корня), но для фактической реализации фактического квадратного корня нужны методы аппроксимации. Я буду спрашивать больше об этом, и мы сможем получить ответ. Большое спасибо, эти материалы очень помогают.
Да, ты прав. реализация sqrt root будет методами аппроксимации. Поскольку весь смысл этого упражнения состоит в том, чтобы доказать, что определенные свойства не запускают программу, то кажется уместным предположить существование sqrt с некоторыми свойствами.
Полностью согласен. Однако я так понимаю, что assume и HelperLemma доказуемы с помощью Дафни, верно?
Вот и все. Кстати: есть пруверы, которые решают такие задачи (синус, квадрат...) до определенного момента: например, MetiTarski и dReal. Еще раз спасибо!
HelperLemma доказуема, если предположить, что sqrt_ineq и для каждого положительного действительного числа sqrt существует.
Я снова читаю код и думаю, что не понимаю вашего решения. Например, «ковариация» (я думаю, что это «произведение») не использует никакого «среднего» вычисления. А зачем ему топливо? Он должен развернуть формулу как минимум до длины списков, не так ли? Помощь :(
Согласно вашему наблюдению, исходное неравенство изоморфно неравенству Коши. Чтобы увидеть, выполните это преобразование, a = x - <x_mean> и b = y - <y_mean>, <> для представления последовательности с повторяющимся элементом. Предположим, что первые два остаются в силе, а третье нет, но это не требуется для доказательства. Топливо требуется для случая |a| == 2, где нам нужно a * b == a[0]*b[0] + a[1]*b[1]. Нет, он не будет разворачиваться до длины, но согласно определению, т. е. = a*b = a[0]*b[0] + a[1..]*b[1..], теперь разворачивается a[1. .] * b[1..] не произойдет из-за недостаточного количества топлива
Я думаю, что не понимаю, извините :( Мой вопрос прост: является ли product функцией covariance? Я проверил ее для случая дисперсии (т. Е. product(x,x)), и это не так. правильный ответ), тогда как a=[2,2] вернет covariance. 0 — это product, где 8 делает Covariance(a,a) (как и вы) и summation(a,a)/(|a|-1) (это другая часть).
Я знаю, что я что-то упустил, так как в Coq они доказали Коши-Шварц, также используя ваше определение product (см. второй ответ в stackoverflow.com/questions/67033055/…). Но мне нужно использовать типичное определение ковариации (то есть с суммированием), чтобы я мог использовать его в другом исполняемом коде. Посмотрим, поймаю ли я то, что мне не хватает.
product не то же самое, что covariance, но covariance можно выразить через product. covariance(x, x) = product(a, a) / |a|-1 где a = [x[0] - x_mean, x[1] - x_mean, ...]. Теперь все, что вы намеревались доказать изначально, можно доказать с помощью неравенства Коши с ковариацией, выраженной как произведение.
Я вижу, вы можете выразить ковариацию в терминах произведения. Однако, когда вы доказываете ensures square(product(a, b)) <= product(a, a) * product(b, b) в CauchyInequality, мне не кажется, что вы доказываете определенное мною неравенство, а именно: square(covariance(a, b)) <= covariance(a, a) * covariance(b, b). Поскольку мне кажется, что я этого не понимаю, я приведу следующее доказательство: я определю covariance через product и посмотрю, верна ли лемма square(covariance(a, b)) <= covariance(a, a) * covariance(b, b), используя ваше CauchyInequality в теле. Это звучит нормально?
Да нормально звучит. И кажется доказуемым с помощью CauchyInequality
Привет, я сделал это (см. «Разработка ответа» в посте), и это не удалось проверить. Есть идеи, почему?
Добавлен способ проверки неравенства cov и удалены некоторые предварительные условия в старых леммах, которые не требовались. Я бы посоветовал сначала наметить доказательство с помощью бумаги и карандаша, прежде чем проводить проверку с помощью инструментов. Это помогает, например, в вашей попытке передать неправильные аргументы.
Не могу поверить, что я так долго не понимал этого: проверка square(product(a, b)) <= product(a, a) * product(b, b) означает проверку square(cov(x,y)) <= cov(x,x)*cov(y,y), потому что последнее — это просто первое, но с обеими частями неравенства, разделенными на n^2. Боже мой, я просто неправильно понимал определение product снова и снова. Большое спасибо за ваше терпение и разъяснения. Все понятно и проверено.
Я понимаю, что Дафни имеет внутри себя аксиому, которая гласит что-то вроде (a/n)<=(b/n) подразумевает a<=b, потому что он способен проверить cauchyInequality_usingCov() только позвонив CauchyInequality(). Еще раз спасибо!!
Привет, извините за повторный вопрос, но я думаю, что есть assume, которое невозможно доказать. В CauchyInequality мы сталкиваемся с тремя допущениями: assume product(xs, xs) >= 0.0, assume product(ys, ys) >= 0.0 и assume product(xs, ys) >= 0.0. Первые два доказуемы, поскольку они умножаются сами на себя (таким образом, они всегда положительны): действительно, это причина, по которой variance(x) или covariance(x,x) всегда положительны. Однако последнее кажется неверным, product(xs, ys) >= 0.0 может быть отрицательным (как covariance(x,y) с x!=y может быть отрицательным). Я прав?
Да, но это предположение не требуется. Как HelperLemma, не имеет предусловия z >= 0.0. Позвольте мне удалить это
Я понимаю! Тоже удалил, еще раз спасибо. Конечно, это может быть так, что мы не принимаем отрицательную ковариацию (a, b), но это будет заявлено с символической гарантией, которую невозможно доказать... или мы должны добавить абсолютное значение. Еще раз спасибо!
Привет еще раз, я думаю, что HelperLemma не может быть доказана, я привел контрпример в (см. добавление «Доказательство HelperLemma» в посте).
Я добавил проверку HelperLemma. Одна вещь, которую я заметил, когда проверял, что мне нужно >= 0,0 и b >= 0,0 в качестве предварительного условия HelperLemma. Но это уже предусмотрено, так как все элементы обоих последовательностей положительны. Я изменил часть кода, чтобы отразить это. Что касается вашего контрпримера, вы не можете выбрать x и y равными 0 как квадрат (z) <= x * y. Таким образом, x * y должно быть больше 1.
Привет, большое спасибо за доказательство. Что касается «одной вещи, которую я заметил при проверке того, что мне нужны a >= 0,0 и b >= 0,0 в качестве предварительного условия HelperLemma», я думаю, что это не так. Я имею в виду, что для исходной последовательности s a[0] равно (s[0]-a_mean), что может быть отрицательным, даже если все элементы s положительны. Например, при s=[2,4] среднее равно 3, а a[0]=(2-3), что отрицательно.
Ты прав. Это можно доказать, когда a <0 или b <0. Я обновил свой ответ. Ваше здоровье
Я собирался сказать: устранение этого требует не дает никаких проблем. С возвращением!
Можете ли вы также дать определение
covariance_indiv_fun?