Вопрос о дафни для доказательства леммы in seq‹int›

Я только начинаю учиться с Дафни. Теперь у меня есть предикат:

predicate allEqual(s:seq<int>)
//{forall i,j::0<=i<|s| && 0<=j<|s| ==> s[i]==s[j] }
//{forall i,j::0<=i<=j<|s| ==> s[i]==s[j] }
//{forall i::0<i<|s| ==> s[i-1]==s[i]} 
{forall i::0<=i<|s|-1 ==> s[i]==s[i+1]}

и тогда мне нужно доказать лемму:

lemma equivalenceContiguous(s:seq<int>)
ensures (allEqual(s) <==> forall i::0<=i<|s|-1 ==> s[i]==s[i+1])

как я могу это доказать? Насколько я знаю, мне нужно написать «утверждать» или что-то в этом роде?


dafny
person shirleyChen    schedule 16.02.2020    source источник
comment
Почему это помечено как c?   -  person Ed Heal    schedule 16.02.2020

Ответы (1)


arrow_upward
0
arrow_downward

Это доказательство особенно просто, поскольку вы пытаетесь доказать, что allEqual является тем, чем оно определено. Просто добавьте к лемме пустое тело:

lemma equivalenceContiguous(s: seq<int>)
  ensures allEqual(s) <==> forall i :: 0 <= i < |s| - 1 ==> s[i] == s[i+1]
{
}
person Rustan Leino    schedule 18.02.2020
comment
Я не думал, что придет .. так что все, что мне нужно сделать, это просто добавить пустой корпус? Но пустое тело ничего не значило... Вы имеете в виду, что Дафни обладает способностью автоматически доказывать какую-то лемму, и тогда он может сам понять эту лемму? - person shirleyChen; 20.02.2020
comment
Чтобы объявить лемму, вы пишете что-то вроде lemma Name(params: Types) ensures <Condition-to-prove>. Чтобы дать доказательство, вы следуете за этим объявлением с блоком кода, точно так же, как вы делаете для method. В этом случае достаточно пустого тела, потому что доказательство тривиально. - person Rustan Leino; 21.02.2020