¿Probar la irrelevancia de la prueba en Coq?

¿Hay alguna manera de probar el siguiente teorema en Coq?

Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.

EDITAR : un intento de dar una breve explicación de "qué prueba es irrelevante" (corríjame a alguien si estoy equivocado o es inexacto)

La idea básica es que en el mundo de las proposiciones (o el Proptipo en Coq), lo que realmente le interesa (y debería) es la posibilidad de probar una proposición, no las pruebas de ella, puede haber muchas (o ninguna). En caso de que tenga múltiples pruebas, desde el punto de vista de la demostrabilidad, son iguales en el sentido de que prueban la misma proposición . Entonces su distinción es irrelevante. Esto difiere del punto de vista en la que realmente se preocupan por la distinción de dos términos, por ejemplo, computacional, básicamente, que no quieren que los dos habitantes del booltipo (o Seten palabras de Coq), a saber truey falseel ser igual. Pero si los pones Prop, se tratan igual.

La irrelevancia de la prueba en general no está implícita en la teoría detrás de Coq. Incluso la prueba de irrelevancia para la igualdad no está implícita; es equivalente al axioma K de Streicher . Ambos se pueden agregar como axiomas .

Hay desarrollos en los que es útil razonar sobre objetos de prueba, y la irrelevancia de la prueba hace que esto sea casi imposible. Podría decirse que estos desarrollos deberían tener todos los objetos cuya estructura es importante Set, pero con la teoría básica de Coq, existe la posibilidad.

Hay un importante subcase de irrelevancia de la prueba que siempre se mantiene. El axioma K de Streicher siempre tiene dominios decidibles, es decir, las pruebas de igualdad en conjuntos decidibles son únicas. La prueba general está en el Eqdep_decmódulo en la biblioteca estándar de Coq. Aquí está su teorema como corolario (mi prueba aquí no es necesariamente la más elegante):

Require Bool.
Require Eqdep_dec.
Theorem bool_pirrel : forall (b : bool) (p1 p2 : b = true), p1 = p2.
Proof.
  intros; apply Eqdep_dec.eq_proofs_unicity; intros.
  destruct (Bool.bool_dec x y); tauto.
Qed.

Para este caso especial, aquí hay una prueba directa (inspirada en la prueba general en Eqdep_dec.v). Primero, definimos definimos una prueba canónica de true=b(como es habitual en Coq, es más fácil tener la constante primero). Luego mostramos que cualquier prueba de true=btiene que ser refl_equal true.

Let nu b (p:true = b) : true = b :=
  match Bool.bool_dec true b with
    | left eqxy => eqxy
    | right neqxy => False_ind _ (neqxy p)
  end.
Lemma bool_pcanonical : forall (b : bool) (p : true = b), p = nu b p.
Proof.
  intros. case p. destruct b.
  unfold nu; simpl. reflexivity.
  discriminate p.
Qed.

Si agrega lógica clásica a Coq, obtendrá irrelevancia de prueba. Intuitivamente hablando, la lógica clásica le brinda un oráculo de decisión para las proposiciones, y eso es lo suficientemente bueno para el axioma K. Hay una prueba en el módulo de biblioteca estándar de Coq Classical_Prop.