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