Início / coding / Perguntas / 79586887
Accepted
Caleb Stanford
Asked: 2025-04-22 23:47:19 +0800 CST

Introdução de quantificadores em Dafny: prove que abs é sobrejetivo

  • 772

Esta é uma pergunta semelhante, mas não consegui mapeá-la para o meu caso de uso. Basicamente, quero usar Dafny para provar uma afirmação básica com quantificadores aninhados (para todo X existe Y) em lógica de primeira ordem sobre inteiros. A afirmação específica que escolhi é que a absfunção é sobrejetiva em inteiros não negativos. Aqui está um trecho de código minimizado:

function abs(x: int): int {
    if x > 0 then x else -x
}

// Passes the verifier
lemma AbsSurjectiveFor(y: int)
requires y >= 0
ensures exists x :: abs(x) == y
{
    assert abs(y) == y;
}

// Error in this lemma (universal generalization of the above)
lemma AbsSurjective()
ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
{
    // Forall introduction syntax
    forall y: int | y >= 0
    ensures exists x :: abs(x) == y
    {
        AbsSurjectiveFor(y);
    }
}

Pergunta

Qual é a sintaxe correta para que o segundo lema seja aprovado?

De forma mais geral, estou procurando a sintaxe para as regras de introdução e eliminação para todos, caso eu queira fazer uma demonstração manualmente (por exemplo, em um estilo de dedução natural). Suspeito que estou fazendo algo muito "óbvio" errado, mas não consegui encontrar a sintaxe correta no manual de referência.

Notas

Dafny prova o primeiro lema (fácil, não é necessária a introdução de um quantificador), mas falha no segundo lema, embora eu tenha correspondido exatamente à sintaxe dada na resposta de Rustan , que sugere usar um bloco de instruções forall dentro do lema.

Uma dica do que pode estar errado é que estou recebendo avisos por usar quantificadores sem gatilhos. No entanto, não me importo muito com os gatilhos, pois minha intenção é provar as instruções forall/exists manualmente. Não tenho certeza se existe uma maneira de simplesmente desativar os gatilhos ou dizer ao Dafny para não instanciar os quantificadores, a menos que eu diga para ele fazer isso.

Saída de dafny verify:

$ dafny verify fol-minimal.dfy 
fol-minimal.dfy(15,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(18,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
18 |     forall y: int | y >= 0
   |     ^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(16,0): Error: a postcondition could not be proved on this return path
   |
16 | {
   | ^

fol-minimal.dfy(15,8): Related location: this is the postcondition that could not be proved
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
dafny

1 respostas

  1. Best Answer

    Você pode validar isso movendo suas condições para funções predicativas. Gatilhos são basicamente os símbolos que o verificador usa para reconhecer quando certas condições são verdadeiras. Tecnicamente, eles não são iguais às funções predicativas, mas, na maioria dos casos, é possível estabelecer essa equivalência. Um requisito importante para gatilhos é que eles não podem conter aritmética.

    Portanto, uma instrução como essa x + 1 > 0não é um gatilho válido. No entanto, ao movê-la para uma função de predicado como predicate nextGTZ(x: int) { x + 1 > 0}essa, você pode fazer uma implicação como essa nextGTZ(x) ==> Q(x)e ela reconhecerá o gatilho.

    Recomendo praticar este exercício aqui . Além de ler este FAQ

    Pergunta mais antiga: aqui

    module CalebStanford {
    function abs(x: int): int {
        if x > 0 then x else -x
    }

    predicate IsNat(x: int)
    {
        x >= 0
    }

    // Passes the verifier
    lemma AbsSurjectiveFor(y: int)
        requires IsNat(y)
        ensures exists x :: abs(x) == y
    {
        assert abs(y) == y;
    }

    // Error in this lemma (universal generalization of the above)
    lemma AbsSurjective()
        ensures forall y: int :: IsNat(y) ==> (exists x :: abs(x) == y)
    {
        // Forall introduction syntax
        forall y: int | IsNat(y)
        ensures exists x :: abs(x) == y
        {
            AbsSurjectiveFor(y);
        }
    }
}
    • 2

relate perguntas