iff negation

Stream: new members

[Bhavik Mehta]

Is there a tactic I can use to make this immediate?

example (A B : finset (fin n)) (a : fin n) (h : a ∉ A ↔ a ∉ B) : (a ∈ A ↔ a ∈ B) := by finish

I know I can do it by hand if I had to, but this seems like the sort of thing finish ought to be good at so I don't have to think about it

[Kevin Buzzard]

logic.basic is the place to look for things like this

[Kevin Buzzard]

Oh -- you want a tactic?

import data.finset
import tactic.tauto

variable (n : ℕ)

example (A B : finset (fin n)) (a : fin n) (h : a ∉ A ↔ a ∉ B) : (a ∈ A ↔ a ∈ B) :=
by tauto!

[Kevin Buzzard]

tauto and tauto! are always good for logic nonsense.

[Bhavik Mehta]

Yeah I want a tactic so I don't have to get my hands dirty with this sort of thing in the middle of a big proof

[Bhavik Mehta]

I tried tauto, finish and finish!, but I didn't think to try tauto!... :(

[Kevin Buzzard]

Yeah, Patrick taught me about tauto!

[Kevin Buzzard]

Looking at the meta code, what might be going on is that tauto is for constructive logic and tauto! for classical logic?

[Bhavik Mehta]

That makes sense!

[Bhavik Mehta]

I do wonder still why finish couldn't do it though

[Joe]

tauto works for me.

[Joe]

import data.finset
import tactic.tauto

variable (n : ℕ)

example (A B : finset (fin n)) (a : fin n) (h : a ∉ A ↔ a ∉ B) : (a ∈ A ↔ a ∈ B) :=
by tauto

[Bhavik Mehta]

Oh. My mistake then

[Kevin Buzzard]

import data.finset

variable (n : ℕ)

example (A B : finset (fin n)) (a : fin n) (h : a ∉ A ↔ a ∉ B) : (a ∈ A ↔ a ∈ B) :=
by split;finish