Stream: new members

Topic: intro inside iff

Danila Kurganov (Jul 13 2020 at 13:28):

Hi,

Is there any way to do a version of intro x, where the x is then introduced (removed) from both sides of the goal statement at once?
 ⊢ (∀ (x : X), x ∈ A → x ∈ B) ↔ ∀ (x : X), x ∈ B ↔ x ∈ A ∪ B

Mario Carneiro (Jul 13 2020 at 13:28):

apply forall_congr, intro x

Jalex Stark (Jul 13 2020 at 13:44):

for what it's worth, forall_congr comes up if you ask suggest for advice (although it's not quite at the top of the list)

import tactic
example (X: Type) (A B : set X) : (∀ (x : X), x ∈ A → x ∈ B) ↔ ∀ (x : X), x ∈ B ↔ x ∈ A ∪ B :=
begin
suggest,
end


Mario Carneiro (Jul 13 2020 at 13:45):

The congr tactic should really be able to do this

Jalex Stark (Jul 13 2020 at 13:51):

I agree. I spent a minute trying to massage it into a form where congr or congr' did something, but this didn't work.

Danila Kurganov (Jul 13 2020 at 14:09):

I think I got a little tunnel vision doing a problem and forgot I could even do suggest!

Kevin Buzzard (Jul 13 2020 at 16:05):

@Danila Kurganov in some sense the reason this isn't easier (e.g. "true by definition") is that it's only a one way implication. "forall x, (P x <-> Q x)" certainly implies "(forall x, P x) <-> (forall x, Q x)", but the other implication is false in general. That's why you have to apply something.

Danila Kurganov (Jul 13 2020 at 21:00):

That's a good point, so for backwards reasonings generally

Last updated: May 13 2021 at 18:26 UTC