Zulip Chat Archive

Stream: Is there code for X?

Topic: tactic to eliminate double negation


view this post on Zulip Patrick Thomas (Oct 04 2020 at 11:29):

Is there a tactic that does nothing except change not not P to P everywhere in an expression?

view this post on Zulip Shing Tak Lam (Oct 04 2020 at 11:35):

simp only [not_not]

view this post on Zulip Patrick Thomas (Oct 04 2020 at 11:37):

Thank you.

view this post on Zulip Patrick Thomas (Oct 04 2020 at 11:53):

The simp lemma has to be of the form l = r or l ↔ r?

view this post on Zulip Patrick Thomas (Oct 04 2020 at 12:15):

Out of curiosity, is there a theoretical limitation preventing having a similar tactic that also works for ?

view this post on Zulip Kevin Buzzard (Oct 04 2020 at 12:51):

Find the iff version using library search and simp on that instead

view this post on Zulip Patrick Thomas (Oct 04 2020 at 12:53):

I was just thinking it might be an interesting exercise to make one, but not if it is theoretically impossible.

view this post on Zulip Reid Barton (Oct 04 2020 at 13:07):

It's a rather different problem, because everything in Lean preserves =, while only some specific subset of things preserves .

view this post on Zulip Reid Barton (Oct 04 2020 at 13:12):

For example if p = q then you can conclude not p = not q but from p -> q you can't conclude not p -> not q.

view this post on Zulip Aaron Anderson (Oct 04 2020 at 17:16):

You may also be interested in push_neg

view this post on Zulip Patrick Thomas (Oct 04 2020 at 17:45):

How do you use simp to simplify a hypothesis, for example:

example {P Q : Prop} : ¬ (¬ P  Q)  (P  ¬ Q) :=
begin
have s1 : ¬ (¬ P  Q)  (¬ ¬ P  ¬ Q) := sorry
-- use a variation of simp only [not_not] here
end

view this post on Zulip Aaron Anderson (Oct 04 2020 at 17:50):

simp at s1

view this post on Zulip Aaron Anderson (Oct 04 2020 at 17:52):

Although it'd be better to use simp only [...], as that hint says, so simp only [not_not] at s1

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:02):

I may be doing something else wrong. This doesn't seem to work:

import tactic

lemma not_not_1 {P : Prop} : ¬ ¬ P  P :=
assume a1 :  ¬ ¬ P,
by_contradiction (
  assume a2 : ¬ P,
  show false, from a1 a2
)

lemma not_not_2 {P : Prop} : P  ¬ ¬ P :=
assume a1 : P,
assume a2 : ¬ P,
show false, from a2 a1

lemma not_not' {P : Prop} : ¬ ¬ P  P :=
iff.intro not_not_1 not_not_2

example {P Q : Prop} : ¬ (¬ P  Q)  (P  ¬ Q) :=
begin
have s1 : ¬ (¬ P  Q)  (¬ ¬ P  ¬ Q) := sorry,
have s2 : ¬ (¬ P  Q)  (P  ¬ Q), by simp only [not_not'] at s1,
sorry
end

view this post on Zulip Ruben Van de Velde (Oct 04 2020 at 18:05):

simp changes the existing hypothesis; this works:

have s2 : ¬ (¬ P  Q)  (P  ¬ Q), by {simp only [not_not'] at s1, exact s1},

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:11):

Oh. Can it be used to return the result instead?

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:11):

That is, is there an option to it for that.

view this post on Zulip Patrick Massot (Oct 04 2020 at 18:13):

What do you mean by "return the result"?

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:15):

Maybe add a new hypothesis with a user given name and leave s1 unchanged?

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:15):

I guess it doesn't really matter.

view this post on Zulip Shing Tak Lam (Oct 04 2020 at 18:15):

That's what Ruben's code does. s1 is the same before and after that line.

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:15):

Nevermind, sorry.

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:16):

Oh. Right. I was putting the cursor after the first part of it, I didn't expect it to change back.

view this post on Zulip Patrick Thomas (Oct 04 2020 at 18:17):

Thank you.


Last updated: May 07 2021 at 21:10 UTC