Actualmente tengo que aprender Coq y no sé cómo lidiar con un or
:
Como ejemplo, tan simple como es, no veo cómo demostrar:
Theorem T0: x \/ ~x.
Realmente lo agradecería si alguien pudiera ayudarme.
Como referencia utilizo esta hoja de trucos .
También un ejemplo de una prueba que tengo en mente: aquí para doble negación:
Require Import Classical_Prop.
Parameters x: Prop.
Theorem T7: (~~x) -> x.
intro H.
apply NNPP.
exact H.
Qed.
NNPP
El tipo esforall p:Prop, ~ ~ p -> p.
, así que es una trampa usarlo para probarT7
. Cuando importasClassical_Prop
obtienesAxiom classic : forall P:Prop, P \/ ~ P.
apply classic.
resuelve tu objetivoT0
.Respuestas:
No se puede probar en Coq "vainilla", porque se basa en una lógica intuicionista :
Hay varias formas de lidiar con una situación como esta.
Introduzca la ley del medio excluido como un axioma:
No hay más necesidad de probar nada después de este punto.
Introducir algún axioma equivalente a la ley del medio excluido y demostrar su equivalencia. Aquí hay solo algunos ejemplos.
La eliminación de la doble negación es uno de esos axiomas:
La ley de Peirce es otro ejemplo:
O use una de las leyes de De Morgan :
fuente
Axiom peirce
: tal como está, no es la ley de Peirce (y de hecho estrivial
para probar).Como otros le informaron, su tautología no es una tautología a menos que asuma la lógica clásica. Pero como estás haciendo tautologías sobre valores de verdad decidibles, puedes usarlas en
bool
lugar deProp
. Entonces su tautología sostiene:fuente