## Stream: Is there code for X?

### Topic: tactic to eliminate double negation

#### 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?

#### Shing Tak Lam (Oct 04 2020 at 11:35):

simp only [not_not]

Thank you.

#### Patrick Thomas (Oct 04 2020 at 11:53):

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

#### 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 ?

#### Kevin Buzzard (Oct 04 2020 at 12:51):

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

#### 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.

#### 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 .

#### 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.

#### Aaron Anderson (Oct 04 2020 at 17:16):

You may also be interested in push_neg

#### 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

simp at s1

#### 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

#### 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

#### 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},

#### Patrick Thomas (Oct 04 2020 at 18:11):

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

#### Patrick Thomas (Oct 04 2020 at 18:11):

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

#### Patrick Massot (Oct 04 2020 at 18:13):

What do you mean by "return the result"?

#### Patrick Thomas (Oct 04 2020 at 18:15):

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

#### Patrick Thomas (Oct 04 2020 at 18:15):

I guess it doesn't really matter.

#### 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.

#### Patrick Thomas (Oct 04 2020 at 18:15):

Nevermind, sorry.

#### 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.

#### Patrick Thomas (Oct 04 2020 at 18:17):

Thank you.

Last updated: May 07 2021 at 21:10 UTC