## Stream: new members

### Topic: excluded middle from dne

#### Manikhanta Teja (Mar 14 2019 at 07:34):

I'm trying to prove A \/ not A using double negation elimination,

open classical
variable A : Prop
theorem dne ( h: not ( not A )) : A :=
(assume h1 : not A,
show false, from h h1)
example : A ∨ ¬ A :=
have h1 : not ( not ( A ∨ not A), from
assume hA : A,
have h2 : A ∨ ¬ A, from or.inl hA,
assume h3 : ¬ (A ∨ ¬ A),
show false, from h3 h2
show A ∨ ¬ A,from dne (A ∨ not A) h1


I'm getting these errors

em.lean:8:34: error
invalid expression
em.lean:13:0: error
invalid 'have' declaration, ',' expected


I dont knwo whats wrong with this. Is this the right way to do this?

#### Manikhanta Teja (Mar 14 2019 at 07:44):

Sorry. Balanced it but no change. i think i didnt prove this
 have h1 : not ( not ( A ∨ not A), from

#### Kevin Buzzard (Mar 14 2019 at 07:51):

I have been using this software for a while now and I still look at code like this and find it incomprehensible. I know all this have, assume, from stuff is supposed to make it feel closer to English or whatever but for me it turns the code into spaghetti. @Manikhanta Teja have you tried using tactic mode and more structured code with {} in?

#### Kevin Buzzard (Mar 14 2019 at 07:55):

What does assume even do? How can I just randomly assume A in the middle of a proof of not ( not ( A ∨ not A))?

#### Kevin Buzzard (Mar 14 2019 at 07:56):

Whilst I am not an expert in this horrible mode, I conjecture that if you're trying to prove things, you can't just write random assumptions like assume hA : A in the middle of a proof.

#### Manikhanta Teja (Mar 14 2019 at 07:57):

@Kevin Buzzard I'm trying to understand how this working. I'm still a beginner. I'm sorry.

#### Kevin Buzzard (Mar 14 2019 at 07:58):

I would probably have given up Lean there and then were it not for the fact that I had read a Coq tutorial that went straight into tactic mode

#### Manikhanta Teja (Mar 14 2019 at 07:59):

Yeah i started with TPIL.

#### Kevin Buzzard (Mar 14 2019 at 07:59):

I teach a lot of beginners how to use Lean, and for a question like this I would always start with the following template:

example : A ∨ ¬ A :=
begin
sorry
end


#### Kevin Buzzard (Mar 14 2019 at 07:59):

Here is a crazy suggestion: just stop what you're doing, go straight to chapter 5, and read a bit about doing basic logic in tactic mode.

#### Kevin Buzzard (Mar 14 2019 at 08:00):

The absolutely massive advantage of tactic mode for beginners is that at all times you can see exactly what you have already proved, and what you are trying to prove.

#### Manikhanta Teja (Mar 14 2019 at 08:01):

Starting chapter 5 now. Thanks.

#### Andrew Ashworth (Mar 14 2019 at 09:10):

What does assume even do? How can I just randomly assume A in the middle of a proof of not ( not ( A ∨ not A))?

assume is just notation for λ

#### Kevin Buzzard (Mar 14 2019 at 09:20):

So that answers the question of why the original code didn't compile -- the assume ha : A looks invalid because it would only work for goals of the form A -> <something>

#### Manikhanta Teja (Mar 15 2019 at 00:01):

open classical
variable A : Prop
theorem dne ( h: not ( not A )) : A :=
(assume h1 : not A,
show false, from h h1)
example : A ∨ ¬ A :=
have hN : not ( not ( A ∨ not A), from
(assume h1 :  ¬ (A ∨ ¬ A),
have h2 : ¬ A, from
assume h3 : A,
have h4 : A ∨ ¬ A, from or.inl h3,
show false, from h1 h4,
have h5 : A ∨ ¬ A, from or.inr h2,
show false, from h1 h5)
show A ∨ ¬ A,from dne(A ∨ not A) hN

em.lean:8:34: error
invalid expression
em.lean:17:0: error
invalid 'have' declaration, ',' expected


This is what i was trying to do. Get ¬¬(A ∨ ¬A) → A ∨ ¬A from dne( A \/ not A) and then apply implication elimination of ¬¬(A ∨ ¬A) → A ∨ ¬A to get A ∨ ¬A.
The proof for ¬¬(A ∨ ¬A) worked

variable A : Prop
theorem cc : ¬ (¬ ( A ∨ ¬ A)) :=
(assume h1 :  ¬ (A ∨ ¬ A),
have h2 : ¬ A, from
assume h3 : A,
have h4 : A ∨ ¬ A, from or.inl h3,
show false, from h1 h4,
have h5 : A ∨ ¬ A, from or.inr h2,
show false, from h1 h5)


Is there anything wrong with this
show A ∨ ¬ A,from dne(A ∨ not A) hN

#### Kevin Buzzard (Mar 15 2019 at 00:09):

The error seems to indicate you've got the syntax wrong somewhere.

#### Chris Hughes (Mar 15 2019 at 00:11):

There's a missing comma after show false, from h1 h5)

#### Manikhanta Teja (Mar 15 2019 at 00:13):

Still have a problem with
em.lean:8:34: error invalid expression

#### Manikhanta Teja (Mar 15 2019 at 00:14):

Got it. I'm an idiot. I didn't balance the paranthesis.

#### Kevin Buzzard (Mar 15 2019 at 00:20):

If you were to use tactic mode you would have none of these problems and the errors would be far less obscure

#### Kevin Buzzard (Mar 15 2019 at 00:21):

Tactic mode forces you to structure your proofs properly

Last updated: May 11 2021 at 00:31 UTC