rw not rw'ing

Stream: new members

[Jake Kesinger]

In this code:

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


@[simp]
lemma prod_inv_flip_is_inv {R:Type*} (a:R) (b:R) [field R] (anz:a≠0)(bnz:b≠0): (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:a≠0)(bnz:b≠0) (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.

[Jake Kesinger]

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

[Reid Barton]

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

[Reid Barton]

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

[Jake Kesinger]

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

[Kevin Buzzard]

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

[Jake Kesinger]

trying to minimize now

[Jake Kesinger]

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:a≠0)(bnz:b≠0): (a*b)⁻¹ = b⁻¹ * a⁻¹ :=
by {field_simp}

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

@[simp]
lemma prod_inv_cancel_right {R:Type*} (a:R) (b:R) (x:R) [field R] (anz:a≠0)(bnz:b≠0) (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

[Floris van Doorn]

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.

[Simon Hudon]

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

[Floris van Doorn]

#4846

[Simon Hudon]

Thanks!