Início / coding / Perguntas / 77699115
Accepted
pratyai
Asked: 2023-12-21 23:58:29 +0800 CST

Provar que "cada elemento em uma sequência é 0 ==> o elemento em cada índice da sequência é 0" é contra-intuitivo. Como raciocinar sobre isso?

  • 772
lemma blah(p:nat->bool, xs:seq<nat>)
  requires forall t | t in xs :: p(t)
  ensures forall i | 0 <= i < |xs| :: p(xs[i]) {}

lemma zero_is_zero(xs:seq<nat>)
  requires forall x | x in xs :: (x == 0)
  ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) {
  // blah(x => x == 0, xs);
}

Então, estou testando a versão dafny 4.4.0e estou lutando para entender o trecho de código acima. Corresponde aproximadamente a um dos dois lemas relevantes aqui ; mas eu os simplifiquei um pouco.

Meu entendimento é que o zero_is_zerolema é basicamente uma generalização do blahlema (sendo a propriedade pneste caso x => x == 0). Então, na verdade, deveria ser mais fácil verificar automaticamente o zero_is_zero. Eu esperava que um elemento da sequência fosse considerado indistinguível do mesmo elemento quando acessado por meio de um índice.

Na prática, acontece que isso blahé verificado automaticamente (ou seja, não preciso fazer nada no corpo do lema). Mas zero_is_zerotenho que invocar explicitamente blahpara mostrar que isso realmente vale para a propriedade x => x == 0e, de repente, não é mais um problema.

Qual é a explicação para isso?

Obrigado!

dafny

1 respostas

  1. Best Answer

    Em Dafny o conceito de gatilhos é importante para qualquer operador existencial ou para todos. Aqui você especificou isso x in xscomo o gatilho para um valor ser zero. Portanto, você precisa invocar esse gatilho para verificar a sequência.

    lemma zero_is_zero(xs:seq<nat>)
  requires forall x | x in xs :: (x == 0)
  ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) 
{
    forall k | 0 <= k < |xs|
        ensures xs[k] == 0
    {
      assert xs[k] in xs;
    }
}
    • 1

relate perguntas