ac_refl

Stream: general

[Greg Price]

I seem to be looking at a bug in ac_refl. Does this pattern of behavior look familiar to anyone?

It's failing at an equality that is indeed just a matter of commutativity:

example (r x : ℝ) (hne : r ≠ 0) (hx1 : -r < x) (hx2 : x < r)
  : deriv arcsin ((r)⁻¹ * x) / r = (r)⁻¹ / sqrt ((r ^ 2 - x ^ 2) / r ^ 2) :=
by {
  field_simp,
  /-
  ac_refl failed
  state:
  r x : ℝ,
  hne : r ≠ 0,
  hx1 : -r < x,
  hx2 : x < r
  ⊢ 1 / (sqrt ((r ^ 2 - x ^ 2) / r ^ 2) * r) = 1 / (r * sqrt ((r ^ 2 - x ^ 2) / r ^ 2))
  -/
  ac_refl,
}

[Greg Price]

Replacing the ac_refl by rw mul_comm successfully closes the goal.

[Greg Price]

This behavior seems to have some kind of interaction going on with state that field_simp leaves behind which isn't immediately visible. If we start directly from what the infoview says is the goal state at that point:

example (r x : ℝ) (hne : r ≠ 0) (hx1 : -r < x) (hx2 : x < r)
  : 1 / (sqrt ((r ^ 2 - x ^ 2) / r ^ 2) * r) = 1 / (r * sqrt ((r ^ 2 - x ^ 2) / r ^ 2)) :=
by {
  ac_refl,
}

then it succeeds, just as one would hope.

[Yakov Pechersky]

when you make that example, are you sure your numerals are the same type as in your failing goal?

[Greg Price]

Hmm I'll double-check!

[Greg Price]

Looks like the 1 numerators are of type ℝ in both cases.

[Greg Price]

And the 2 exponents are of type ℕ.

And the 0 in a hypothesis is of type ℝ too.

So it seems like the types all match between the two cases.

[Greg Price]

That's based on hovering over them in the infoview.

[Yakov Pechersky]

Turns out the second 1 is different, it comes from monoid.has_one instead of real.has_one.

[Greg Price]

Haha oof.

Thanks! How did you track that down?

[Greg Price]

Ah I see, that's also there in the little box in the infoview that I get when I click on that subexpression.

[Yakov Pechersky]

I tracked it down by doing set_option pp.all true before the examples and then trying to see a difference

[Yakov Pechersky]

The two are supposedly defeq, so now it's a question of what's going on in ac_refl:

example : (monoid.to_has_one ℝ).one = (real.has_one).one := rfl -- works
example : (monoid.to_has_one ℝ).one = (real.has_one).one := by ac_refl -- fails

[Greg Price]

Ah excellent, thanks.

Wow yeah, with that it really jumps out that there is a difference.

[Greg Price]

I tried to take a peek at the implementation of ac_refl, but it looks like it's mostly behind meta constant declarations. I'm guessing that means the implementation is in C++ and not in Lean.