bug in `conv?`

Stream: mathlib4

[Kevin Buzzard]

conv? usually works great for me but I ran into a bug yesterday which I have taken some time to minimise because I thought @Patrick Massot might be interested. I explain it all in the MWE below but basically conv? seems to have
an off-by-one error when faced with a goal which has a typeclass instance in it. I'm sure it can be minimised much further but when I started on this an hour ago
myClass was IsHaarMeasure and it took me a long time to get rid of the
measure theory import whilst preserving the bug, so hopefully I've done enough.

import Mathlib.Tactic.Widget.Conv

class myType : Type where
  n : Nat

def mymap (φ : Bool) (α : myType) : myType := α

-- this class plays a key role
class myClass (μ : myType) : Prop

-- let's make it always true
instance (μ : myType) : myClass μ where

-- the `[myClass μ]` instance in hSF is essential for the bug
def hSF (μ' μ : myType) [myClass μ] : Int := sorry

theorem bug_in_conv_questionmark (μ α β : myType) (φ : Bool) :
    hSF α (mymap φ α) = hSF (mymap φ μ) μ := by
  -- the goal is some statement with two `α`s.
  -- I want to rewrite the second one with a `β`.
  have smul : α = β := sorry
  -- here's the goal with the second `α` replaced by a `β`.
  have foo : hSF α (mymap φ β) = hSF (mymap φ μ) μ := sorry
  /-
  The goal is currently

  ⊢ hSF α (mymap φ α) = hSF (mycomap φ μ) μ

  so it has two `α`s in. I would like to `rw [smul]` at the second `α`
  using `conv` (in my application things are much more complicated and I can't
  use `rw` or `simp only` for reasons I won't go into (`β` depends on `α`,
  motive is not type correct etc), but `conv?` is perfect for this (indeed when
  I fix the bug manually in my application `conv` is working fine).

  But `conv?` fails to highlight the correct term. During the minimisation
  process, sometimes `conv?` succeeded and highlighted a different term (typically `φ`),
  and sometimes it just failed completely with error `Error: Not a valid conv target`.
  Right now, it's focussing on the `φ` just before `α`.
  -/
  conv? -- try clicking on the second `α` in the goal -- you'll end up
        -- focussed on the `φ` which is just before it.
  -- The code I want `conv?` to generate:
  conv =>
    enter [1, 2, 2] -- currently `conv?` produces `enter [1, 2, 1]`.
    rw [smul]
  -- this just checks that it worked:
  exact foo

[Patrick Massot]

I’ll try to find time to investigate this, but most of the work on this widget is not due to me. I mostly took it from the ProofWidget example folder. See https://github.com/leanprover-community/ProofWidgets4/blob/main/ProofWidgets/Demos/Conv.lean

[Patrick Massot]

@𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒 may know more about this issue.

[Aaron Liu]

conv? is very broken

[Aaron Liu]

I tried some simple tests and it failed most of them

[Patrick Massot]

@Aaron Liu could you create an issue in the Mathlib repo with examples of things that fail?

[Kevin Buzzard]

Yes, if you can easily make it fail then a much simpler example than mine would definitely be helpful! Do all your failures involve typeclasses? For me that was what triggered the problem.

[Jovan Gerbscheid]

The following is generated by conv?:

import Mathlib

example (h : ∃ i : Nat, i = 8) : False := by
  conv at h =>
    enter [2, 2]

But what works is:

import Mathlib

example (h : ∃ i : Nat, i = 8) : False := by
  conv at h =>
    enter [1, i]

[Aaron Liu]

Patrick Massot said:

Aaron Liu could you create an issue in the Mathlib repo with examples of things that fail?

#25162

[Aaron Liu]

I fixed this in #25889