Início / coding / Perguntas / 77426613
Accepted
Random Citizen
Asked: 2023-11-05 23:52:47 +0800 CST

Por que 'especializar' não é uma tática inválida em uma prova?

  • 772

No livro de fundamentos de software ( arquivado ) a specializetática foi introduzida como forma de simplificar uma hipótese.

Não entendo por que é uma etapa válida em uma prova.

O exemplo fornecido aumenta minha confusão:

Theorem specialize_example: forall n,
     (forall m, m*n = 0)
  -> n = 0.
Proof.
  intros n H.
  specialize H with (m := 1).
  simpl in H.
  rewrite add_comm in H.
  simpl in H.
  apply H. Qed.

Quando substituo a hipótese (forall m, m*n = 0) -> n = 0.por 1*n = 0 -> n = 0., vejo que agora estamos provando com sucesso n=0essa nova hipótese.

Não entendo por que isso é aceito como prova do teorema original forall n, (forall m, m*n = 0) -> n = 0.. Não estamos agora continuando a provar um novo teorema forall n, 1*n = 0 -> n = 0.?

Como a prova do novo teorema se generaliza para ser uma prova válida para o teorema original?

O texto descreve a specializetática como “essencialmente apenas uma combinação de asserte apply” .
Talvez reescrever o script de prova deste (ou outro exemplo de uso specialize) para outro script de prova usando asserte applyem vez de specializepossa esclarecer as coisas.

coq

2 respostas

  1. Best Answer

    Não estamos agora continuando a provar um novo teorema forall n, 1*n = 0 -> n = 0?

    Na verdade, é isso que você está provando a princípio. Mas então você pode voltar ao seu teorema original e observar o ponto de partida (forall m, m*n = 0). Se esta afirmação for verdadeira, então ela implica 1*n = 0o que seu novo teorema implica n=0. Isso, portanto, prova o teorema original

    (forall m, m*n = 0) -> 1*n = 0 -> n=0

    (Eu não conheço a linguagem coq, então se a linha acima não estiver sintaticamente correta, ela significa simplesmente no sentido matemático A=>B=>C). Deixar cair a parte do meio entre as duas setas é o teorema original.

    Seu novo teorema é mais forte que o original, porque precisa de menos suposições para chegar à mesma conclusão.

    • 2

  2. [Prefiro postar isso como um comentário, mas ainda sou muito novo no SO.]

    Estou relutante em responder à primeira parte da sua pergunta para não estragar o exercício: Fundamentos Lógicos em particular é uma viagem e uma progressão em oposição a um compêndio de receitas, e a componente intelectual desse exercício, e sem o estragar, eu acho que é crucial.

    Quanto às suas dúvidas sobre a validade de tal transformação, talvez eu entenda o que você quer dizer: se estamos provando um teorema que deveria ser válido para todo n, como é que podemos prová-lo apenas para algum n? Mas agora observe que não é em n que estamos nos especializando acima, então se você também pensar como funciona a aplicação de hipóteses em oposição a objetivos...

    • 0

relate perguntas