Membuktikan tautologi dengan coq

12

Saat ini saya harus belajar Coq dan tidak tahu bagaimana menghadapi or:

Sebagai contoh, sesederhana itu, saya tidak melihat cara membuktikan:

Theorem T0: x \/ ~x.

Saya akan sangat menghargainya, jika seseorang dapat membantu saya.

Untuk referensi saya menggunakan lembar contekan ini .

Juga contoh bukti yang ada dalam pikiran saya: Di sini untuk negasi ganda:

Require Import Classical_Prop.

Parameters x: Prop.

Theorem T7: (~~x) -> x. 
intro H. 
apply NNPP. 
exact H. 
Qed.
logic coq Imago
sumber
NNPPJenisnya adalah forall p:Prop, ~ ~ p -> p., jadi curang untuk menggunakannya untuk membuktikan T7. Ketika Anda mengimpor Classical_PropAnda mendapatkanAxiom classic : forall P:Prop, P \/ ~ P.
Anton Trunov
Jadi, apply classic.selesaikan tujuan Anda T0.
Anton Trunov

Jawaban:

14

Anda tidak dapat membuktikannya dalam Coq "vanilla", karena didasarkan pada logika intuitionistic :

Dari perspektif bukti-teoretis, logika intuitionistic adalah pembatasan logika klasik di mana hukum eliminasi menengah dan ganda yang dikecualikan bukanlah aturan logis yang valid.

Ada beberapa cara Anda bisa menghadapi situasi seperti ini.

  • Kenalkan hukum menengah yang dikecualikan sebagai aksioma:

    Axiom excluded_middle : forall P:Prop, P \/ ~ P.

    Tidak perlu lagi membuktikan apa pun setelah titik ini.

  • Perkenalkan beberapa aksioma yang setara dengan hukum menengah yang dikecualikan dan buktikan kesetaraannya. Ini hanya beberapa contoh.

    • Penghapusan negasi ganda adalah salah satu aksioma seperti:

      Axiom dne : forall P:Prop, ~~P -> P.

    • Hukum Peirce adalah contoh lain:

      Axiom peirce : forall P Q:Prop, ((P -> Q) -> P) -> P.

    • Atau gunakan salah satu hukum De Morgan :

      Axiom de_morgan_and : forall P Q:Prop, ~(~P /\ ~Q) -> P \/ Q.
Anton Trunov
sumber
Terima kasih banyak sejauh ini Saya tidak terbiasa dengan semua yang Anda tulis, tetapi akan memeriksa. Saya menggunakan coqIde dan pada kenyataannya juga mendapat bukti untuk negasi ganda, saya menambahkannya ke deskripsi masalah untuk kejelasan lebih lanjut nanti. Saya berharap ada cara analog untuk masalah yang diberikan di atas. Mungkin saya harus memasukkan satu contoh.
Imago
1
@AntonTrunov Anda perlu menambahkan beberapa tanda kurung ke Axiom peirce: Anda berdiri bukan hukum Peirce (dan sebenarnya trivialuntuk membuktikan).
gallais
@allais Terima kasih telah melihatnya! Tetap.
Anton Trunov
6

Sebagaimana orang lain memberi tahu Anda, tautologi Anda bukan tautologi kecuali Anda menggunakan logika klasik. Tetapi karena Anda melakukan tautologi tentang nilai kebenaran yang dapat ditentukan, Anda dapat menggunakannya boolsebagai ganti Prop. Kemudian tautologi Anda berlaku:

Require Import Bool.

Lemma how_about_bool: forall (p : bool), Is_true (p || negb p).
Proof.
  now intros [|].
Qed.
Andrej Bauer
sumber