Tenho um objetivo com uma variável existencial ?x. Para provar isso, preciso destruir um termo t e, nos diferentes casos gerados pela destruição de t, o termo para instanciar ?x deve ser diferente para ser correto.
Quando terminei de provar o primeiro caso, Coq instanciou ?x com base no meu primeiro caso, o que torna o segundo caso não demonstrável. Existe uma maneira de transformar um objetivo do formulário P(?x)em exists x,P(x)? Ou existem outras maneiras de resolver o problema que encontro?
Uma variável existencial é apenas um atalho para um termo que você não sabe ou não deseja escrever. Em particular, tem apenas uma instanciação, pois representa um termo fixo que ainda não foi escrito explicitamente. Em particular,
exists x, P xnão implica logicamenteP ?x. No seu caso, acredito que a solução é nunca introduzir?x, ou seja, evitar a tática que o introduziu (normalmenteeapply).