Buktikan bukti tidak relevan dalam Coq?

Apakah ada cara untuk membuktikan teorema berikut dalam Coq?

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

EDIT : Upaya memberikan penjelasan singkat untuk "apa bukti tidak relevan" (koreksi saya seseorang jika saya salah atau tidak akurat)

Gagasan dasarnya adalah bahwa dalam dunia proposisi (atau Propsemacamnya dalam Coq), yang benar-benar Anda (dan Anda harus) pedulikan adalah provabilitas proposisi, bukan buktinya, mungkin ada banyak (atau tidak ada). Jika Anda memiliki banyak bukti, dari sudut pandang provabilitas, mereka sama dalam arti bahwa mereka membuktikan proposisi yang sama . Jadi perbedaan mereka tidak relevan. Ini berbeda dari sudut pandang komputasi di mana Anda benar-benar peduli tentang perbedaan dua istilah, misalnya, pada dasarnya, Anda tidak ingin dua penghuni booljenis (atau Setdalam kata-kata Coq), yaitu truedan falsemenjadi sama. Tetapi jika Anda memasukkannya Prop, mereka diperlakukan sama.

lo.logic type-theory proof-assistants coq hari
sumber

Menarik. Saya yakin Anda akan mendapatkan jawaban dalam hitungan menit di milis Coq. (Pastikan untuk mengirim tanggapan di sini, jika Anda melakukannya.)

Dave Clarke

Bagi kita yang ingin tahu tentang pertanyaan Anda, tetapi tidak terbiasa dengan Coq, dapatkah Anda menambahkan satu atau dua kalimat yang menjelaskan apa arti teorema dalam bahasa Inggris? (Dan mungkin "bukti tidak relevan" tentang apa?)

Joshua Grochow

@ Yosua, saya tidak cukup untuk menjelaskannya secara terperinci, karena ini juga baru bagi saya, itu juga mengapa hal itu membingungkan saya untuk beberapa waktu. Tapi bagaimanapun, inilah usaha saya (lihat di bagian pertanyaan).

hari

@Joshua, IIRC, dalam matematika konstruktif, bukti dari suatu implikasi seperti

adalah fungsi / proses / algoritma / konstruksi yang mengubah suatu bukti dari

ke bukti dari

, dan konstruksi adalah bukti tidak relevan jika bukti yang dihasilkan dari

tidak tergantung pada yang bukti diberikan untuk

A \to B

$A \rightarrow B$

A

$A$

B

$B$

B

$B$

A

$A$

Kaveh

Jawaban:

Bukti tidak relevan secara umum tidak tersirat oleh teori di balik Coq. Bahkan bukti yang tidak relevan untuk kesetaraan tidak tersirat; itu setara dengan Streicher ini aksioma K . Keduanya bisa ditambahkan sebagai aksioma .

Ada perkembangan di mana berguna untuk alasan tentang objek bukti, dan bukti tidak relevan membuat ini hampir mustahil. Bisa dibilang perkembangan ini harus memiliki semua objek yang strukturnya disusun kembali Set, tetapi dengan teori Coq dasar kemungkinan ada di sana.

Ada subkumpulan bukti penting yang tidak relevan yang selalu berlaku. Aksioma Streicher K selalu berpegang pada domain yang dapat didekati, yaitu bukti kesetaraan pada set yang dapat ditentukan adalah unik. Bukti umum ada di Eqdep_decmodul di perpustakaan standar Coq. Inilah teorema Anda sebagai akibat wajar (bukti saya di sini belum tentu paling elegan):

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.

Untuk kasus khusus ini, inilah bukti langsung (terinspirasi oleh bukti umum Eqdep_dec.v). Pertama, definisikan kita mendefinisikan bukti kanonik true=b(seperti biasa dalam Coq, lebih mudah untuk memiliki konstanta pertama). Kemudian kami menunjukkan bahwa setiap bukti true=bharus 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.

Jika Anda menambahkan logika klasik ke Coq, Anda mendapatkan bukti yang tidak relevan. Secara intuitif, logika klasik memberi Anda oracle keputusan untuk proposisi, dan itu cukup baik untuk aksioma K. Ada bukti dalam modul perpustakaan standar Coq Classical_Prop.

Gilles 'SANGAT berhenti menjadi jahat'
sumber