Existential quantifier to negation of universal quantifier

Stream: new members

[Javier Gómez Zaragoza]

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!

[Alex J. Best]

docs#not_forall_not

[Javier Gómez Zaragoza]

Thanks a lot!

[Kevin Buzzard]

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

[Kevin Buzzard]

@Javier Gómez Zaragoza

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

:-|

[Javier Gómez Zaragoza]

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

[Kevin Buzzard]

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.

[Javier Gómez Zaragoza]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

But it's best to avoid smileys.

[Javier Gómez Zaragoza]

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.

[Kevin Buzzard]

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!

[Javier Gómez Zaragoza]

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!