logic - ¿Qué significa "verdadero=falso" en Coq?

Question

[No estoy seguro de que esto sea apropiado para el desbordamiento de pila, pero aquí hay muchas otras preguntas de Coq, así que quizás alguien pueda ayudar]

Estoy trabajando en lo siguiente en http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28 (justo debajo de donde se presenta el caso). Tenga en cuenta que soy un completo principiante en esto y trabajo en casa, no soy un estudiante.

Theorem andb_true_elim1 : forall b c : bool,
andb b c = true -> b = true.
Proof.
intros b c H.
destruct b.
Case "b = true".
reflexivity.
Case "b = false".
rewrite <- H. reflexivity.
Qed.

y estoy mirando lo que hace la reescritura:

 Case := "b = false" : String.string
c : bool
H : andb false c = true
============================
false = true

luego rewrite <- H. se aplica:

 Case := "b = false" : String.string
c : bool
H : andb false c = true
============================
false = andb false c

y está claro cómo la prueba tendrá éxito.

Puedo ver cómo, en términos de manipulación de símbolos de forma mecánica, estoy llegando a una prueba. Esta bien. Pero me molesta el "significado". En particular, ¿cómo puedo tener false = true en medio de una prueba?

Parece que estoy haciendo algún tipo de discusión con contradicciones, pero no estoy seguro de qué. Siento que he estado siguiendo ciegamente las reglas y de alguna manera he llegado a un punto en el que estoy escribiendo tonterías.

¿Qué estoy haciendo arriba?

Espero que la pregunta sea clara.

Answer 1

Generalmente, cuando se hace un análisis de caso en un probador de teoremas, muchos de los casos se reducen a "no puede suceder". Por ejemplo, si está probando algún hecho sobre los enteros, es posible que deba hacer un análisis de caso para determinar si el entero i es positivo, cero o negativo. Pero puede haber otras hipótesis en tu contexto, o quizás alguna parte de tu objetivo, que sea contradictoria con uno de los casos. Puede que sepas por una afirmación anterior, por ejemplo, que nunca puedo ser negativo.

Sin embargo, Coq no es tan inteligente. Por lo tanto, todavía tiene que pasar por la mecánica de demostrar que las dos hipótesis contradictorias pueden unirse en una prueba de absurdo y, por lo tanto, una prueba de su teorema.

Piénsalo como en un programa de computadora:

switch (k) {
case X:
/* do stuff */
break;
case Y:
/* do other stuff */
break;
default:
assert(false, "can''t ever happen");
}

El false = true objetivo es el "no puede suceder nunca". Pero no puedes simplemente abrirse paso en Coq. Realmente tienes que poner un término de prueba.

Así que arriba, tienes que probar que la meta absurda es false = true . Y lo único con lo que tienes que trabajar es la hipótesis H: andb false c = true . Un momento de reflexión le mostrará que en realidad esta es una hipótesis absurda (porque andb false y reduce a false para cualquier y por lo tanto, no puede ser cierto). Así que golpeas la meta con la única cosa a tu disposición (a saber, H ) y tu nueva meta es false = andb false c .

Entonces aplicas una hipótesis absurda tratando de alcanzar un objetivo absurdo. Y he aquí que terminas con algo que realmente puedes mostrar por reflexividad. Qed.

ACTUALIZACIÓN Formalmente, esto es lo que está pasando.

Recuerde que cada definición inductiva en Coq viene con un principio de inducción. Estos son los tipos de principios de inducción para la igualdad y la proposición False (en oposición al término false de tipo bool ):

Check eq_ind.
eq_ind
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y
Check False_ind.
False_ind
: forall P : Prop, False -> P

El principio de inducción para False dice que si me das una prueba de False , puedo darte una prueba de cualquier proposición P

El principio de inducción para eq es más complicado. Considerémoslo confinado a bool . Y específicamente a false . Dice:

Check eq_ind false.
eq_ind false
: forall P : bool -> Prop, P false -> forall y : bool, false = y -> P y

Entonces, si comienzas con alguna proposición P(b) que depende de un booleano b , y tienes una prueba de P(false) , entonces para cualquier otro booleano y que sea igual a false , tienes una prueba de P(y) .

Esto no suena terriblemente emocionante, pero podemos aplicarlo a cualquier proposición P que queramos. Y queremos uno particularmente desagradable.

Check eq_ind false (fun b : bool => if b then False else True).
eq_ind false (fun b : bool => if b then False else True)
: (fun b : bool => if b then False else True) false ->
forall y : bool,
false = y -> (fun b : bool => if b then False else True) y

Simplificando un poco, lo que esto dice es True -> forall y : bool, false = y -> (if y then False else True) .

Así que esto quiere una prueba de la True y luego algunos valores booleanos que podamos elegir. Así que vamos a hacer eso.

Check eq_ind false (fun b : bool => if b then False else True) I true.
eq_ind false (fun b : bool => if b then False else True) I true
: false = true -> (fun b : bool => if b then False else True) true

Y aquí estamos: false = true -> False .

Combinando con lo que sabemos sobre el principio de inducción para False , tenemos: si me da una prueba de false = true , puedo probar cualquier proposición.

Así que volvemos a andb_true_elim1 . Tenemos una hipótesis H que es false = true . Y queremos probar algún tipo de objetivo. Como he mostrado anteriormente, existe un término de prueba que convierte las pruebas de false = true en pruebas de lo que quieras. Entonces, en particular, H es una prueba de false = true , por lo que ahora puede probar cualquier objetivo que desee.

Las tácticas son básicamente la maquinaria que construye el término de prueba.

Answer 2

Me doy cuenta de que esto es antiguo, pero quiero aclarar algunas de las intuiciones detrás de la respuesta de Lambdageek (en caso de que alguien encuentre esto)

Noté que el punto clave parece ser que definimos una función F:bool->Prop con diferentes valores en cada punto (ie. true => True y false => False ). Sin embargo, se puede mostrar fácilmente desde el principio de inducción para la igualdad eq_ind la idea intuitiva que

forall A:Type, forall P:A->Prop, forall x y:A, (x=y) -> (P x = P y),

Pero esto significaría que, asumiendo true=false , tenemos True=False , pero como sabemos que es True , derivamos False .

Lo que esto significa es que la propiedad fundamental que estamos usando es la capacidad de definir F , que viene dada por el principio de recursión para bool, bool_rect :

forall P:bool -> Type, P true -> P false -> (forall b:bool, P b)

estableciendo P (b:bool) := b=>Prop , entonces esto es lo mismo que

Prop -> Prop -> (forall b:bool, Prop),

donde ingresamos True y False para obtener nuestra función F

Answer 3

true = false es una declaración que compara dos valores booleanos diferentes. Dado que esos valores son diferentes, esta declaración claramente no es demostrable (en el contexto vacío).

Teniendo en cuenta tu prueba: llegas a la etapa en la que el objetivo es false = true , por lo que claramente no podrás probarlo ... pero lo false = true es que tu contexto (suposiciones) también es contradictorio. Esto sucede a menudo, por ejemplo, cuando realiza análisis de casos y uno de los casos es contradictorio con sus otras suposiciones.