Generalmente, cuando haces 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 números enteros, puede necesitar hacer un análisis de caso de si el número entero i es positivo, cero o negativo. Pero puede haber otras hipótesis en su contexto, o quizás alguna parte de su objetivo, que sea contradictoria con uno de los casos. Puede saber por una afirmación anterior, por ejemplo, que i nunca puede ser negativo.
Sin embargo, Coq no es tan inteligente. De modo que todavía tiene que pasar por la mecánica de mostrar realmente que las dos hipótesis contradictorias se pueden unir en una prueba de absurdo y, por lo tanto, una prueba de su teorema.
Piense en ello como en un programa de ordenador:
switch (k) {
case X:
/* do stuff */
break;
case Y:
/* do other stuff */
break;
default:
assert(false, "can't ever happen");
}
El objetivo false = true es la "no puede suceder nunca". Pero no puedes simplemente afirmar tu salida en Coq. De hecho, tienes que poner un término de prueba.
Así que arriba, tienes que demostrar el objetivo absurdo false = true. Y lo único 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 se reduce a falso para cualquier y y, por lo tanto, no puede ser cierto). Entonces usted golpea el objetivo con lo único a su disposición (a saber, H) y su nuevo objetivo es false = andb false c.
Así que aplica una hipótesis absurda tratando de lograr 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 los principios de inducción para la igualdad y la proposición False (en comparación con el 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
Ese principio de inducción para False dice que si me das una prueba de False, me puede darle una prueba de cualquier proposición P.
El principio de inducción para eq es más complicado. Consideremos que se limita 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
Así que si comenzar con alguna proposición P(b) que depende de un valor lógico b, y usted tiene una prueba de P(false), entonces para cualquier otra booleano y que es igual a false, usted tiene una prueba de P(y).
Esto no suena terriblemente excitante, pero podemos aplicarlo a cualquier proposición P que queramos. Y queremos una 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 dice es True -> forall y : bool, false = y -> (if y then False else True).
Así que esto quiere una prueba de True y luego un booleano y que podemos elegir. Así que hagámoslo.
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 das una prueba de false = true, puedo probar cualquier proposición.
De nuevo a andb_true_elim1. Tenemos una hipótesis H que es false = true. Y queremos demostrar 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 desee. Así que, 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 maquinaria que construye el término de la prueba.
Puede intentar usar: ['discriminate'] (http://www.fing.edu.uy/inco/grupos/mf/man/Coq/node.1.2.8.html). (Veo que es una publicación anterior) – guest