¿Por qué no se puede probar UIP en Coq? ¿Por qué la construcción de coincidencia generaliza tipos?
UIP (y equivalentes como el axioma K) debe ser añadido axiomáticamente en Coq si se desea:
uip : ∀ A (x y: A) (p q: x = y), p = q
Esto es sorprendente, ya que parece obvio a partir de la definición de igualdad, que solo tiene un constructor. (Esto, por supuesto, se basa en la interpretación de que una definición inductiva en Coq captura todos los elementos de su tipo).
Cuando uno intenta demostrar UIP, se queda atascado en el subcaso reflexivo:
uip_refl : ∀ A (x: A) (h: x = x), h = eq_refl x
Podríamos esperar que el siguiente término sea un término de prueba apropiado:
fun A (x: A) (h: x = x) =>
match h as h0 in (_ = a) return (h0 = eq_refl x) with
| eq_refl _ => eq_refl (eq_refl x)
end
Esto falla porque está mal tipado. Sabemos que h: x = x, pero cuando hacemos coincidir el término, perdemos la información de reflexividad y se generaliza a h0: x = a. Como resultado, nuestro tipo de retorno h0 = eq_refl x está mal tipado.
¿Por qué es que el constructo de coincidencia generaliza nuestro tipo aquí? ¿Sería posible una alternativa no generalizadora?
davy.ai
La construcción de coincidencia generaliza nuestro tipo aquí porque utiliza el razonamiento inductivo para la igualdad, lo que puede llevar a diferentes tipos de pruebas para casos diferentes. En otras palabras, cuando hacemos coincidir con h, lo tratamos como una prueba arbitraria de x = a, en lugar de simplemente como reflexividad.
Una alternativa que no generaliza sería manejable. Un enfoque sería utilizar coincidencia de patrones dependiente, lo que nos permite refinar el tipo de la variable que se hace coincidir con base en la forma del patrón. En este caso, podríamos hacer coincidir con h con el patrón
(eq_refl _), que devuelve explícitamente solo el caso de reflexividad. Esto evitaría la generalización de nuestro tipo y nos permitiría construir un término de prueba apropiado.