## Stream: general

### Topic: ac_refl

#### Greg Price (Apr 02 2021 at 05:05):

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 (Apr 02 2021 at 05:06):

Replacing the ac_refl by rw mul_comm successfully closes the goal.

#### Greg Price (Apr 02 2021 at 05:07):

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 (Apr 02 2021 at 05:08):

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

#### Greg Price (Apr 02 2021 at 05:08):

Hmm I'll double-check!

#### Greg Price (Apr 02 2021 at 05:10):

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

#### Greg Price (Apr 02 2021 at 05:11):

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 (Apr 02 2021 at 05:11):

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

#### Yakov Pechersky (Apr 02 2021 at 05:24):

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

#### Greg Price (Apr 02 2021 at 05:24):

Haha oof.

Thanks! How did you track that down?

#### Greg Price (Apr 02 2021 at 05:25):

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 (Apr 02 2021 at 05:26):

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

#### Yakov Pechersky (Apr 02 2021 at 05:27):

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 (Apr 02 2021 at 05:27):

Ah excellent, thanks.

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

#### Greg Price (Apr 02 2021 at 05:29):

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.

Last updated: Aug 03 2023 at 10:10 UTC