not(p<->not p)

Stream: new members

[Manikhanta Teja]

Is there a way in which we can prove not(p<->not p) without using classical?

[Mario Carneiro]

yes

[Kevin Buzzard]

Ha ha this question should be in the FAQ, as we used to say in the heyday of USENET

[Kevin Buzzard]

@Manikhanta Teja this comes up every few months. It's an exercise in Theorem Proving In Lean. Searching for a solution in this forum might work. It's a great exercise :-)

[Manikhanta Teja]

I couldnt find it. But i tried doing it.

variable p : Prop
example : ¬(p <-> ¬p) :=
assume h1 : (p <-> ¬p),
show false, from
(assume h2 : p,
have h3 : not p, from iff.elim_left h1 h2,
have h4 : p, from iff.elim_right h1 h3,
show false, from h3 h4
)

I get this error

type mismatch at application
  (λ (this : false), this)
    (λ (h2 : p),
       have h3 : ¬p, from iff.elim_left h1 h2,
       have h4 : p, from iff.elim_right h1 h3,
       show false, from h3 h4)
term
  λ (h2 : p), have h3 : ¬p, from iff.elim_left h1 h2, have h4 : p, from iff.elim_right h1 h3, show false, from h3 h4
has type
  p → false
but is expected to have type
  false

but if I do this, it works.

variable p : Prop
variable h2 : p
example : ¬(p <-> ¬p) :=
assume h1 : (p <-> ¬p),
show false, from
have h3 : not p, from iff.elim_left h1 h2,
have h4 : p, from iff.elim_right h1 h3,
show false, from h3 h4

How do i do this without using another variable h2

[Manikhanta Teja]

i got it. But i didnt get it using the above solution

[Mario Carneiro]

putting a variable h2 : p like that is basically assuming that p is true

[Mario Carneiro]

you actually proved p -> ¬(p <-> ¬p)

[Mario Carneiro]

Here's a hint: not p means p -> false. Is there another way to prove h3?

[Andrew Ashworth]

I thought for sure there was a worked solution somewhere in the chat history. Anyway, here's something ugly I threw together:

example : ∀ P : Prop, ¬(P ↔ ¬P) :=
λ P h, let p : P := (iff.mpr h $ λ h₁, iff.mp h h₁ h₁) in iff.mp h p p

[Kevin Buzzard]

I thought for sure there was a worked solution somewhere in the chat history.

For sure there is, but I guess it might be hard to search for it.

[Johan Commelin]

@[tidy] meta def apply_assumption' := `[apply_assumption]

lemma help_me (P : Prop) : ¬(P ↔ ¬ P) :=
by tidy?

/- `tidy` says -/
  intros a,
  cases a,
  apply_assumption',
  work_on_goal 0 {
    apply_assumption',
    intros a,
    solve_by_elim },
  apply_assumption',
  intros a,
  solve_by_elim

#print help_me

theorem help_me : ∀ (P : Prop), ¬(P ↔ ¬P) :=
λ (P : Prop),
  id
    (λ (a : P ↔ ¬P),
       iff.dcases_on a
         (λ (a_mp : P → ¬P) (a_mpr : ¬P → P),
            a_mp (a_mpr (id (λ (a : P), a_mp a a))) (a_mpr (id (λ (a : P), a_mp a a)))))

[Scott Morrison]

I really need to finish back, so it can be installed as a standard part of tidy, so you don't need that pesky first line. :-)

[Scott Morrison]

Of course, library_search promptly says: λ (a : Prop), (iff_not_self a).mp. :-)

[Manikhanta Teja]

I got it. Thanks ;)

[Johan Commelin]

One thing that tidy could optimise is recognising that it is proving the same goal twice. I've started work on a dedup-goals tactic... but I got weird buggy behaviour. See the merge-goals branch.

[Kevin Buzzard]

Let me just show you Johan's proof of not(p iff not p) in tactic mode

[Kevin Buzzard]

lemma help_me (P : Prop) : ¬(P ↔ ¬ P) :=
begin
  intro h,
  cases h with h1 h2, -- <- put your cursor here and look at the tactic state
  -- the key lemma
  have hnp : ¬ P,
  -- two goals now, the one we had and the new one we just set ourselves
  { -- back down to one goal, we'll leave the other one until after we finished the {}
    intro hP, -- <- put your cursor here and see what we have, and what we want
    have hnP : ¬ P,
      sorry,
    sorry
  },
  sorry
end

[Kevin Buzzard]

I'm in the middle of writing a tactic mode proof of the question which started this thread.

[Kevin Buzzard]

Assuming you're using VS Code, cut and paste that code into VS Code and put your cursor at the points I suggest, and then move it up and down with the up/down arrow keys. Crucially, make sure you have the right "lean messages" window open as well.-- get it with Ctrl-Shift-Enter

[Kevin Buzzard]

tactic_mode.png

[Kevin Buzzard]

If you are a beginner then I think that the way tactic mode holds your hand is really helpful.

[Kevin Buzzard]

If you can get things set up so they look like the above, and you start moving your cursor up and down, you will see the tactic state and the goal changing on the right, and this set-up greatly clarifies, for me at least, exactly what you can assume and what you are supposed to be proving at any point.

[Patrick Massot]

To be fair, one should say the term mode analogue of Kevin's template is:

lemma help_me (P : Prop) : ¬(P ↔ ¬ P) :=
assume ⟨h₁, h₂⟩,
  have hnp : ¬ P, from
    assume hP,
    have hnP : ¬ P, from _,
    _, _

putting the cursor on the underline also tells you what is the state and what Lean wants. But I still agree with Kevin that it's much easier in tactic mode

[Kevin Buzzard]

Yeah, Patrick is exactly right, but this very important trick with _ is not as far as I remember, stressed in TPIL

[Kevin Buzzard]

It was extremely helpful for me when I started to learn term mode properly

[Kevin Buzzard]

but with tactic mode the entire tactic state and goal are there, the moment you have understood the difference between the two windows both unfortunately called "Lean Messages", which I just used to open randomly

[Kevin Buzzard]

One is ctrl-shift-enter, one is ctrl-alt-shift-enter, they both look indistinguishable, and one is helpful in tactic mode and the other isn't.

[Kevin Buzzard]

lemma help_me (P : Prop) : ¬(P ↔ ¬ P) :=
begin
  intro h,
  cases h with h1 h2, -- <- put your cursor here and look at the tactic state
  -- the key lemma
  have hnP : ¬ P,
  -- two goals now, the one we had and the new one we just set ourselves
  { -- back down to one goal, we'll leave the other one until after we finished the {}
    intro hP, -- <- put your cursor here and see what we have, and what we want
    have hnP : ¬ P,
    -- after each "have" open some {}s to keep the number of goals down to 1
    { exact h1 hP
    },
    exact hnP hP,
  },
  have hP : P,
  { exact h2 hnP,
  },
  exact hnP hP
end

[Manikhanta Teja]

I'll start with simple proofs. This looks a lot better. Thanks @Kevin Buzzard

[Kevin Buzzard]

http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/M1F_introduction/prop_exercises.html

This is some very shoddy notes

[Kevin Buzzard]

It's what I tell my students to look at. I will rewrite them properly this summer, but it pushes tactic mode from the start.

[Andrew Ashworth]

Just a small note on those notes: you might want to use "introduce" where-ever you use "construct", mostly because if you're mashing ctrl-t for lemma search, introduction rules are generally marked with intro (e.g. iff.intro), same with elimination (iff.elim)

[Kevin Buzzard]

Thanks!