¿Puede alguien darme por favor un ejemplo simple de instanciación existencial y generalización existencial en Coq? Cuando quiero probar exists x, P, donde P es Prop que usa x, a menudo quiero nombrar x (como x0 o algo así), y manipular P. ¿Puede ser esto en Coq?ejemplificación existencial y generalización en coq
Si va a demostrar la existencia directamente y no a través de un lema, puede usar eapply ex_intro. Esto introduce una variable existencial (escrita ?42). A continuación, puede manipular el término. Para completar la prueba, debe proporcionar una forma de construir un valor para esa variable. Puede hacerlo explícitamente con la táctica instantiate, o implícitamente a través de tácticas como eauto.
Tenga en cuenta que a menudo es engorroso trabajar con variables existenciales. Muchas tácticas suponen que todos los términos son instanciados y pueden ocultar los existentes en subgoles; solo se enterará cuando Qed le diga "Error: intento de guardar una prueba incompleta". Solo debe usar variables existenciales cuando tenga un plan para instanciarlas pronto.
Aquí hay un ejemplo tonto que ilustra el uso de eapply.
Goal exists x, 1 + x = 3.
Proof. (* ⊢ exists x, 1 + x = 3 *)
eapply ex_intro. (* ⊢ 1 + ?42 = 3 *)
simpl. (* ⊢ S ?42 = 3 *)
apply f_equal. (* ⊢ ?42 = 2 *)
reflexivity. (* proof completed *)
Qed.
Con Coq trunk puede convertir existenciales no activados en subobjetivos al final de la prueba, que es algo que deseaba desde hace mucho tiempo. –
Una adición a [el comentario anterior] (https://stackoverflow.com/questions/10686164/existencial-instantiation-and-generalization-in-coq#comment13933112_10693631): esto se puede hacer con ['Grab Existenntial Variables'] (https://coq.inria.fr/refman/Reference-Manual009.html#GrabEvars) –
Sé que ha habido preguntas coq aquí en el pasado, pero sospecho que a medida que se introducen en el mejor lugar para las preguntas más sitios Coq es ahora http://cs.stackexchange.com/ (no tan contentos con la fragmentación yo mismo, pero es un hecho de la vida ...) –
@andrewcooke [Esto no se ha establecido de manera concluyente.] (http://meta.cs.stackexchange.com/questions/52/scope-limits-on- proof-assistants-eg-coq) Mi sensación es que las preguntas de Coq son más sobre el tema en SO si el objetivo es hacer una prueba, y en [cs.se] si el objetivo es entender por qué está funcionando una técnica de prueba o no funciona, pero es una línea muy delgada. La experiencia se extiende por [so], [cs.se] y [cstheory.se]. – Gilles