coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Beginner question: how to prove ~ P \/ P ?
Date: Mon, 31 Jul 2023 09:38:28 +0900
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-data: A9a23:gNDWR6g1FLR4NB7+BcNIRytaX161NhQKZh0ujC45NGQN5FlHY01je htvXWzVPayJMWOnLYsjO4nj90oFu8Xdxt9nTAZrrC8xQX9jpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UqieUsxIbVcMYD87jh5+kPIOjIdtgNyoayuAo tqaT/f3YTdJ4BYqdDpNg06/gEk35q+q52hA5gZWic1j5TcyqVFFVPrzGonqdxMUcqEMdsamS uDKyq2O/2+x13/B3fv4+lpTWhRiro/6ZWBiuFIOM0SRqkQqShgJ70oOHKF0hXG7JNm+t4sZJ N1l7fRcQOqyV0HGsLx1vxJwS0mSMUDakVNuzLfWXcG7liX7n3XQL/pGHn9oZolfwsdLAVpn2 dIKLG5UdAqqiLfjqF67YrEEasULKcDqOMUUv3AmxDqfDPBOrZLrGv+Ro4EDmm1o3YYURKy2i 8kxMVKDaDzJbBtOIVcQDbo1mebuj3K5cjswRFe9+/BpvjSMk1AZPL7FPtb2Xdmjf8Rsx1+Jv V3+7mnVOEkjK4nKodaC2inw27eXwnyTtJgpPLa/77thhECZ7ncCDQUfE1q9u/iwzECkM++zM GQR8ysq66M39QqiRZ/8WXVUvUJooDYOZYQLF6oCyT2N8YP4zRSdWDEeVBdOPYlOWNANeRQm0 VqAntXMDDNpsaGIRX/1yop4vQ9eKgBPdD5TOnNsoR8tvIi7+Nhr5v7aZo87SPbdszHjJd3n6 xGsxBXSap0WhM8Pka6+/BbOiHStoPAlrzLZBC2LAQpJDSsjPeZJgrBED3CBs56sy67DEDG8U IAswZT20Qz3JcjleNaxaOsMBqq1wP2OLSfRh1Vid7F4qWX1pCL6LdsNv24lTKuMDiriUWK4C KM0kV4AjKK/wFPwBUOKS9vtWpt0lfCI+SrNDamPP4QmjmdNmP+vp30zPRbPgAgBYWAylq02N 5CdfI6tAXsTYZmLPxLrL9rxJYQDn3hkrUuKHMCT8vhS+ebGDJJjYetfYQTmgyFQxP/snTg5B P4EaJbVlkoBC7SnCsQVmKZKRW03wbEALcieg6RqmiSre2KKwUlxVaGD8qBrYIF/gaVem8HB+ 3z3CAcSy0PyiTeDYU+GY2xqIuGnF5tuj2MJDQp1N3aR2l8nfdmO6oUbfMAJZrUJzrFo4sN1a PgnQP++JMpzZA7JwBkjSKXsjZdDcU2rjD2ePiD+bzkYeYVhdjPz+dTlX1XO8XAOBxWoqPpk+ qWE0y3ZZZ8HWiVjE8fkR/a9xHyhvXUmubxTXmmZBvJxaUnT4IxRBCiptcAOIuYIMgfm6gKB8 gSrXScjuujGprEq/Onzhayrq5mjF818FBF4G1b3wKmXNy6A2Eae2q5FDfi1eA7CWFPO+KmNY ftfy9f+OqYlmHdIq49NLKZ5/5kh5tfAp65o8So8JS/lN2+UM7JHJmWK+eJttacXn79QhlaQa 3K1o9JfPe2EBdPhHFsvPzEaV+Wk189FvhnJ7P8wHlf22z8vwpqDTndpHketjA5zEeJLFb0Lk MkdvPwY0QidsiYRE82ni3lU/lucL3ZbXKQAsIobMbDRiQEq6w9jZLrAAxSr4KCeNs1GM2gxA zqunKGZra9t9knDVHsSFHb2wutWg6oVii1K1FMvI1eomMLPo/0KgC1q7jU8SzpKwiV90+5cP nZhM2t3L/6s+whEqddiXWf2PS18Hzycp1LMzmUWmF3jT0WHUnLHKEs/M72v+GEb62dtQShJz oqHyWrKUSfYQ++p53EcAXVakv3EScB90ibgm8r9RsSMIMQcUArf26SrYTIFlgvjDcYPn3b4n OhN/tghTY3gNCUVnb83NJnC65QUVyK/BTJjRdNPwfo3OF/yKRCI9xqAEUSTQv92Bufr9Ba4A vN+J8gUWBWZ0j2Pnw8hBqUNAuFVmdg17eFfeoL6eHYMspqEjz9TqJmL3DPPtGwqZNRPkMgGN YLacQyZIFGQnXd5n2zsrtFOH2iFPek/ewz32d6q/NUzF54stP9mdWcw2OCWu0q5HRRG/RXOm i/+fI7TkvJfzLpzk7vWEqlsAxu+LfXxXr+q9CGxq9F/UsPdA/zRtg86qkjVACoOBOE/A+9Ir LWqtML7+Gjnv7xsCmDQpMSnJplzvM63WLJaD9LzIHxkhhC9Yc7L4SVSy1DgfNYN2JlY69K8T gS1VNqoeJRHE51BzXlScG5FHwxbF63zabz6qDigq+iXTCIQyhHDMMjt4EqBgbu3rcPUE8aW5 s7IV/eSChRwqY1NAFkPAvAgCpQ+IVmLtW7KsTHunWHwM4VqqgrqVnjeed4I4jTKTHCPVsf8i X4Abgarbwy84ckk0/kA27GffXQr4LJViuwxOEsWvd9w49x/4KjqMsxFWag75lpofuAeGX02i PwhrIfvNMklYQl5TA==
Ironport-hdrordr: A9a23:GD406a4HtAntrDbyyAPXwOzXdLJyesId70hD6qkRc20vTiX2rb HLoB12726QtN9VYgBDpTniAsm9qBHnhPhICOAqVN/INmSLhILrFvAA0WKI+UyYJ8SRzJ8k6U 6iScdDIey1I1xzjcO/xhK5HdYmyNzC1Kyzn+/RwzNMYGhRGsZdBstCZDpz23cWeDV7
Ironport-phdr: A9a23:1YyEkROX3h0YhZcVYZMl6nbpBhdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv6sr0wWCBtiTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnA JYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yeG/94fRbglWizawb7N/J wiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjU LxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4 LpxSBLwhygHOTw2/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kc 4YPAOwBPedDr4n9oFsOqAa1CBesBOz11j9Imnj23bUg3Os8EQHH3BYvHtITu3nTttr1O6ESU eGuzKnIyjXDauhb1iv46IjJaBwuu+2DUahxccrX0EQiER7OgVqMp4L/JTyVyvgNvHaB7+pmT e+iiW8qpxx+rDWg2sogl4vEi4YIxl3L+yh0z4k7KcO6RUJnYtOpEZ9duSGVOoV2Rs4vTH9kt SQkxrACpJO2YCsHxZI6zBDRbPyHdpKH4hPlVOuJLzZ4hXFleLOnhxms7Eegy/fzWtOz0FZQo SpJisTMtmgT2BzV7MiLUOVy8Vq82TqX1gDT7PtEIUEumqbBJZ4h2Lg9nYcQv0TbBiL6hVv6g aGMekgl9OWk8frrbqnoq5OGKYN4lx/yPrwwlsCjBek0KAsDUmiB9eiiybHu/Ff1TbVXgvAwj 6LXqorVJd4Bqa68GwJV0pgs6xK4Dzq+1dQXh3gHLFZfdB2biojpOkvCL+rkAvulglSsli9nx /HAPrL/HpXANmXPnKnvcLpn6kNRxhA/wc5D659aEL0NPu//VlHpuNzdFBA5Mgi0w+j9CNV60 4MTQXiAAqCfMKPTql+I5uUvI+yXaYAJvTb9KuIp6OTygnMjmF8de7Gl3Z0MZ3+gBPRpP12ZY WbwgtcGCWoGoxIyTPb2h12aTT5Te3GyUrog6TE8EYKqFJvMRoSwgLOaxyq7BZ1XZmVeCl+WC 3vodoOEW+0NaC2IOMNhnCYEBvCdTNoq0gjrvwvnwZJmKPDV82sWr8HNzt9wssTckxAp9TtxR ++d2n2RSHl9kmMZTi5+iKlwp01mylCG+aN9grpRHppS4aUaAU8BKZfAwrkiWJjJUQXbc4LRI L7HatCvADVqC8k038dLeEFlXdOrkhHE2SOuRb4Tjb2CQpIuoerHx3akAcF7xj7d0bU5yUE8S 55GOmunna548iDYAo+Pmk7flqD5Pb8E0nv1/XyYhXGLoFkeVQdxVavfWnVKb0TQrM/54UbqR LqvT70sdApHmoaZMqUfTNrvgB1dQev7ftTTZ2Xkg2CrGROB3a+BdqLvcmQZmi7YCQ4NmEYS+ x5qLCAYASGs6yLbBT1qThf0Zl/0tPJ5sDW9R1M1yAeDawtg0aC081gbn67UTfRbxb8CtCo7z lc8VF+gw9LbDcaBrAt9be1dZ906+lJOyWPesUR0IJWhK6loglNWfR5wugvi0BB+C4MIlsZPz jtixQV0KLmY11ZpfDaZm5n7fLzRayHz8B2pd6/KywTGyt/FsqwL6fk+txDipFTwTBFkrS4hi YEOlSHFvMavbkJaS5/6X0cp+gIvorjbZnJ4/IbIzTh3NrHytDbe2tUvDe9jyxC6ft4ZPrnXc W26W8AcGcWqL/Qn3lazaRdRduld8q8vP8SjX/CD2eiiN6Bhmnj16AYPqJA4yU+K+ydmH6TB0 JAE2PGf2yOMUja6hVzns8a9yshUIDoVGGS40y3tAoVcM7ZzcYg8AmCrO8Srx996ivYBQlZg/ UW4TxMD0c6tIl+JakDlmBZXzQIRqGCmni2xy3p1lSsop+yRxn6Gz+PnfRsBcmlFIQsqxV7jJ 4mvj9cfdEOtbk4gn12k4w72yrNaq6J2M2TICR4SJG6odCc4CvD27OPYK8dUoIslqyBWTPixb TX4Avbmrh0W3jmiV2pSyTYndi2775Dwnhh0kmWYfz54qHvUf901xA+KvYaHA6AKmGBeH28i0 GOEYzr0d8Ok9tiViZrZ5+W3Vmb6E4ZWbTGu1oSY8i2y+WxtBxS72fG1gNzuVwYggkqZn5FnU zvFqBHkb8zlzaO/ZKhucU9pH1/77uJxH4A4m4B2hZdaih14zt2FuGEKl2v+K4AR0K34bWENQ jsjyNvUpgHunkxlZCHB18fyUXOTxdFkbt+xbzYN2y4z2MtNDb+d8L1OmSYmxzjw5RKUe/V2m S0RjOc/8HNPyf9coxIjl2/OSqBXB0RTOjbg0giF/8zr5rsCf36hKPC1xAJolNSlRtluuyl6X 3D0MtcnFC50tYBkNU7UlWb08sficcXRatQasluVlQ3Bhq5bMsB5kP1CnidhNW/n2B9tg+cmk Rxj2427t4mbOi1s+qy+GBtRKjzyYYsa5Djsia9Umsve0ZqoG91tHTACXZ2gSvzNcnparfP8K wOHCyExsF+eELvbWwSa6QFvpDTOFdHjNn2aImUY0cQ3RBSZIx864khcVzE7k5glUwGykZW7K wEnvXZLvgW+8EIWmYcKf1HlX2zSpRmlcGIxQZmbd19N6x1aolzSKYqY5/5yGCdR+tugqhaMI yqVfVctbylBV0qaClTkJrTr68PH9r3SD+W4LuDOZrCmoulfEf6Dg5OpmNgDnX7EJoCUM39uA udukFJERmx8Et/Fli8nTiUWk2TGas/drRz6+ys9/aXduLz7HQno44WIEb5bN95irgu3jam0P OmVnC9lKDxc2/vkJFfNwbkbmlUXimdnfH+sF+ZY3cYoZKnVm+leBFgabXErXCOnx6k5309EM ojajIGsvoM=
Ironport-sdr: 64c70298_fmzMfrVPkgOZgjRLIkgDopl3NnY3TPKXLlsoJRSLdjNEd1Z 43o6kJb+cl2wb/ySfmQTYAJC9x58yICO4vnQ2eQ==

No, you cannot prove it without adding an additional axiom (possibly by importing the Classical library)

You can read more about this here:

https://en.m.wikipedia.org/wiki/Law_of_excluded_middle

Or the relevant section on this page: https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html

See also, this FAQ about the difference between Bool and Prop: https://coq.inria.fr/files/coq-itp-2015/faq-1.pdf

The manual for auto can be found here: https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html

Generally, many proofs in Coq are just okay without the excluded middle. If you think you need it, you may want to look into Classical, or work with Props that reflect bools, using a library like ssreflect.

On Mon, Jul 31, 2023, 09:28 Frank Schwidom <schwidom AT gmx.net> wrote:

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