Zulip Chat Archive

Here are two versions of "the same" function, a simple list membership function. The item type is a parameter, along with an implicit proof of decidable equality for that type. In the first version, these arguments are given before the color. In the second version, they are given after the colon (and so two additional variables are also used in pattern matching, etc. The problem is that while the first version works, in the second, I get a typeclass inference error: Lean complains that it can't synthesize a typeclass instance for "decidable (h = i)," the condition in the if. Can you tell me what's the underlying problem here? Thank you!

def member'
    {item_type : Type u}
    [decidable_eq item_type]  :  -- COLON HERE
    list item_type → item_type → bool
| list.nil _ := ff
| (h::t) i :=
    if (h = i)      -- THIS IS FINE
    then tt
    else (@member' t i)

def member :        -- COLON NOW HERE
    ∀ {item_type : Type u}
    [decidable_eq item_type],
    list item_type → item_type → bool
| item_type e list.nil _ := ff
| item_type e (h::t) i :=
    if (h = i)     -- THIS IS NOT FINE
    then tt
    else (@member item_type e t i)

Ruben Van de Velde (Jul 15 2022 at 18:53):

Type class inference works with a cache that is populated at the colon, you'd need resetI or something like that

Kevin Sullivan (Jul 15 2022 at 18:54):

Ruben Van de Velde said:

Type class inference works with a cache that is populated at the colon, you'd need resetI or something like that

Hmm. Where would I learn more about resetI

Eric Wieser (Jul 15 2022 at 18:55):

tactic#resetI, maybe

Eric Wieser (Jul 15 2022 at 18:56):

https://leanprover-community.github.io/mathlib_docs/tactics.html#Instance%20cache%20tactics

Kyle Miller (Jul 15 2022 at 19:00):

You can use by exactI your_expression to have the instance cache be reset in the context of your_expression

Kevin Sullivan (Jul 15 2022 at 19:01):

Thank you, everyone.

Kevin Sullivan (Jul 15 2022 at 19:40):

Solution.

def member :
    ∀ {item_type : Type u}
    [decidable_eq item_type],
    list item_type → item_type → bool
| item_type e list.nil _ := ff
| item_type e (h::t) i :=
    by exactI (    --- HERE
        if (h = i)
        then tt
        else (@member item_type e t i)
    )

Reid Barton (Jul 15 2022 at 19:47):

You should not even need the parentheses (maybe barring some weird edge cases that aren't present here)

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib