## Stream: general

### Topic: Rewriting under forall with conv

#### Eric Wieser (Sep 11 2020 at 20:27):

How I can I rewrite(∀ a, ∀ b, b = f a → p b) ↔ (∀ a, p (f a)) to (∀ a, ∀ b, f a = b → p b) ↔ (∀ a, p (f a))? I want to apply eq_comm to the expression under the binder, but I can't see how to do it, and conv doesn't seem to give me any tool to remove the binder.

#### Chris Hughes (Sep 11 2020 at 20:29):

simp only [@eq_comm _ _ (f _)] is the easiest way.

#### Chris Hughes (Sep 11 2020 at 20:31):

 conv in (_ = f _) { rw eq_comm } is another way

#### Eric Wieser (Sep 11 2020 at 20:33):

If I'm in conv mode, is there an equivalent to intro to step inside the binder?

#### Kenny Lau (Sep 11 2020 at 20:34):

I believe it's congr

#### Eric Wieser (Sep 11 2020 at 20:34):

congr by itself throws away the entire expression

#### Bryan Gin-ge Chen (Sep 11 2020 at 20:35):

I thought it was funext? https://leanprover-community.github.io/extras/conv.html

#### Eric Wieser (Sep 11 2020 at 20:35):

mwe:

variables {α : Sort*} {β : Sort*}

theorem forall_eq_apply_imp_iff {f : α → β} {p : β → Prop} :
(∀ a, ∀ b, b = f a → p b) ↔ (∀ a, p (f a)) :=
by {
conv {
to_lhs,
congr,
},
sorry
}


#### Eric Wieser (Sep 11 2020 at 20:35):

I think @Chris Hughes gave me what I actually needed, but the manual conv steps would be helpful anyawy

#### Eric Wieser (Sep 11 2020 at 20:39):

@Bryan Gin-ge Chen , funext does nothing at all

#### Kenny Lau (Sep 11 2020 at 20:41):

conv in (_ = _) { rw eq_comm },

#### Chris Hughes (Sep 11 2020 at 20:43):

funext is for lambdas, this would be piext

#### Chris Hughes (Sep 11 2020 at 20:43):

Which doesn't exist

#### Eric Wieser (Sep 11 2020 at 20:45):

Just doesn't, or also can't?

#### Reid Barton (Sep 11 2020 at 20:45):

I wonder if this is why I get stuck using conv so often

#### Reid Barton (Sep 11 2020 at 20:45):

the conv in (_ = _) feels like it should be redundant--where else could you rw eq_comm?

#### Kenny Lau (Sep 11 2020 at 20:46):

yeah conv is highly incomplete and buggy

#### Eric Wieser (Sep 11 2020 at 20:47):

Also conv in (_ = _) { sorry } doesn't work, I have to already know what I want to do inside the {} it seems

#### Reid Barton (Sep 11 2020 at 20:47):

I see. I always assumed the documentation just didn't have the information I needed

#### Reid Barton (Sep 11 2020 at 20:48):

Eric Wieser said:

Also conv in (_ = _) { sorry } doesn't work, I have to already know what I want to do inside the {} it seems

I think this is probably bad error reporting--most likely there is no conv tactic sorry

#### Eric Wieser (Sep 11 2020 at 20:48):

It's not, because if I type really_sorry I get a different error

oh weird

#### Reid Barton (Sep 11 2020 at 20:50):

Well, the documentation claims that any error in a conv in will be reported as the pattern not being found

#### Eric Wieser (Sep 11 2020 at 20:52):

I guess conv in (_ = _) { skip } gives the behavior I was after with sorry

Last updated: May 08 2021 at 09:11 UTC