not_eq_impl_false

Stream: new members

[Cypooos]

Hello !

I'm a new member who just started learning Lean with The Natural Number Game.

I want to prove in intuitionistic logic this property (I've started a bit)

example (A : Prop) : (∀ B : Prop, (((A → B) → A) → A)) → (¬¬ A → A) :=
begin
  intros h nnA,
  have choose_B_false := h (false),

end

And now I need to use the definition of not : implie false.
Where can I find such a property ? And for the future, where can I easely find them ?

Should I use axiom ? And how ?

Thanks for the answers ^^

[Patrick Massot]

Lean knows about the definition, you don't need to "use it".

[Patrick Massot]

If you want to help your eyes, you can type things like: change ¬ A → false at nnA,

[Patrick Massot]

Do you know about the apply tactic? And about false.elim?

[Cypooos]

I know about the apply one, not the false.elim

[Patrick Massot]

Maybe you know the exfalso tactic then?

[Patrick Massot]

Anyway, false.elim will take as input a proof of false and output a proof of whatever you want.

[Cypooos]

yes but I've never used it.

I know how to solve the puzzle, I just want to write the proof in Lean. Maybe you want me to tell you how ?

[Patrick Massot]

Oh sure.

[Patrick Massot]

I thought you didn't want spoilers.

[Patrick Massot]

Give 30 seconds to launch the web editor from your snippet

[Patrick Massot]

example (A : Prop) : (∀ B : Prop, ((A → B) → A) → A) → (¬¬ A → A) :=
begin
  intros h nnA,
  have choose_B_false := h (false),
  apply choose_B_false,
  intro hnA,
  exact false.elim (nnA hnA),
end

[Patrick Massot]

This is using your beginning.

[Patrick Massot]

It can be compressed a lot of course.

[Patrick Massot]

example (A : Prop) : (∀ B : Prop, ((A → B) → A) → A) → (¬¬ A → A) :=
λ h nnA, h false (λ hnA, (nnA hnA).elim)

[Cypooos]

Yeah I just need to understand it now. What does false.elim ? I've read the doc but I didn't really truly understand it.

[Cypooos]

Patrick Massot said:

example (A : Prop) : (∀ B : Prop, ((A → B) → A) → A) → (¬¬ A → A) :=
λ h nnA, h false (λ hnA, (nnA hnA).elim)

That's dense

[Patrick Massot]

If you are interested in pure logic rather than regular maths (as I gather from the fact that you know the words "intuitionistic logic") then we have great resources for you, search for "Logic and proof" and "Theorem proving in Lean" on https://leanprover-community.github.io/learn.html

[Cypooos]

Definitely going to look at this !

Thanks !

[Patrick Massot]

We don't mind answering beginners questions, but you'll have a far less frustrating experience if you try to follow Theorem proving in Lean instead of trying to get away with explanation from the natural number game.

[Cypooos]

I will then. Sorry to bother !

[Patrick Massot]

There is no problem at all!