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.