Zulip Chat Archive

Stream: new members

Topic: excluded middle from dne


view this post on Zulip 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 :=
by_contradiction
    (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?

view this post on Zulip Patrick Massot (Mar 14 2019 at 07:39):

You should start with ensuring parentheses are balanced

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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))?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 14 2019 at 07:58):

Are you reading TPIL?

view this post on Zulip Kevin Buzzard (Mar 14 2019 at 07:58):

They start with this horrible mode

view this post on Zulip 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

view this post on Zulip Manikhanta Teja (Mar 14 2019 at 07:59):

Yeah i started with TPIL.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Manikhanta Teja (Mar 14 2019 at 08:01):

Starting chapter 5 now. Thanks.

view this post on Zulip 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 λ

view this post on Zulip 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>

view this post on Zulip Manikhanta Teja (Mar 15 2019 at 00:01):

open classical
variable A : Prop
theorem dne ( h: not ( not A )) : A :=
by_contradiction
    (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

view this post on Zulip Kevin Buzzard (Mar 15 2019 at 00:09):

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

view this post on Zulip Chris Hughes (Mar 15 2019 at 00:11):

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

view this post on Zulip Manikhanta Teja (Mar 15 2019 at 00:13):

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

view this post on Zulip Manikhanta Teja (Mar 15 2019 at 00:14):

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

view this post on Zulip 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

view this post on Zulip 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