Rewriting under forall with conv

Stream: general

[Eric Wieser]

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]

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

[Chris Hughes]

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

[Eric Wieser]

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

[Kenny Lau]

I believe it's congr

[Eric Wieser]

congr by itself throws away the entire expression

[Bryan Gin-ge Chen]

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

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Kenny Lau]

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

[Chris Hughes]

funext is for lambdas, this would be piext

[Chris Hughes]

Which doesn't exist

[Eric Wieser]

Just doesn't, or also can't?

[Reid Barton]

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

[Reid Barton]

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

[Kenny Lau]

yeah conv is highly incomplete and buggy

[Eric Wieser]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

oh weird

[Reid Barton]

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

[Eric Wieser]

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