instance with tactic autoparam

Stream: lean4

[James Gallicchio]

is there a way to get something like this working?

instance (h : n < UInt8.size := by decide) : CoeDep Char (Char.ofNat n) UInt8 where
  coe := ⟨n, h⟩

#check (instCoeDepCharOfNatUInt8 : CoeDep Char 'a' UInt8)
#synth CoeDep Char 'a' UInt8

the synth line fails unfortunately

[James Gallicchio]

Oh wait, meant for this to be in #lean4 if someone is able to move it >_<

[Notification Bot]

This topic was moved here from #mathlib4 > instance with tactic autoparam by Eric Wieser.

[Alex Keizer]

I don't think you can use decide like that, but you can trick the typeclass synthesis system into proving such inequalities. E.g., the following is part of mathlib (https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Fin/Fin2.lean)

/-- This is a simple type class inference prover for proof obligations
  of the form `m < n` where `m n : ℕ`. -/
class IsLT (m n : ℕ) where
  /-- The unique field of `Fin2.IsLT`, a proof that `m < n`. -/
  h : m < n
#align fin2.is_lt Fin2.IsLT

instance IsLT.zero (n) : IsLT 0 (succ n) :=
  ⟨succ_pos _⟩

instance IsLT.succ (m n) [l : IsLT m n] : IsLT (succ m) (succ n) :=
  ⟨succ_lt_succ l.h⟩

/-- Use type class inference to infer the boundedness proof, so that we can directly convert a
`Nat` into a `Fin2 n`. This supports notation like `&1 : Fin 3`. -/
def ofNat' : ∀ {n} (m) [IsLT m n], Fin2 n
  | 0, _, ⟨h⟩ => absurd h (Nat.not_lt_zero _)
  | succ _, 0, ⟨_⟩ => fz
  | succ n, succ m, ⟨h⟩ => fs (@ofNat' n m ⟨lt_of_succ_lt_succ h⟩)
#align fin2.of_nat' Fin2.ofNat'

[James Gallicchio]

I'm a bit worried doing that, just because chars get kind of big sometimes and I don't want tc synthesis to have to synthesize a chain of 200 elements instead of calling a dedicated tactic :/

[James Gallicchio]

maybe this is a feature request, heh

[Eric Wieser]

You could generate 256 instances instead for a chain length of 1

[Alex Keizer]

Being able to use autoparams for effectively running custom code as part of typeclass synthesis would be a very useful and powerful feature for sure.

[Eric Wieser]

Eric Wieser said:

You could generate 256 instances instead for a chain length of 1

Given you can do this with a macro and write only a handful of lines of code, I think this is a perfectly reasonable hack for UInt8; though I wouldn't advise it for Uint16

[Gabriel Ebner]

You can do this in a roundabout way:

class Decide (p : Prop) [Decidable p] : Prop where
  isTrue : p

instance : @Decide p (.isTrue h) := @Decide.mk p (_) h

instance [Decide (n < UInt8.size)] : CoeDep Char (Char.ofNat n) UInt8 where
  coe := ⟨n, Decide.isTrue⟩

#check ('a' : UInt8)

[Eric Wieser]

How much reduction does this perform onDecidable instances to work out if they match isTrue?

[Gabriel Ebner]

Decidable p is an instance-implicit argument, so it is unified with semireducible transparency.

[Gabriel Ebner]

It's essentially the same thing that by decide does under the hood.

[James Gallicchio]

ah, very cool, that should work for my purposes

[Sebastian Ullrich]

James Gallicchio said:

is there a way to get something like this working?

The short answer from an implementation view is: the mutual recursion between typeclass synthesis and unification is already one of the most complicated parts of the system. Adding tactic execution to the mix would make the complexity explode, and likely complicate caching as well.

[James Gallicchio]

It seems very reasonable to keep it limited to decide esque problems -- anything beyond that feels like too much to expect tc synthesis to do. Maybe we can add the Decide class to Std.

[Mario Carneiro]

I still think that we should just allow tactic execution there, but require of implementers that the tactic must be pure, because the result will be cached just like a typeclass resolution problem

[Mario Carneiro]

Disallowing tactics just causes people to implement execution more poorly using the typeclass system. There are many cases where you can do significantly better with a custom automation

[Alex Keizer]

For example, my project often has typeclass problems of the form \all (i : Fin 3), Foo (f i), (where the 3 might be any concrete, known number) which I want to automatically be inferred from instances of Foo (f 0), Foo (f 1) and Foo (f 2). This is doable by having a chain of instances, effectively doing induction on the Fin (but even then I had to add an auxiliary typeclass, or the synthesis would somehow fail).
I would love to just say something like by intro i; fin_cases i; inferInstance