Prove a irrelevância da prova no Coq?

Existe uma maneira de provar o seguinte teorema em Coq?

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

EDIT : Uma tentativa de dar uma breve explicação sobre "o que é irrelevância para a prova" (corrija-me alguém se eu estiver errado ou impreciso)

A idéia básica é que, no mundo das proposições (ou do Proptipo Coq), o que você (e você deveria) realmente se importa é a provabilidade de uma proposição, não as provas dela, pode haver muitas (ou nenhuma). Caso você tenha várias provas, do ponto de vista da provabilidade, elas são iguais no sentido em que provam a mesma proposição . Portanto, a distinção deles é irrelevante. Isso difere do ponto de vista computacional, onde você realmente se preocupam com a distinção de dois termos, por exemplo, basicamente, você não quer que os dois habitantes do booltipo (ou Set, nas palavras de Coq), ou seja, truee falsepara ser igual. Mas se você os colocar Prop, eles serão tratados da mesma forma.

A irrelevância da prova em geral não está implícita na teoria por trás da Coq. Mesmo a irrelevância da prova para a igualdade não está implícita; é equivalente ao axioma K de Streicher . Ambos podem ser adicionados como axiomas .

Existem desenvolvimentos em que é útil raciocinar sobre objetos de prova, e a irrelevância da prova torna isso quase impossível. Pode-se argumentar que esses desenvolvimentos deveriam ter todos os objetos cuja estrutura é importante Set, mas com a teoria básica de Coq a possibilidade existe.

Há uma subcasa importante da irrelevância da prova que sempre é válida. O axioma K de Streicher sempre se aplica a domínios decidíveis, ou seja, as provas de igualdade em conjuntos decidíveis são únicas. A prova geral está no Eqdep_decmódulo da biblioteca padrão da Coq. Aqui está o seu teorema como corolário (minha prova aqui não é necessariamente a mais 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, aqui está uma prova direta (inspirada na prova geral em Eqdep_dec.v). Primeiro, defina que definimos uma prova canônica true=b(como de costume no Coq, é mais fácil ter a constante primeiro). Então mostramos que qualquer prova disso true=bprecisa 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.

Se você adicionar lógica clássica ao Coq, terá irrelevância à prova. Intuitivamente falando, a lógica clássica fornece um oráculo de decisão para proposições, e isso é bom o suficiente para o axioma K. Há uma prova no módulo de biblioteca padrão da Coq Classical_Prop.