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.

— dzień
źródło

Intrygancki. Jestem pewien, że otrzymasz odpowiedź w ciągu kilku minut na liście mailingowej Coq. (Pamiętaj, aby opublikować odpowiedź tutaj, jeśli tak.)

— Dave Clarke

Czy dla tych z nas, którzy są ciekawi, o co chodzi w twoim pytaniu, ale nie znają Coq, możesz dodać zdanie lub dwa wyjaśniające, co to twierdzenie oznacza w języku angielskim? (A może na czym polega „nieistotność dowodu”?)

— Joshua Grochow

@Joshua, nie jestem w stanie wyjaśnić tego szczegółowo, ponieważ jest to również dla mnie nowe, dlatego też zastanawiało mnie to od dłuższego czasu. Ale tak czy inaczej, oto moja próba (patrz w części z pytaniami).

— dzień

@Joshua, IIRC, konstruktywnych matematyce dowód implikacji jak

jest funkcją / procesu / algorytm / konstrukcja, która przekształca odporne od

do dowodu w

, a konstrukcja jest dowodem znaczenia , jeśli uzyskany dowód

nie jest zależny od czego dowodem jest podana dla

A \to B

$A \rightarrow B$

A

$A$

B

$B$

B

$B$

A

$A$

— Kaveh

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.

— Gilles „SO- przestań być zły”
źródło