Zulip Chat Archive

Stream: new members

Topic: rw not rw'ing


view this post on Zulip Jake Kesinger (Oct 30 2020 at 23:40):

In this code:

@[simp]
lemma prod_inv_flip {R:Type*} (a:R) (b:R) [field R] (anz:a0)(bnz:b0): (a*b)⁻¹ = b⁻¹ * a⁻¹ :=
begin
  field_simp,
end


@[simp]
lemma prod_inv_flip_is_inv {R:Type*} (a:R) (b:R) [field R] (anz:a0)(bnz:b0): (a*b)⁻¹ * b * a = 1 :=
begin
finish
end

@[simp]
lemma prod_inv_cancel_right {R:Type*} (a:R) (b:R) (x:R) [field R] (anz:a0)(bnz:b0) (xnz: x 0):
x * (a*b)⁻¹*b*a = x :=
begin
  rw prod_inv_flip_is_inv a b,
sorry,
end

the rw prod_inv_flip_is_inv a b is failing, and I'm not understanding why.

view this post on Zulip Jake Kesinger (Oct 30 2020 at 23:41):

I tried set option pp.all true and got this message:

Rewrite tactic failed, did not find instance of the pattern in the target expression
  @has_mul.mul.{u_1} R
    (@distrib.to_has_mul.{u_1} R
       (@ring.to_distrib.{u_1} R (@division_ring.to_ring.{u_1} R (@field.to_division_ring.{u_1} R _inst_1))))
    (@has_mul.mul.{u_1} R
       (@distrib.to_has_mul.{u_1} R
          (@ring.to_distrib.{u_1} R (@division_ring.to_ring.{u_1} R (@field.to_division_ring.{u_1} R _inst_1))))
       (@has_inv.inv.{u_1} R (@field.to_has_inv.{u_1} R _inst_1)
          (@has_mul.mul.{u_1} R
             (@distrib.to_has_mul.{u_1} R
                (@ring.to_distrib.{u_1} R (@division_ring.to_ring.{u_1} R (@field.to_division_ring.{u_1} R _inst_1))))
             a
             b))
       b)
    a

view this post on Zulip Reid Barton (Oct 30 2020 at 23:42):

That's because (despite where you put the spaces :upside_down:) x * (a*b)⁻¹*b*a means ((x * (a*b)⁻¹)*b)*a.

view this post on Zulip Reid Barton (Oct 30 2020 at 23:43):

There is actually another tactic for dealing with this exact issue: assoc_rw

view this post on Zulip Jake Kesinger (Oct 31 2020 at 00:00):

thanks!
assoc_rw did the trick, and with ring I was able to finish all goals, but I was getting failures saying "result contains meta-variables".
I found in another thread the recover goal, and from that was able to call exact a couple times to clear hypotheses, but the "For debugging only" in the description of recover is making me nervous

view this post on Zulip Kevin Buzzard (Oct 31 2020 at 00:05):

This is normally down to a buggy tactic. Can you post a #mwe?

view this post on Zulip Jake Kesinger (Oct 31 2020 at 00:13):

trying to minimize now

view this post on Zulip Jake Kesinger (Oct 31 2020 at 00:18):

import data.real.basic

namespace mwe

@[simp]
lemma abcd_is_adbc {R:Type*} (a:R) (b:R) (c:R) (d:R) [comm_monoid R] : a*b*c*d = a*d*b*c :=
begin
finish
end

@[simp]
lemma prod_inv_flip {R:Type*} (a:R) (b:R) [field R] (anz:a0)(bnz:b0): (a*b)⁻¹ = b⁻¹ * a⁻¹ :=
by {field_simp}

@[simp]
lemma prod_inv_flip_is_inv {R:Type*} (a:R) (b:R) [field R] (anz:a0)(bnz:b0): (a*b)⁻¹ * b * a = 1 :=
by {finish}

@[simp]
lemma prod_inv_cancel_right {R:Type*} (a:R) (b:R) (x:R) [field R] (anz:a0)(bnz:b0) (xnz: x 0):
x * (a*b)⁻¹*b*a = x :=
begin
  assoc_rw prod_inv_flip_is_inv a b,
  ring,
  recover,
  exact bnz,
  exact anz,
end

end mwe

view this post on Zulip Floris van Doorn (Oct 31 2020 at 03:40):

It seems like assoc_rw doesn't handle hypotheses well in a partially applied term. @Simon Hudon

As a workaround, assoc_rw prod_inv_flip_is_inv a b _ _ produced 3 goals as expected.

view this post on Zulip Simon Hudon (Oct 31 2020 at 03:50):

Would you mind filing a bug with this information and tagging me?

view this post on Zulip Floris van Doorn (Oct 31 2020 at 03:52):

#4846

view this post on Zulip Simon Hudon (Oct 31 2020 at 03:59):

Thanks!


Last updated: May 06 2021 at 22:13 UTC