Problem in conv

Stream: mathlib4

[Michael Stoll]

mport Mathlib

example (z : ℂ) : Complex.abs z = Complex.abs z := by
  conv => -- obtained by `conv?` and shift-clicking on the first `z`
   enter [1, 2] -- error `cannot select argument`
  sorry

enter [1]gives | ↑Complex.abs z, and enter [1,1] gives | Complex.abs. How do I reach the argument z?
enter [1, 3] gives the (expected) error invalid 'arg' conv tactic, application has only 2 (nondependent) argument(s).

[Alex J. Best]

The issue is with the conv mode congr tactic. It should ideally produce two conv goals when applied here, one for the function being FunLiked and one for the argument. Unfortunately It uses a weaker congruence lemma which doesn't allow the arguments to be different, so only returns the goals of the differences between the functions. I don't see an obvious way to fix this easily, it looks like the non-conv congr is using hcongr under the hood to construct the better lemma, and this doesn't fit so nicely into the conv framework. Making a mathlib-free minimization and reporting to core would probably be the best way forward here

[Michael Stoll]

Now I have even managed to produce a PANIC in conv!
Using conv?, in the term

List.filter (fun x => decide ¬x < p) (factors m) ++ List.filter (fun x => decide (x < p)) (factors m) ~ factors m

I select ¬x < p, shift-click and "generate conv". This results in

PANIC at _private.Mathlib.Tactic.Widget.Conv.0.solveLevel Mathlib.Tactic.Widget.Conv:63:13: no name found

If I have time later today, I will try to minimize. (But I don't want to discourage everybody else :smile:)

[Michael Stoll]

It seems I cannot reproduce this in a clean test file. What I get with

import Mathlib

example (p m : ℕ) :
  List.filter (fun x => decide ¬x < p) (Nat.factors m) ++
    List.filter (fun x => decide (x < p)) (Nat.factors m) ~ Nat.factors m := by
  conv =>
   enter [1, 1, 1, x, 1]

(where the enterline was produced by the widget) is the error message

tactic 'refl' failed, metavariable has already been assigned

@Patrick Massot

[Kyle Miller]

It seems that conv's enter is actually just not capable of visiting every sub-expression.

I'm wondering if conv needs to be modified to support having Eq and HEq goals, which would let conv get into every argument

[Michael Stoll]

I just had the PANIC again. It seems likely to be triggered when there are fairly complicated terms.

[Michael Stoll]

I also noticed that conv? at h does not seem to work (whereas conv at h does).

[Patrick Massot]

conv? should let you select a subterm in the local context.

[Michael Stoll]

When I do that, conv? says "The selected sub-expression should be in the main goal."

[Michael Stoll]

E.g.,

example (n : ℕ) (h : n ^ 4 = n) : n ≤ 1 := by
  conv?
  sorry

select n ^ 4 (say) in h and shift-click.

[Patrick Massot]

@Michael Stoll I'm sorry, I misremembered. It should be fixed at #8217.