coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Beginner question: how to prove ~ P \/ P ?

From: Frank Schwidom <schwidom AT gmx.net>
To: coq-club AT inria.fr
Subject: [Coq-Club] Beginner question: how to prove ~ P \/ P ?
Date: Mon, 31 Jul 2023 02:13:19 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=schwidom AT gmx.net; spf=Pass smtp.mailfrom=schwidom AT gmx.net; spf=None smtp.helo=postmaster AT mout.gmx.net
Ironport-data: A9a23:uIZHnqm65O28EAEkWgMIY2vo5gyBIkRdPkR7XQ2eYbSJt1+Wr1Gzt xJKWG+CPf3cNjT2LogiPYuxo0lVsMCDn4dgSFdo+yg1FFtH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajt8B56r8ks156yt42tA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN0yAkwnZq0KvdxlJlB0r vBfcygUVjeM0rfeLLKTEoGAh+wmK9T3eowaqjdmwC2x4fQOG8mZBf+QupkBgXFp16iiHt6GD yYdQSFkbAvBbxpKElgSGNQ4kfvAanzXKmQJ9gvO+vZri4TV5AJ0z6THHNfLQfLJSu9XtEmdu Frr8F2sV3n2M/TGlGbbqyvy7gPVpgvwX5tXH7ml/NZxkViLzyoSDgcXXB21u5GEZlWWXtVCN wob/zpoq6UunKC2cjXjd0G2rW/fngxbYch3Itdh5EbW0rPsxAnMUwDoUQV9QNAhscY3Qxkj2 VmIg87lCFRTXFu9FyP1GlC88mvaBMQFEYMRTXJdE1BUsrEPtKlv0EuVE76PBYbv1oWdJN3m/ 9ydhA4a71n5pfwGyai9913djD+qznQiZlJquF+/so6NyARjeI7tTZah41Hd8Z59wGuxS16co D4LntjY6u0SZX1sqMBvaLRWdF1Kz6zcWNE5vbKJN8d4n9hK0yD6Fb28GBkkeC9U3j8sIFcFm nP7twJL/4N0N3C3d6JxaI/ZI510nPC/SY21Da2ONYImjn1NmOmvo38Giam4gDCFraTQufpiU XtmWZvyVipHVMyLMhLsHLdFidfHORzSNUuKGMyllk35uVZvTCfbEP8ENkeDdOY08OuNr23oH yV3Z6O3J+FkeLSmOEH/qNZNRXhTdCRTLc6s96R/KLXZSiI4QzFJNhMk6elxE2CTt/8Kx7igE 7DUchMw9WcTclWcdljVNy89M+q2NXu9xFpiVRER0Z+T8yBLSe6SAG03LvPbpJF3qbwx/u0+V PQfZcSLD9JGTzmNqXxXboDwoMYmPF6njB6HdXjtKjUuXY9SdyqQ8P/dfyzr6HYvCAizvpAAu LGO7F7QbqcCYAVAN/zoTsyT4Wm/h0VAp9IqbXD0eoFSXG7O7LlVLzfAi65rAsMUdjTG6Dio9 yeXJhY6o+P9rJI/9eeRpKGbrrWGF/l1MVpaElL6s5e3F3j+1UiyzbBQVN2neWjma1r136G5d MNpz/3YG98WrmZg6oZTPe5i8vMj2oHJubRf8DVBIFzKSFaaUpVbPXiM2Jh0hJ1nn7N2l1O/Z ROSx4N8J76MBcLCFWwRLioDasCo96kduhvW3MQPDHTK3g1F15vZbhwKJDiJsjJXE5VtOoB8w esBht8f2zbitjUUaOS5ngJm3EXSCExYSKg2lIAoMKmygCoR91xyS5j9CCj33ZKxV+txInQae j+6uIeShpB35FbzTH4oJH2cgctfncsvvT5J/n8jJnOIuMbP3cFv+Bhd7TkcExln/ixG98lRO WFbEVJ/CovT3jVvhelFB3uNHSMYDjKn20XB8Xk7v0yHcFuNSUrMM3wbBeaB2Gs74lBsVGFX0 5/AwVm0TAuwWt/62xUDfHJMqtvhfIRXzRLDksX2JPa1NcA2ThS9i5D/eFdSjQXsBP4wo0j1p eNK2uJUQo+jPA4yp5wLMaWr5Y4yejulelMbGepA+ZkXF17yYDuxgDiCC36gc/N3esDlzxWKN NxMFOluCTKOjD2DvxIKN54qerVUpsMk1PAGW7HsJFMFjYehkypUgMrQ2xX61UAWQIRIsMciK 4nuWSqIPU6OiFB1xWLcjsl2FVCpQNsDZT+mhbyR9bgNG7kiq8BpS1k5iZGvjkWWMSxm3hOah xzCbKno1N5fyZxgso/vM6dbDSC2FI/Db/uJ+wWNrNh+V9PDHsPQvQczqFO8HQBpEZYOetZwz 5KhjcXW2R7bgbMITGzpoZmNOK1X78GUXuAMEMbWLmFfrBSSSv3X/BoP1GCpG6NnyOoHyJGce DK5T8+sefo+edRXniRVYhcDNSctMf38a6O4qB6tq/iJNAMm7jXGC9GZpE/ZNTQRMmdCPpDlE Qb7tsq//t0S/swGGBYAAOogGJNiZkPqXaw9bdDqqD2EFS+Sj0ifvqf53w8Vgd0R5qJozO6hi X4EevT/SPh2kKTP0c0fvIli+BsaEB6RRAX2kl01o7ZLZ/KSVQbq7tjx9b0JD4ESlCHuvH09T C+Yd3MsUE0RQhwdGSgRI73fssO3CekefNH0OlTFOq9ShzieXOu9PVeqysusD7qatNcuICFL5 OzyIkHNAyU=
Ironport-hdrordr: A9a23:9qLF1qjpmTicsc76lWyGtEUODXBQXv4ji2hC6mlwRA09TyW9rb HLoB19726OtN9xYgBEpTnkAsK9qBznmqKdjbN+AV7AZniFhILLFvAA0WKK+VSJdkHDH4VmtZ uIHZIeNPTNLRxdkdvw5hW+Hu0t2d+d7cmT9J/jJjtWPGZXg7oL1XYeNu93KDwOeOHMaKBSKK ah
Ironport-phdr: A9a23:nFUmHB9wHifjB/9uWfy3ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Y gqAv7421RfgZsby07p8ke3YsqTtCyQrwK2qlzQ8SqFKTAIPks4MngYtU4avAEz/K+P2PWRhR JwRHFBq8GumPkdLBc3we0PdomGo7T4VBx7zKRd5Kv76F4LMjsm7zeK/94PcbwhGmTa2fK9/I gixoQjNrMcdnJFsKrw2yhvHo3tIf/pZyGZ1Ll+NnBjy+9m98od7/ytfp/wu+chAUb7nf6sjV rxXEC4mM2Eu68L1sxTIUBaC6WEdUmUSlRpIHhTF4RTnVZr/rif2quxw0zScMMbrT747RC6i4 r9lRhHolikJKj03/27LhcNtgq1VrwmspwBmw4POfI2ZKPRzcr3bcNgHRWRBRMFRVylZD428d YsAFewBPeVFpIfgu1QOrRW/BQixC+Pozz9Dm3j73bYm3OQhHwDG3REvH9ULsHnPo9X1MagTX fqzzKbW0TXOdvVb0iry54bUaB4uu+2MXa5ufsrLz0kiDwPLgFWNpYHmMT2b2eQAvmyF4udvS ++jlW8qpgFtrjav2sohl4nEipwUx13A6Sl0zoY4KcGmREN0fdKpE59duj2cOoBrQc0iW3llt DgnxrEYo5K3YjYGxZY9yxLCa/GLaZWE7xb7WOuSJTp0nm9pdbKlixqs/0WtyPfwWtSp3FpWq CdOj8PCuWoX1xPJ78iKUvt98Vml2TaIzw3T7+ZEIV0olabBJJ4hx7ExmoAVsUvdAi/6gET2j KmIeUU44uWk9fnrbqv8qpOCKYN5iBvyPrkul8ClHOg1NhACX22B9uS90L3j81f5QLJPjvAui anWrJDaJMoapqGkBA9V150u6xm6DzapytgYm2cILE5ddBKBlIfmI0vOL+zgDfejn1Ssly9my +3eMr37HprNNmTDkKvmfbtl90FczxMzwclD6JJQF7EOO+n+WlTxtdzdFh82KRa4w+fhCNVn1 4MRQ3iDAqGDMPCajVjd7eU2ZuKIeYU9uTDnKvFj6eS9o2U+nAozZ6Cv3tMsY3CnH/hhJg3Ne nHsndYNFmIisQ8uCurnlAvRAnZoe3+uUvdktXkAA4W8ANKbLmjMqLmI3SPhW4ZTengDEFeHV 3Hha4SDXf4ILiOUOM5o1DIeBvC6U4F08xaouUfhzqZ/aPLO83gDvpL81dRy4sXckAF08zFoX IyGy2/Yd2hvhSsTQiMumqV2oEhz0FCGhLNzg+NZGdtWz/xMQkE8OIKPh/diBYXUXQTMNsyMV E7gQtiiBmQpScktxtYVf0tnM9ClkwyF0C+6RbkYi9RnHbQS9aTRlzj0Lsd5kTPd0bU5ykMhS Y1JPHGngah2807SAZTImgOXjfTic6NUxyPL+GqZqAjG9EhFTA59V7nEVnEDdwPXq9r+/EbLU 76pD/wuLAJAzceILqYCZMfuiB1KQ/LqOdKWZGzU+S/4Hh2I2bKAa4/CdGANmiPQFAlMkgwe+ 2qHKRlrHj2o8CrVCD1jE06qYlu5q7Ak7inhEQltkkfTPh4EtfL94BMeiP2CRulG27sFvH1ks DBoBBOn2NmQDdOcpg1ndaEaYNUn4V4B23iK0m41dpGmMa1mgUYTNgptuEa7nQ58CppBnc8vh Hwv3Ex0JL7SgzYjP3uImIv9PLHaMDy45xuvdK/a3VT239OGvKEC9L5r40WmtwavGE049nxh2 NQAyHqQ6KLBCw8KWI7wWEI6n/Rjj4nTeTJ1p4bd1Hk2dLKxrieHwdUiQu0s1hened5bdqKCD g77VcMAVYCiL+kjml7haRxhXqga76U0IMKqcP6u16u7euBtgHqqgH9G74Z0zk+Xv3AlEKiSh clDmqzeh1rPXiy0lFq7t8HrhY1IAFNaVnGyzyTpHs8ZZ6F/e5oKFXb7JsS2wttkgJu+E3Vc9 VOlGxYHwJrzIEDUNQaim1QNkx1G8hnF0WOiwjd5ki8ktP+a1S3KmaH5cQYff3RMTy9khEvtJ o69i5YbWlKpZk4njkjAhw6yyq5FqaB4N2SWT11Pen28NGpiTaq8sb+qbMtfrpUlrW8ENYb0K UDfUbP7rxYAhmn4FGtBxTw8chmlv4W/mRFmwjHVPDN4q3zXftt1zBHU6YnHRPJf6TEBQTFxl TjdAlXvWrvhtcXRjZrItfqyEn6wTpAGOze+1puO7WHorX0vGxC0mOq/38HqARRvmzGuzMFkD ECq5F79etW5jf3hd7s5Iw82WBmkrJAhUoBmztlv2NdKgShc29PLoT1dzy/yKYkJg/ukKiBXG nhSmYCTuVK1nxc+SxDBj4PhCifHm5EnPYPlJDpLnHp6tZ0CCb/IvuYdx20v+AX+9F2XOb8nw X8c0ad8tyJc2blZ/lZrl3THRepMeCsQdS30y0bYtZbn8vgRPTv+N+D3jhY2nMj9Xuvb/UcDA jCjIshkRWgqsY1+KA6egCe1s9+5PoOKPJRI73j221/Bl7QHeMh3z6RXw3A8YSSn5DUzwuo/x 3SCxLmcu46KYyVo9aO9WFtDMyHtItkU8XfrhLpfmcCf28auGI9gE3MFRsmgS/XgCz8Uufn9U mTGWDQhtneWH6beFg6D+Q9nqXzICZWiK3CQIjEQ09xjQBCXIEEXjhoTWX02mZswFwbiw8KEE g8x/jcK+lvxsQdB0MptMATjFGjatEGuZyt1AJmTIRxK7x1TskfYNcvNi4A7Vypc/5CnsEmMM jnBPl4OVztWHBXZQQmybdzMrZHa/uOVB/SzNa7LaLSK86lFUuuQgIio2c1g9iqNMcOGOj9jC ec60wxNRyMceYyRljMRRigQjy+IYdScoUL24SZ3scGz9/HDVwf/o42CF/EBVLcnswDzmqqFO +OK0WxhLi1E05oX2XLS4L0YwUJUhCR+MT+gDf5T0EyFBLKVkahRARkBbip1P8Yd9KMw0D5GP svDg8/03Lp15hbQI1hARRrnl937PaTiwkm4M07bQkmOJPKAKCGZm6kfjouzTK0WiuhI5UTYh A==
Ironport-sdr: 64c6fffc_mdjJZvzW6eUvjsl8vORSEqSLysTiw/bLfojNgu9LodGV96z BKluDTfqdrwGbUBK+irQKAiG6gmiLuTWrlXldSw==
Ui-outboundreport: notjunk:1;M01:P0:aYkXqJu+4Tw=;ozZ3vgLhQyTTMegsk6TWyGUau/u U2TsGCkTpcWuAP6kuh8RSoQvOz9GyPt+lFdBxeyUpQKifJ9+cpUDlgl3QVf2XSWUKHw6nNV7F U8OmF5LeR6JI1Q6SzrIGeLvoe2cMs+LLBiHxOa93Tn0Mku9rpriTvh42JD0hRKC3Z4epBro6m bWRM4VZmGrc8lybhaMEJF/xTykMWH8QFSaX43jbANxDQfPkEtR8uXiH86P5jLcvTDH/9zqz97 spdcBkpu5seLwxfkN6am54Si9ZJU/GKRqa5diBKiUXWTaCPolq/A+MW8kEffC9ZmC93pquxbF c/4oQsWHRlbdKq4QaWKVVBcx7tK3kaqEWGCrygyPGfq7kFTjB7UWlNhhr7Yzkb8N1NnhmRmfd DV23IyGjr2c7iV4eJN8OQa/v+S6q2K4BKvhjZGg2fzfdvyGrRB84qG7hEmrXloq2HgMSVGGcT G7CqRNV2RFx23s+j5Kg5BgJiQfcm0q1IT8yG8LnspC61HXBCPyrEY4bOtVHqT740dI6/8E270 HseLQTOIBfmNWb7yFVi2qv2qi0HpCqjdkljwDO1VAF08RilUUGy4lDh/eTGFL+KGudgiJPry8 7Y6pIqYCStyw7oMNc2YzsAiq0Rj6rjYWuPJ23oLSUJg16UdEnvzAE/Ky4DmMJ37exVP7EFQXx EaQSCsAgUd59OTHCVjTQBz+sL60Nj4+kSD9nHcUIqbKWu3hCvOygK/GVHvnPzcmvX51+ANPNL KITTc6B47THI25PePvtZZbLg4ZGbWJfYn5g5wH1EYfaTR4V46L2/KtaIXuj4Tg6XXez/DHHiy vokg1t4NVOj1lArWWNghS4NlwTvitnroxSiE6QgoLNAjeDiegFCjwwe2f/JmaN82gl1fgei6t lskR+FdpNHt9Stwcp+sTSJYXn97FsDY0l7yCK/anz+DC70lWILbEKWYa/yrJlbY3nGkp4neSK ZfbEBg==

Hi,

I found out I can prove

(ins)Coq < Goal forall P : Prop, ~ ( ~ P /\ P ).
1 subgoal

============================
forall P : Prop, ~ (~ P /\ P)

(ins)Unnamed_thm < intro.
1 subgoal

P : Prop
============================
~ (~ P /\ P)

(ins)Unnamed_thm < intro.
1 subgoal

P : Prop
H : ~ P /\ P
============================
False

(ins)Unnamed_thm < destruct H.
1 subgoal

P : Prop
H : ~ P
H0 : P
============================
False

(ins)Unnamed_thm < auto.
No more subgoals.

(ins)Unnamed_thm < Qed.
Unnamed_thm is defined

But here I don't know what auto does. How can I figure out the operations of
auto?

And for ~P \/ P I need this import.

(ins)Coq < Require Import Classical.

(ins)Coq < Goal forall P : Prop, ~P \/ P.
1 subgoal

============================
forall P : Prop, ~ P \/ P

(ins)Unnamed_thm0 < intros.
1 subgoal

P : Prop
============================
~ P \/ P

(ins)Unnamed_thm0 < elim (classic P).
2 subgoals

P : Prop
============================
P -> ~ P \/ P

subgoal 2 is:
~ P -> ~ P \/ P

(ins)Unnamed_thm0 < auto.
1 subgoal

P : Prop
============================
~ P -> ~ P \/ P

(ins)Unnamed_thm0 < elim (classic P).
2 subgoals

P : Prop
============================
P -> ~ P -> ~ P \/ P

subgoal 2 is:
~ P -> ~ P -> ~ P \/ P

(ins)Unnamed_thm0 < auto.
1 subgoal

P : Prop
============================
~ P -> ~ P -> ~ P \/ P

(ins)Unnamed_thm0 < auto.
No more subgoals.

(ins)Unnamed_thm0 < Qed.
Unnamed_thm0 is defined

Here I also don't know what auto does. And it seems to be that this Axiom
"classic"
which is defined under /usr/lib/coq/theories/Logic/Classical_Prop.v
is itself unproven.

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

And it is not used by auto.

How can I figure out the operations of auto?

And is there a way to proof ~ P \/ P without this "Classical" library?

I guess it is possible to proof the same logical formulae easier when I use
the bool datatype.

(ins)Coq < Goal forall b : bool , true = (orb (negb b) b).
1 subgoal

============================
forall b : bool, true = negb b || b

(ins)Unnamed_thm < intro.
1 subgoal

b : bool
============================
true = negb b || b

(ins)Unnamed_thm < destruct b;compute;reflexivity.
No more subgoals.

(ins)Unnamed_thm < Qed.
Unnamed_thm is defined

Why is the prop datatype not fully defined in this sense?

Does the Term ~P \/ P do not appear in proofs?

Regards,
Frank

[Coq-Club] Beginner question: how to prove ~ P \/ P ?, Frank Schwidom, 07/31/2023
- Re: [Coq-Club] Beginner question: how to prove ~ P \/ P ?, Agnishom Chattopadhyay, 07/31/2023