Zulip Chat Archive

Stream: general

Topic: Rewriting under forall with conv


view this post on Zulip 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.

view this post on Zulip Chris Hughes (Sep 11 2020 at 20:29):

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

view this post on Zulip Chris Hughes (Sep 11 2020 at 20:31):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 11 2020 at 20:34):

I believe it's congr

view this post on Zulip Eric Wieser (Sep 11 2020 at 20:34):

congr by itself throws away the entire expression

view this post on Zulip Bryan Gin-ge Chen (Sep 11 2020 at 20:35):

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

view this post on Zulip 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
}

view this post on Zulip 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

view this post on Zulip Eric Wieser (Sep 11 2020 at 20:39):

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

view this post on Zulip Kenny Lau (Sep 11 2020 at 20:41):

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

view this post on Zulip Chris Hughes (Sep 11 2020 at 20:43):

funext is for lambdas, this would be piext

view this post on Zulip Chris Hughes (Sep 11 2020 at 20:43):

Which doesn't exist

view this post on Zulip Eric Wieser (Sep 11 2020 at 20:45):

Just doesn't, or also can't?

view this post on Zulip Reid Barton (Sep 11 2020 at 20:45):

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

view this post on Zulip Reid Barton (Sep 11 2020 at 20:45):

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

view this post on Zulip Kenny Lau (Sep 11 2020 at 20:46):

yeah conv is highly incomplete and buggy

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 11 2020 at 20:47):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Sep 11 2020 at 20:48):

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

view this post on Zulip Reid Barton (Sep 11 2020 at 20:50):

oh weird

view this post on Zulip 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

view this post on Zulip 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