Udowodnić nieistotność dowodu w Coq?

Czy istnieje sposób na udowodnienie następującego twierdzenia w Coq?

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

EDYCJA : Próba krótkiego wyjaśnienia „czym jest nieistotność dowodu” (popraw mnie, jeśli się mylę lub nieścisłość)

Podstawowym założeniem jest to, że w świecie propozycja (lub Proprodzaju w Coq), co (i powinny) troszczą się o to niedowodliwość z propozycją, nie dowody tego, że może być wiele (lub brak). Jeśli masz wiele dowodów, z punktu widzenia sprawdzalności są one równe w tym sensie, że dowodzą tej samej propozycji . Zatem ich rozróżnienie jest po prostu nieistotne. Różni się to od obliczeniowego punktu widzenia, w którym naprawdę zależy ci na rozróżnieniu dwóch terminów, np. Zasadniczo nie chcesz, aby dwaj mieszkańcy tego booltypu (lub Setsłowami Coq), a mianowicie truei falsebyli równi. Ale jeśli je włożysz Prop, będą traktowane równo.

Teoria leżąca u podstaw Coq nie sugeruje dowodu na brak znaczenia w ogóle. Nie sugeruje się nawet dowodu nieistotności dla równości; jest to równoważne z aksjomatowi K Streichera . Oba można dodać jako aksjomaty .

Istnieją udoskonalenia, w których warto uzasadniać obiekty dowodowe, a nieistotność dowodu sprawia, że ​​jest to prawie niemożliwe. Prawdopodobnie w tych zmianach powinny zostać przekształcone wszystkie obiekty, których struktura ma znaczenie Set, ale przy podstawowej teorii Coq istnieje taka możliwość.

Istnieje ważna podgrupa nieistotności dowodów, która zawsze obowiązuje. Aksjomat K Streichera zawsze dotyczy domen rozstrzygalnych, tzn. Dowody równości zbiorów rozstrzygalnych są unikalne. Ogólny dowód znajduje się w Eqdep_decmodule w standardowej bibliotece Coq. Oto twoje twierdzenie jako następstwo (mój dowód tutaj niekoniecznie jest najbardziej elegancki):

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.

W tym specjalnym przypadku oto bezpośredni dowód (zainspirowany ogólnym dowodem w Eqdep_dec.v). Po pierwsze, zdefiniuj definiujemy kanoniczny dowód true=b(jak zwykle w Coq, łatwiej jest mieć stałą na początku). Następnie pokazujemy, że każdy dowód true=bmusi być 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.

Jeśli dodasz klasyczną logikę do Coq, otrzymasz dowód nieistotności. Intuicyjnie mówiąc, klasyczna logika daje wyrocznię decyzyjną dla propozycji, co jest wystarczające dla aksjomatu K. W standardowym module bibliotecznym Coq znajduje się dowód Classical_Prop.