tactic to eliminate double negation

Stream: Is there code for X?

[Patrick Thomas]

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

[Shing Tak Lam]

simp only [not_not]

[Patrick Thomas]

Thank you.

[Patrick Thomas]

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

[Patrick Thomas]

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

[Kevin Buzzard]

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

[Patrick Thomas]

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

[Reid Barton]

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

[Reid Barton]

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]

You may also be interested in push_neg

[Patrick Thomas]

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

[Aaron Anderson]

simp at s1

[Aaron Anderson]

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

[Patrick Thomas]

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]

simp changes the existing hypothesis; this works:

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

[Patrick Thomas]

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

[Patrick Thomas]

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

[Patrick Massot]

What do you mean by "return the result"?

[Patrick Thomas]

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

[Patrick Thomas]

I guess it doesn't really matter.

[Shing Tak Lam]

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

[Patrick Thomas]

Nevermind, sorry.

[Patrick Thomas]

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

[Patrick Thomas]

Thank you.