Zulip Chat Archive

Stream: new members

Topic: Existential quantifier to negation of universal quantifier


view this post on Zulip Javier Gómez Zaragoza (Nov 20 2020 at 11:54):

Hi, I'm starting in Lean and doing a codewar kata I wanted to use the following (∃ x, p x) ↔ ¬ (∀ x, ¬ p x). I know this is an exercise in the Lean tutorial and I suppose it is a theorem in classical logic, but I'm not sure how is it called. Thanks a lot!

view this post on Zulip Alex J. Best (Nov 20 2020 at 12:18):

docs#not_forall_not

view this post on Zulip Javier Gómez Zaragoza (Nov 20 2020 at 12:19):

Thanks a lot!

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:23):

import tactic

example (X : Type) (p : X  Prop) : ( x, p x)  ¬ ( x, ¬ p x) :=
begin
  library_search -- output tells you what you wanted to know :-)
end

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:23):

@Javier Gómez Zaragoza

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:24):

oh cool, and the smiley in the comment breaks the "try this" click as well :D

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:25):

lol, if you replace it by :-( then the try this click eats end!

view this post on Zulip Reid Barton (Nov 20 2020 at 12:26):

:-|

view this post on Zulip Javier Gómez Zaragoza (Nov 20 2020 at 12:28):

Thanks a lot! I thought the library_search tactic didn't work in codewars but I guess it does!

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:29):

I'm not suggesting you use it in your final code :-) It's just a general trick for answering questions of the form you are asking. The library now is gigantic and it's very hard to remember all the names of everything, despite the fabulous #naming conventions.

view this post on Zulip Javier Gómez Zaragoza (Nov 20 2020 at 12:33):

Yes, I will replace it with exact not_forall_not as Alex J. Best suggested. Thanks for the quick answer!

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:39):

Just to check you know -- library_search is a tactic which actually produces output. In the infoview it says "try this: ..." and if you click on the suggestion then library_search replaces itself with the theorem which the search found.

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:39):

But it's best to avoid smileys.

view this post on Zulip Javier Gómez Zaragoza (Nov 20 2020 at 12:44):

I'm actually not that familiarised with the "interactiveness" of this tactic since I'm mainly using Lean in codewars now, and there you have to send the attempt and wait for the output to appear. When I install Lean and mathlib in VScode I'll use this tactic a lot more for sure.

view this post on Zulip Kevin Buzzard (Nov 20 2020 at 12:47):

Youch! I would strongly recommend installing Lean and mathlib and VS Code, and setting up a Codewars project which uses precisely the same version of Lean and mathlib as Codewars does. If you just upload code to codewars then you cannot write code interactively, making any non-trivial kata extremely difficult to solve.

At the very least you might want to use the web editor but this runs a slightly more modern lean/mathlib which could occasionally be problematic. But at least you can see what you're doing rather than coding blind!

view this post on Zulip Javier Gómez Zaragoza (Nov 20 2020 at 12:52):

Yes, I use the web editor sometimes to look up theorems, but you're right the proper way to solve katas is to run VS Code on the side. Thanks a lot!


Last updated: May 14 2021 at 06:16 UTC