Fwd: Question about proof of law of excluded middle in HOL Light
Paola Bruscoli <[email protected]> Fri, 15 May 2015 19:25:15 +0000
| Newsgroups | gmane.science.mathematics.frogs |
|---|---|
| Message-ID | <[email protected]> |
--_000_A13E98EA7C4E4FE1BE9526BE79527E2Bbathacuk_ Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Number of messages awaiting moderation for this list : 1 From: Robert White <[email protected]<mailto:ai.robert.wangshua= [email protected]>> Subject: Question about proof of law of excluded middle in HOL Light Date: 15 May 2015 18:02:52 BST Hi all, I wonder if anyone could explain a bit of the last step of the proof of law= of excluded middle (in the file class.ml<http://class.ml/>) in HOL Light. = I am not sure how the rewriting magically converted 0 [`F <=3D> (@x. (x <=3D> F) \/ t)`] 1 [`T <=3D> (@x. (x <=3D> T) \/ t)`] 2 [`t`] `~((@x. (x <=3D> T) \/ t) <=3D> (@x. (x <=3D> F) \/ t)) =3D=3D> (@x. (x <= =3D> F) \/ t)` to `t \/ ~t` The proof in HOL Light is as follows: let EXCLUDED_MIDDLE =3D prove (`!t. t \/ ~t`, GEN_TAC THEN SUBGOAL_THEN `(((@x. (x <=3D> F) \/ t) <=3D> F) \/ t) /\ (((@x. (x <=3D> T) \/ t) <= =3D> T) \/ t)` MP_TAC THENL [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN DISJ1_TAC THEN REFL_TAC; DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~(T <=3D> F)`) THEN PURE_ONCE_ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[ITAUT `p \/ T <=3D> T`]]);; PS: Is there a way I can print out how it is done step by step automaticall= y form OCaml Toplevel? Thanks very much! -- Regards, Robert --_000_A13E98EA7C4E4FE1BE9526BE79527E2Bbathacuk_ Content-Type: text/html; charset="us-ascii" Content-ID: <FD5B4A00B7F0754D8DA0D63D43DDF5AA-+E0FUbDlCk21Qrn1Bg8BZw@public.gmane.org> Content-Transfer-Encoding: quoted-printable <html> <head> <meta http-equiv=3D"Content-Type" content=3D"text/html; charset=3Dus-ascii"= > </head> <body style=3D"word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-lin= e-break: after-white-space;" class=3D""> <div> <blockquote type=3D"cite" class=3D""> <div class=3D"">Number of messages awaiting moderation for this list : 1<br= class=3D""> <div style=3D"margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margi= n-left: 0px;" class=3D""> <span style=3D"font-family: -webkit-system-font, Helvetica Neue, Helvetica,= sans-serif; color:rgba(127, 127, 127, 1.0);" class=3D""><b class=3D"">From= : </b></span><span style=3D"font-family: -webkit-system-font, Helvetica Neue,= Helvetica, sans-serif;" class=3D"">Robert White <<a href=3D"mailto:ai.r= [email protected]" class=3D"">[email protected]</a>>= <br class=3D""> </span></div> <div style=3D"margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margi= n-left: 0px;" class=3D""> <span style=3D"font-family: -webkit-system-font, Helvetica Neue, Helvetica,= sans-serif; color:rgba(127, 127, 127, 1.0);" class=3D""><b class=3D"">Subj= ect: </b></span><span style=3D"font-family: -webkit-system-font, Helvetica Neue,= Helvetica, sans-serif;" class=3D""><b class=3D"">Question about proof of l= aw of excluded middle in HOL Light</b><br class=3D""> </span></div> <div style=3D"margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margi= n-left: 0px;" class=3D""> <span style=3D"font-family: -webkit-system-font, Helvetica Neue, Helvetica,= sans-serif; color:rgba(127, 127, 127, 1.0);" class=3D""><b class=3D"">Date= : </b></span><span style=3D"font-family: -webkit-system-font, Helvetica Neue,= Helvetica, sans-serif;" class=3D"">15 May 2015 18:02:52 BST<br class=3D""> </span></div> <div style=3D"margin-top: 0px; margin-right: 0px; margin-bottom: 0px; margi= n-left: 0px;" class=3D""> <span style=3D"font-family: -webkit-system-font, Helvetica Neue, Helvetica,= sans-serif;" class=3D""><br class=3D""> </span></div> <br class=3D""> <br class=3D""> <div dir=3D"ltr" class=3D""> <div style=3D"font-size:12.8000001907349px" class=3D"">Hi all,</div> <div style=3D"font-size:12.8000001907349px" class=3D""><br class=3D""> </div> <div style=3D"font-size:12.8000001907349px" class=3D"">I wonder if anyone c= ould explain a bit of the last step of the proof of law of excluded middle = (in the file <a href=3D"http://class.ml/" class=3D"">class.ml</a>) in = HOL Light. I am not sure how the rewriting magically converted</div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= size: 15px; font-family: 'Courier New'; vertical-align: baseline; white-spa= ce: pre-wrap; background-color: transparent;" class=3D""><br class=3D""> </span><span style=3D"font-size: 15px; font-family: 'Courier New'; vertical= -align: baseline; white-space: pre-wrap; background-color: transparent;" cl= ass=3D""> 0 [`F <=3D> (@x. (x <=3D> F) \/ t)`]</span><span= style=3D"font-size: 15px; font-family: 'Courier New'; vertical-align: base= line; white-space: pre-wrap; background-color: transparent;" class=3D""><br= class=3D""> </span><span style=3D"font-size: 15px; font-family: 'Courier New'; vertical= -align: baseline; white-space: pre-wrap; background-color: transparent;" cl= ass=3D""> 1 [`T <=3D> (@x. (x <=3D> T) \/ t)`]</span><span= style=3D"font-size: 15px; font-family: 'Courier New'; vertical-align: base= line; white-space: pre-wrap; background-color: transparent;" class=3D""><br= class=3D""> </span><span style=3D"font-size: 15px; font-family: 'Courier New'; vertical= -align: baseline; white-space: pre-wrap; background-color: transparent;" cl= ass=3D""> 2 [`t`]</span><br class=3D""> </div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= size: 15px; font-family: 'Courier New'; vertical-align: baseline; white-spa= ce: pre-wrap; background-color: transparent;" class=3D""><br class=3D""> </span></div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= size: 15px; font-family: 'Courier New'; vertical-align: baseline; white-spa= ce: pre-wrap; background-color: transparent;" class=3D"">`~((@x. (x <=3D= > T) \/ t) <=3D> (@x. (x <=3D> F) \/ t)) =3D=3D> (@x. (x <=3D> F) \/ t)`</span><br class=3D""> </div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= size: 15px; font-family: 'Courier New'; vertical-align: baseline; white-spa= ce: pre-wrap; background-color: transparent;" class=3D""><br class=3D""> </span></div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= size: 15px; font-family: 'Courier New'; vertical-align: baseline; white-spa= ce: pre-wrap; background-color: transparent;" class=3D"">to </span></d= iv> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= family: 'Courier New'; font-size: 15px; white-space: pre-wrap; background-c= olor: transparent;" class=3D""><br class=3D""> </span></div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= family: 'Courier New'; font-size: 15px; white-space: pre-wrap; background-c= olor: transparent;" class=3D"">`t \/ ~t`</span></div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= family: 'Courier New'; font-size: 15px; white-space: pre-wrap; background-c= olor: transparent;" class=3D""><br class=3D""> </span></div> <div style=3D"font-size:12.8000001907349px" class=3D""><span style=3D"font-= family: 'Courier New'; font-size: 15px; white-space: pre-wrap; background-c= olor: transparent;" class=3D"">The proof in HOL Light is as follows:</span>= </div> <div style=3D"font-size:12.8000001907349px" class=3D""> <div class=3D"">let EXCLUDED_MIDDLE =3D prove</div> <div class=3D""> (`!t. t \/ ~t`,</div> <div class=3D""> GEN_TAC THEN SUBGOAL_THEN</div> <div class=3D""> `(((@x. (x <=3D> F) \/ t) <=3D> F)= \/ t) /\ (((@x. (x <=3D> T) \/ t) <=3D> T) \/ t)`</div> <div class=3D""> MP_TAC THENL</div> <div class=3D""> [CONJ_TAC THEN CONV_TAC SELECT_CONV THENL</div= > <div class=3D""> [EXISTS_TAC `F`; EXISTS_TAC `T`] THEN</= div> <div class=3D""> DISJ1_TAC THEN REFL_TAC;</div> <div class=3D""> DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN</div= > <div class=3D""> TRY(DISJ1_TAC THEN FIRST_ASSUM ACCEPT_TAC) TH= EN</div> <div class=3D""> DISJ2_TAC THEN DISCH_TAC THEN MP_TAC(ITAUT `~= (T <=3D> F)`) THEN</div> <div class=3D""> PURE_ONCE_ASM_REWRITE_TAC[] THEN</div> <div class=3D""><b class=3D""> ASM_REWRITE_TAC[ITAUT `p \/ T &= lt;=3D> T`]]);;</b></div> </div> <div style=3D"font-size:12.8000001907349px" class=3D""><br class=3D""> </div> <div style=3D"font-size:12.8000001907349px" class=3D"">PS: Is there a way I= can print out how it is done step by step automatically form OCaml Topleve= l?</div> <div style=3D"font-size:12.8000001907349px" class=3D""><br class=3D""> </div> <div style=3D"font-size:12.8000001907349px" class=3D"">Thanks very much!</d= iv> <div class=3D""><br class=3D""> </div> -- <br class=3D""> <div class=3D"gmail_signature"> <div dir=3D"ltr" class=3D""> <div class=3D""> <div dir=3D"ltr" class=3D""> <div class=3D""> <div dir=3D"ltr" class=3D""> <div class=3D""> <div dir=3D"ltr" class=3D""> <div class=3D""><br class=3D""> </div> <div class=3D"">Regards,</div> <div class=3D"">Robert</div> </div> </div> </div> </div> </div> </div> </div> </div> </div> <br class=3D""> <br class=3D""> </div> </blockquote> </div> <br class=3D""> </body> </html> --_000_A13E98EA7C4E4FE1BE9526BE79527E2Bbathacuk_--