Tactics in typeclass instance parameters?

Stream: lean4

[Joey Eremondi]

I'm in the situation where I have a binary equivalence relation, that I'd like to use as a typeclass:

class inductive Rel (x y : T) where
| Refl : Rel x x
...

I'd like to have an instance that gives an instance of Rel x y whenever a proof of type x = y is in scope. I tried doing the following:

@[default_instance]
instance byEq {x y : T} (eq : x = y := by assumption) : Rel x y

But this doesn't work, for example, if I do

 let eq : x = y := by admit
 let foo : Rel x y := inferInstance

I get "failed to synthesize instance".

Is there a way to do it? Can I declare the equality proof to be a local instance somehow?

[Kevin Buzzard]

Those lets should be haves because they're proofs, but that's not your problem: your problem is that typeclass inference isn't ever going to look for an equality because equality isn't a typeclass. You would have to go via the Fact API and make eq a fact in order to get this working.

[Joey Eremondi]

@Kevin Buzzard Thanks, Fact looks like exactly what I want in this situation.

Do you know, does typeclass search only search through global instances? Is there a way to declare a hypothesis as a local instance in the middle of, e.g. a tactic script?

[Mario Carneiro]

typeclass search looks through the context, so have : Foo := ... is sufficient to make typeclass searches for Foo succeed

[Joey Eremondi]

@Mario Carneiro Good to know, that makes things work quite nicely!

One more question, is there a way to prevent backtracking in typeclass search?

For example, if I've got Symm : [Rel a b] -> Rel b a this will loop forever, especially in cases where Rel b a doesn't actually hold. Is there a way to say "see if we can find Rel b a in a single step, but don't backtrack further"?

[Mario Carneiro]

The usual way this is done is using more typeclasses, for example [Rel a b] -> RelSymm a b and [Rel a b] -> RelSymm b a

[Kevin Buzzard]

I thought that lean 4 allowed instance loops (i.e. could deal with them). Is this not the case?

[Mario Carneiro]

it does allow some simple instance loops, but I'm not sure how reliable the mechanism is

[Mario Carneiro]

a basic test seems to work

class Rel (a b : Nat) : Type

instance {a b} [Rel a b] : Rel b a := ⟨⟩
instance : Rel 1 1 := ⟨⟩
instance : Rel 1 4 := ⟨⟩

#synth Rel 1 1 -- ok
#synth Rel 1 2 -- failed
#synth Rel 1 4 -- ok
#synth Rel 4 1 -- ok