Formalizar una prueba significa escribir con precisión qué se supone, qué se quiere demostrar y qué regla justifica cada paso. Un asistente puede comprobar una derivación, pero también puede comprobar perfectamente un enunciado que no era el que queríamos. Primero aprenderemos a plantear objetivos y a cerrar sus obligaciones; después revisaremos hipótesis, axiomas y especificaciones con contraejemplos.
Si necesitas repasar:
1. El primer trabajo es decidir qué afirma exactamente el enunciado
El dominio y las convenciones forman parte del problema. Una operación puede significar algo diferente en naturales, enteros o reales. Formalizar exige declarar esos objetos y las condiciones laterales antes de buscar una prueba.
Una conclusión añadida por error como hipótesis puede hacer trivial una tarea mal planteada. Una hipótesis omitida puede volver falso el enunciado. El verificador controla las reglas del enunciado que recibe; la comparación con la intención necesita revisión matemática.
Una resta cambia de significado al cambiar el dominio
Comparar a−b+b=a para a=1 y b=3.
Enteros
En Z, 1−3=−2 y −2+3=1.La identidad general se justifica con inversos aditivos.
Naturales usuales del asistente
Con resta truncada, 1−3=0 y después 0+3=3, que no es uno.
Reparar
Sobre naturales se puede exigir b≤a para recuperar esa identidad. El dominio y la condición evitan pedir una demostración de algo falso.
No se transporta una ley sin revisar la operación utilizada.
Los naturales comienzan en cero y la resta truncada se ha declarado expresamente.
Introducir la conclusión como hipótesis vacía el problema
Se quiere probar que un algoritmo devuelve una lista ordenada.
Especificación débil
Si se supone ya que la salida está ordenada, repetir esa hipótesis prueba una implicación verdadera.
Intención perdida
Eso no muestra que el algoritmo ordene cada entrada. Se ha recibido como dato justamente la propiedad que se debía establecer.
Objetivo útil
Declarar la función y probar, para cada entrada permitida, que su salida cumple las propiedades requeridas, sin asumirlas de antemano.
Una prueba fácil puede señalar un enunciado demasiado débil.
No toda hipótesis fuerte es un error: se compara con el problema que realmente se quería resolver.
2. El contexto conserva las hipótesis y controla su alcance
Γ registra variables, tipos e hipótesis disponibles. Γ⊢p: P significa que p prueba P bajo ese contexto. Al introducir una hipótesis para probar una implicación, al final se descarga como antecedente; no se convierte en una verdad incondicional.
Las variables introducidas dentro de un caso no pueden escapar sin justificar cómo queda cerrado ese caso. Para demostrar un universal se toma una entrada arbitraria, no un valor especial elegido por conveniencia.
Probar P→P conserva la condición de entrada
Objetivo P→P.
Introducir
Suponer h: P. El nuevo objetivo es P.
Cerrar
La hipótesis h tiene precisamente el tipo requerido.
Descargar
Se obtiene la función λh. h, prueba de P→P.No se ha probado P sin hipótesis.
La implicación registra la dependencia que tenía la prueba local.
Si se borra el antecedente P del resultado, se cambia lo demostrado.
Un número elegido no puede hacerse pasar por arbitrario
Se toma n=5 y se prueba n=5.
Caso particular
La reflexividad prueba 5=5.Generalización inválida
No permite concluir ∀n∈N, n=5: cero sería un contraejemplo.Entrada correcta
Para una prueba universal se introduce n sin fijar su valor y se demuestra la propiedad con las hipótesis que valen para cualquier n.
El contexto debe registrar si n era arbitrario o estaba fijado.
Comprobar una cantidad finita de naturales tampoco demuestra por sí sola un universal sobre N.
3. La forma del objetivo indica qué piezas hay que construir
Para P→Q introducimos una evidencia de P y buscamos una de Q. Para P∧Q necesitamos las dos. Para usar una conjunción extraemos componentes; para usar una implicación entregamos su antecedente. Son reglas con entradas y salidas comprobables.
Para demostrar una disyunción basta construir una rama y marcarla. Para usar una disyunción recibida debemos resolver todos sus casos. Una frase como se ve claro no reemplaza una obligación que todavía no se ha cerrado.
Construir una conjunción con las dos hipótesis disponibles
Contexto hP: P y hQ: Q; objetivo P∧Q.
Primer objetivo
La introducción de conjunción pide P; usar hP.
Segundo objetivo
También pide Q; usar hQ.
Reunir
El par de evidencias (hP, hQ) prueba P∧Q. Si solo se cerrara P quedaría la mitad del trabajo.
La prueba final incluye las dos componentes con sus tipos.
La notación matemática del par corresponde al constructor de conjunción del sistema elegido.
Intercambiar una disyunción exige recorrer las dos ramas
Hipótesis h: P∨Q; objetivo Q∨P.
Si h aporta P
Con la evidencia de P, construir la rama derecha de Q∨P.
Si h aporta Q
Con la evidencia de Q, construir la rama izquierda.
Cerrar casos
Ambas ramas terminan en el mismo objetivo Q∨P. El análisis de h cubre todos los constructores de la disyunción.
La prueba no necesita saber de antemano cuál de las ramas se recibió.
Resolver solo el caso P no autoriza a descartar una entrada que aporte Q.
4. Una existencia lleva testigo y una universal conserva entrada arbitraria
Para ∀x: A, P(x) se introduce x arbitrario y se prueba P(x). Para ∃x: A, P(x) se elige un testigo a y se prueba P(a). El orden de cuantificadores determina qué testigo puede depender de qué entrada.
Al usar una existencia en una prueba, se abre un caso con su testigo y su evidencia. Antes de cerrar ese caso, la conclusión final debe tener el alcance anunciado: no se exporta un nombre local como si fuera un valor global conocido.
El testigo puede depender de la entrada del universal
Demostrar ∀n∈N,∃m∈N: m≥n y m es par.
Entrada
Tomar n arbitrario y elegir m=2n.Propiedades
m es par por su forma.
Como n≥0, 2n≥n.Cerrar
El par de propiedades verifica el testigo para cada n. No se eligió un m fijo que sirva a todos los naturales.
La función testigo n↦2n responde a la estructura ∀n∃m.
∃m∀n, m≥n sería falso: dado m, n=m+1 lo supera.
Usar un testigo local sin dejarlo escapar
De h:∃n, P(n), demostrar ∃n, P(n)∨Q(n).
Abrir h
Dentro del caso, llamar a al testigo recibido y hP a su prueba de P(a).
Construir
Elegir ese mismo a para la nueva existencia. La rama izquierda de la disyunción se prueba con hP.
Cerrar
La conclusión es una existencia; el nombre local a queda ligado por el cuantificador. No se concluye que conozcamos un numeral concreto para a.
El testigo se usa dentro de un alcance controlado.
Las reglas de extracción hacia datos pueden variar entre universos como Prop y Type; esta es una eliminación hacia otra proposición.
5. Una igualdad permite sustituir; el cálculo no prueba todas las identidades
La reducción de definiciones puede llevar expresiones diferentes al mismo término y cerrar una igualdad por cálculo. Otras leyes requieren un teorema, una inducción o una hipótesis de igualdad disponible.
En sentido inverso, f(a)=f(b) no permite concluir a=b salvo que se tenga una propiedad adicional, como inyectividad de f.
Reescribir una igualdad conserva la misma función
Contexto h: a=b y f: A→B.
Objetivo
Se quiere f(a)=f(b).Sustituir
Usar h para reemplazar a por b en el lado izquierdo.
El objetivo se transforma en f(b)=f(b).Cerrar
Reflexividad resuelve la igualdad restante. La congruencia de función justifica ese paso.
Se usó una igualdad de entradas como hipótesis.
Si f es constante, las salidas siempre son iguales y no dicen que las entradas lo fueran.
Un caso calculable no demuestra una ley para todas las entradas
Comparar (2+3)²=25 con ∀n,0+n=n.
Caso concreto
El primer enunciado se calcula: 2+3=5 y 5²=25.Definición elegida
Si suma está definida por recursión en el segundo argumento, a+0=a y a+(n+1)=(a+n)+1.
Ley general
Con n variable, 0+n=n no se cierra solo calculando un numeral. Se demuestra por inducción: base 0+0=0; paso 0+(n+1)=(0+n)+1=n+1 usando la hipótesis.
Qué es definicional depende de las definiciones concretas.
Otra orientación de la recursión puede cambiar qué ley necesita prueba; no cambia la matemática que se desea expresar.
6. La inducción exige una base y un paso para un natural arbitrario
Para P(n) sobre naturales desde cero, la inducción ordinaria pide P(0) y, para cada n, una prueba de P(n)→P(n+1). La hipótesis inductiva solo se usa en ese paso local. Base y paso son obligaciones diferentes.
La prueba no consiste en comprobar los primeros valores y adivinar el resto. La regla de inducción garantiza todos los naturales cuando las dos obligaciones generales están demostradas.
Sumar impares construye un cuadrado
S(0)=0 y S(n+1)=S(n)+(2n+1). Probar S(n)=n².
Base
S(0)=0=0².Hipótesis
Tomar n arbitrario y suponer S(n)=n².Entonces S(n+1)=n²+2n+1.Paso
La identidad algebraica n²+2n+1=(n+1)² cierra el paso.La inducción concluye la igualdad para todo n.
La hipótesis sirve para sustituir S(n), no para suponer directamente el caso siguiente.
S(3)=1+3+5=9 verifica un ejemplo, pero la garantía general viene de la inducción.
Un paso verdadero sin base puede sostener una afirmación falsa
P(n) significa n≥1 para naturales que incluyen cero.
Paso
Si n≥1, entonces n+1≥1.La implicación del paso es verdadera para todo n.
Base
P(0) dice 0≥1, que es falso.Conclusión
No se puede aplicar inducción para afirmar P en todos los naturales. El paso no repara la base fallida.
Base y paso se revisan independientemente.
Podría demostrarse P para n≥1 con otra base y otro dominio, pero sería un enunciado distinto.
7. Una definición recursiva debe justificar por qué deja de llamarse
La recursión define objetos mediante valores anteriores. En una lógica de funciones totales se admite cuando las llamadas disminuyen estructuralmente o según una relación bien fundada. Es una obligación distinta de acertar cuando el programa termina.
Una cantidad natural que baja estrictamente no puede bajar para siempre. Al elegirla comprobamos que disminuya en toda llamada, no solo en unos ejemplos favorables. La corrección funcional necesita después sus propios argumentos.
El factorial usa un argumento estructuralmente menor
fact(0)=1; fact(n+1)=(n+1)·fact(n).
Caso base
En cero no hay llamada recursiva.
Disminución
Para la entrada n+1, la llamada usa n. El tamaño natural disminuye.
Calcular
fact(3)=3·fact(2)=3·2·fact(1)=3·2·1·fact(0)=6.La regla de disminución justifica terminar para cualquier entrada.
El cálculo concreto ilustra una terminación demostrada para todos los naturales.
Definir f(n)=f(n) no aporta una disminución ni una construcción total de resultados.
Euclides disminuye aunque cambien dos argumentos
gcd(a, b)=a si b=0; si b>0, llamar gcd(b, a mod b).
Medida
Usar el segundo argumento b. Para b>0, 0≤a mod b<b, así que la medida disminuye.
Traza
(48,18)→(18,12)→(12,6)→(6,0), que devuelve seis.Corrección separada
Escribir a=qb+r muestra que d divide a y b si y solo si divide b y r. Esta equivalencia conserva los divisores comunes y justifica el resultado, además de terminar.
Un mismo desarrollo distingue terminación de corrección matemática.
Si b=0 se resuelve la base antes de pedir el resto; no se usa una división por cero.
8. Las herramientas construyen pruebas y el núcleo comprueba el resultado
La elaboración interpreta notación, tipos implícitos y sobrecargas. Las tácticas ayudan a producir términos de prueba aplicando reglas y lemas. En el diseño usual basado en términos, el núcleo comprueba el término final y su tipo respecto del entorno.
La garantía depende del sistema y sus mecanismos de confianza. Una herramienta externa puede requerir certificados o dependencias especiales. La apariencia de una sesión terminada no sustituye comprobar el enunciado, los axiomas y el artefacto final.
Una secuencia de acciones debe dejar una prueba completa
Objetivo P→(Q→P∧Q).
Introducir entradas
Tomar hP: P y después hQ: Q. Queda el objetivo P∧Q.
Construir componentes
Cerrar P con hP y Q con hQ.
Término final
λhP. λhQ.(hP, hQ) expresa la derivación completa. Cada aplicación de las reglas puede comprobarse con los tipos, sin depender de la forma de escribir las acciones.
El término registra qué evidencia satisface cada obligación.
Esta es notación matemática revisada; no se afirma que se haya compilado un archivo Lean en esta página.
Una táctica fallida no demuestra que el objetivo sea falso
Una búsqueda automática no encuentra una prueba de R.
Resultado observado
La estrategia concreta no construyó la evidencia solicitada con sus recursos actuales.
Otras posibilidades
Podría faltar un lema, otra estrategia podría funcionar o el enunciado podría ser falso. El fallo no distingue por sí solo esos casos.
Para refutar
Se necesita una prueba de ¬R o un contraejemplo adecuado a la forma del enunciado, no solo una búsqueda sin éxito.
Buscar pruebas y verificar una prueba propuesta son tareas distintas.
El problema general de encontrar siempre la respuesta correcta no se resuelve por disponer de un núcleo verificador.
9. Una prueba terminada conserva las dependencias de sus axiomas
Una derivación es relativa a sus definiciones, axiomas y teoremas importados. Un lema importado conserva sus hipótesis: antes de usarlo se comprueba que realmente estén satisfechas y que las definiciones coincidan con las del problema.
En Lean, el marcador sorry deja una dependencia en sorryAx y no cuenta como prueba acabada. El comando #print axioms permite inspeccionar dependencias transitivas. Estas funciones se describen según su documentación oficial; la página no ofrece una sesión local de ese asistente.
Aceptar un axioma falso no lo convierte en un hecho matemático
Se añade una constante hFalse: False a un entorno lógico.
Derivación
El eliminador de falsedad permite obtener cualquier proposición R desde hFalse.
Comprobación relativa
La derivación puede seguir correctamente las reglas porque se le entregó una contradicción como axioma.
Revisión
Eso no establece R en un entorno consistente sin ese axioma. Se debe inspeccionar de qué depende la prueba, no solo que haya sido aceptada.
Comprobar reglas no demuestra por sí solo la consistencia de las hipótesis.
Los principios clásicos habituales no se identifican sin motivo con un axioma contradictorio.
Una dependencia provisional puede llegar por un lema importado
Un resultado A usa un lema B que contiene una prueba pendiente.
Uso local
La demostración escrita de A puede no mostrar ningún hueco visible.
Dependencia indirecta
Si B depende de un marcador axiomático provisional, A hereda esa dependencia al utilizarlo.
Cerrar trabajo
Hay que completar B o sustituir su uso por una derivación válida. Inspeccionar solo la última línea de A no detecta todo el problema.
La revisión de dependencias es transitiva.
La lista de axiomas tampoco verifica que la especificación corresponda al propósito del algoritmo; esa es otra revisión.
10. Los contraejemplos detectan especificaciones que pierden el propósito
Para ordenar listas, estar ordenada no basta: la lista vacía ya lo está. Conservar el conjunto de valores tampoco basta si se pierden repeticiones. Una especificación habitual exige orden respecto de la relación elegida y ser una permutación de la entrada, con todas las multiplicidades.
La corrección funcional no equivale a una cota de tiempo o memoria. Tampoco garantiza sin más el comportamiento de otra implementación compilada. Se declara qué definición y qué propiedades se han formalizado, y cómo se conectan con lo que se ejecuta.
La salida vacía engaña a una propiedad de orden aislada
Entrada [2,2,1]; algoritmo falso devuelve [].
Orden
La salida no tiene una pareja fuera de orden. La propiedad de estar ordenada es verdadera.
Contenido
Se han perdido el uno y las dos apariciones del dos. No es una permutación de la entrada.
Reparación
Exigir ambas propiedades rechaza el algoritmo: [] cumple una parte y falla la otra.
Un contraejemplo pequeño muestra lo que la especificación omitía.
Probar n=n sobre el tamaño o un número ajeno al algoritmo no certifica tampoco la ordenación.
Mismos valores puede ocultar que falta una repetición
Entrada [2,2,1]; salida [1,2].
Orden y soporte
[1,2] está ordenada y su conjunto de valores es {1,2}, igual al de la entrada.
Contar
La entrada tiene dos apariciones de dos; la salida solo una. La multiplicidad no se conservó.
Objetivo correcto
Ser permutación exige conservar cada aparición, además del orden final. La salida [1,2,2] sí supera estas dos comprobaciones en este ejemplo.
Una propiedad puede ser verdadera y todavía no describir el objetivo completo.
Comprobar esta entrada no prueba que una función concreta sea correcta en todas; ayuda a revisar qué habría que demostrar.
Ahora lo resolvemos de principio a fin.
EJEMPLO RESUELTO 1
Dos hipótesis
Demuestra P∧Q a partir de hP:P y hQ:Q.
Contexto
Tenemos hP: P y hQ: Q como hipótesis, con sus tipos explícitos.
Objetivo
Se quiere construir evidencia de P∧Q.
Regla
La introducción de conjunción pide una evidencia de cada componente.
Primera
hP cierra la obligación P.
Segunda
hQ cierra la obligación Q.
Reunir
El par de pruebas (hP, hQ) cumple ambos requisitos y tiene tipo P∧Q, bajo el contexto declarado.
El par de pruebas (hP,hQ).
Las dos componentes coinciden con los dos objetivos.
EJEMPLO RESUELTO 2
Detectar una especificación débil
¿Qué prueba n=n sobre el algoritmo que debería ordenar una lista?
Enunciado
n=n afirma reflexividad de igualdad para el objeto n elegido.
Prueba
Se puede demostrar por reflexividad sin inspeccionar un algoritmo de listas.
Información ausente
El enunciado no relaciona entrada, salida, orden ni conservación de elementos.
Contraejemplo
Un algoritmo que devuelve siempre [] seguiría permitiendo demostrar n=n y fallaría al ordenar conservando datos.
Especificación útil
Pedir que la salida esté ordenada y sea una permutación de la entrada, para cada entrada permitida.
Conclusión
La verdad de n=n no certifica la corrección de la ordenación.La derivación debe demostrar una propiedad que exprese realmente ese comportamiento.
No certifica la corrección de la ordenación.
Una especificación útil exige orden y conservación de elementos.
Los símbolos que hemos usado
- Γ
- Contexto de variables tipadas e hipótesis disponibles.
- Γ ⊢ p:P
- En el contexto Γ, el término p constituye una prueba de P.
- Objetivo
- Proposición que debe demostrarse en el contexto actual.
- Táctica
- Procedimiento que ayuda a construir un término de prueba o transforma objetivos.
- Núcleo
- Componente que comprueba el término final mediante las reglas fundamentales.
- Axioma
- Proposición aceptada en el entorno sin una demostración a partir de las reglas previas.
- Especificación
- Enunciado formal de las propiedades que se pretenden certificar.
- Permutación
- Relación entre listas que conservan exactamente los elementos y sus multiplicidades.
Ahora te toca a ti.
Tienes cinco ejercicios. Inténtalos; las pistas te ayudan si te atascas.
Practicar este tema →