fun_prop unexpected bound variable #0

Stream: mathlib4

[llllvvuu]

does anyone know how to interpret the error message "unexpected bound variable #0" in this context?

import Mathlib

attribute [fun_prop] Real.continuous_fourierChar
attribute [fun_prop] IsROrC.continuous_re
attribute [fun_prop] IsROrC.continuous_im

[Tomas Skrivan]

It is a bug in fun_prop :) The tactic is still rough around the edges ,I will look into it.

[Thomas Murrills]

Hope you don't mind, I debugged this partially for fun in case it helps (you may have reached the same conclusion by now!): it seems that we index out of bounds when writing let yVal := args[argId]! in splitMorToCompOverArgs. In the example using IsROrC.continuous_re, argId is 5, but args has size 3 (#[K, inst, x]).

(The error message is because the default element of Expr is .bvar 0, which is what [_]! uses when out of bounds. On the web interface the panic isn't passed through.)

[Thomas Murrills]

Here's a #mwe:

import Mathlib.Tactic.FunProp.Attr

set_option autoImplicit true

@[fun_prop] def Test (f : α → Nat) : Prop := sorry

structure F (α β: Type) where
  imp : α → β

def f : F α β  := sorry

instance : DFunLike (F α β) α (fun _ => β) where
  coe := fun ⟨imp⟩ => imp
  coe_injective' := sorry

theorem test_thm {α} : Test (f : α → Nat) := sorry

attribute [fun_prop] test_thm

[Tomas Skrivan]

Ohh thanks for figuring out what went wrong :) I just tested in on my new version of fun_prop which has much cleaner implementation and the problem is gone.

[llllvvuu]

Nice! What command(s) do you use for debugging this sort of thing?