instances and parameters

Stream: general

[Sebastien Gouezel]

I thought that typeclass inference could use information in the context to fill in parameters to instances. However, I can't get this to work.

class my_class (α : Type)

instance foo {x y : ℝ} [x < y] : my_class (Icc x y) := by constructor

instance bar {x y : ℝ} (h : x < y) : my_class (Icc x y) := by apply_instance

bar fails. Is there a way to solve this?

[Kenny Lau]

I don't think it's solvable

[Kevin Buzzard]

Is the issue that x<y isn't a typeclass?

[Kevin Buzzard]

Oh I see, this is the point

[Sebastien Gouezel]

So, you mean I should go for

class my_class (α : Type)

def le_class (x y : ℝ) : Prop := x < y

attribute [class] le_class

instance foo {x y : ℕ} [le_class x y] : my_class (Icc x y) := by constructor

instance bar {x y : ℕ} (h : le_class x y) : my_class (Icc x y) := by apply_instance

This is a little bit sad, but it works...

[Sebastien Gouezel]

Would it be possible in Lean 4 to allow for normal parameters in instances, where instance search would only be allowed to look in the context to fill these parameters, instead of going on with the search?

[Patrick Massot]

That would be really nice.

[Kevin Buzzard]

I half-started typing "maybe you could make a wrapper def and make it a class" but then I thought it would probably be so horrible to use in practice that I had better not mention it!

[Reid Barton]

I learned this week that something much more general is planned for Lean 4: you will be able to invoke tactics from instances using auto_params, like

instance bar {x y : ℝ} (h : x < y . my_tac) : my_class (Icc x y) := by apply_instance

I would guess something along the lines of def my_tac := tactic.linarith <|> tactic.assumption would solve most of your goals automatically, and the rest manually, provided you can stuff the proof you need into the environment somehow.

[Reid Barton]

(I don't think it ever occurred to me to even try this in Lean 3, but I just confirmed that it in fact does not work currently.)

[Patrick Massot]

Where did you see that in Lean 4?

[Reid Barton]

I was at MSR for the past week.

[Patrick Massot]

Did you tell Lean 4 everything you know about IMO problem solving?

[Reid Barton]

But this is my favorite tidbit. Also consider the possibility of coercing to a bundled morphism, with a tactic which synthesizes the proof of continuity, or whatever.

[Patrick Massot]

Do they have tests suggesting this won't kill type class search performance?

[Reid Barton]

Did you tell Lean 4 everything you know about IMO problem solving?

Well, the reason this feature is only planned so far is that there is no mechanism at all to invoke tactics (begin ... end) yet, so it's a bit premature to communicate with Lean 4 directly

[Patrick Massot]

Yeah I know, this (and VScode extension) is why we cannot play with Lean 4 yet.

[Mario Carneiro]

I don't think the problem has ever been about performance. Certainly tactics should be used sparingly and fail fast in such a context, but when I talked about this with leo early in lean 3 his concern was that this will make type class searches nondeterministic (so caching is not necessarily safe anymore)

[Reid Barton]

Do they have tests suggesting this won't kill type class search performance?

Of course it will be bad if the tactic itself is expensive, but based on what I understand about the new instance search procedure, I expect the tactic will be invoked at most once per specific goal per query.

[Mario Carneiro]

it actually might be nice for the typeclass search itself to have the conditions for applicability of the tactic already available. I guess if you want this to work using auto_param instances, you would need a dummy blanket instance like instance (h : continuous f . cont_tac) : continuous f

[Daniel Selsam]

Here is the current plan: when typeclass resolution encounters a precondition in an instance whose head unifies with a goal, it will create a metavariable for the proof and move on as if the precondition had been proved. If typeclass inference eventually succeeds, the elaborator will call any registered tactics to instantiate those metavariables (i.e. to prove the preconditions), and will throw a (good) error message if any of these tactics fail. This plan will not handle cases where different instances are desired depending on whether or not certain preconditions are provable. Interleaving typeclass resolution and tactic invocation would add a lot of complexity and we do not intend to support it. However, we would potentially consider supporting it if there were very valuable uses of typeclasses that require it. If anyone has any such examples, now is the time to share.

[Mario Carneiro]

I assume tactics can still call apply_instance?

[Daniel Selsam]

I assume tactics can still call apply_instance?

Yes, that direction is fine.

[Mario Carneiro]

So instances with auto_params always succeed then? A tactic that appears in an auto_param instance must handle the complete problem without failure?

[Mario Carneiro]

One example that comes to mind is Z/pZ. It would be nice if we could infer a field structure on Z/nZ if and only if n is prime

[Mario Carneiro]

This plan is effectively going to always assume that the primality check succeeds, but then the question is whether that leads to a bad proof sometimes. For example, maybe I want multiplication on Z/4Z, and the instance search does has_mul Z/4Z <- ring Z/4Z <- field Z/4Z <- defer proof that 4 is prime and "succeeds", then it runs the primality check, fails, and says "sorry, no multiplication found", even though let's say the instance it would have tried right after ring A <- field A was ring Z/nZ with no assumptions

[Daniel Selsam]

So instances with auto_params always succeed then?

Here is another way to think about it. Typeclass resolution will ignore preconditions and commit to the first instance it can synthesize (ignoring preconditions). Then the elaborator will call the registered tactics to synthesize the preconditions, and fail if they cannot be synthesized.

A tactic that appears in an auto_param instance must handle the complete problem without failure?

This is actually a separate issue, but I would suggest that the tactics must succeed completely. The alternative is for the elaborator to return subgoals as in Coq's refine, but I think this leads to unmaintainable code.

[Daniel Selsam]

This plan is effectively going to always assume that the primality check succeeds, but then the question is whether that leads to a bad proof sometimes. For example, maybe I want multiplication on Z/4Z, and the instance search does has_mul Z/4Z <- ring Z/4Z <- field Z/4Z <- defer proof that 4 is prime and "succeeds", then it runs the primality check, fails, and says "sorry, no multiplication found", even though let's say the instance it would have tried right after ring A <- field A was ring Z/nZ with no assumptions

Thanks, this is a great example of something that will not work reliably with the current plan.

[Daniel Selsam]

Workaround: make prime a class, with instances for whatever concrete primes you care about, and take [prime n] as an argument to instances instead of (prime n . <tac>). The typeclass resolution will also succeed for arbitrary n if prime n is in the context. Note: you only need to use the restricted [prime n] as an argument to instances, and can still use (prime n . <tac>) for non-instances.

[Mario Carneiro]

That is what we do today, or rather a slight variant in which Z/pZ is a newtype over Z/nZ with an additional argument with the proof of primality; this way the proof doesn't have to be inferred by type class inference. prime p has since become a class anyway, because of issues like this.

[Johan Commelin]

But at the moment you can't provide an instance of prime 2, because it is not 100% a class, I guess?

[Patrick Massot]

@Daniel Selsam did you also see the old discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cleaning.20iff/near/174233034?

[Daniel Selsam]

The following works on my fork of Lean4, no matter the order of the instance declarations:

@[class] def Prime (p : Nat) : Prop := p > 2 -- skipping the rest

@[instance] axiom p2 : Prime 2
@[instance] axiom p3 : Prime 3

@[class] axiom Field : Type → Type
@[class] axiom Ring : Type → Type

@[instance] axiom FieldToHasDiv (α : Type) [Field α] : HasDiv α
@[instance] axiom FieldToHasMul (α : Type) [Field α] : HasMul α
@[instance] axiom RingToHasMul (α : Type) [Ring α] : HasMul α

axiom mkType : Nat → Type

@[instance] axiom PrimeField (n : Nat) [Prime n] : Field (mkType n)
@[instance] axiom NonPrimeRing (n : Nat) : Ring (mkType n)

axiom fooCP2R (α β : mkType 2) : α * β = β * α
axiom fooCP2F (α β : mkType 2) : α / β = β / α
axiom fooCN2R (α β : mkType 4) : α * β = β * α
axiom fooAN2R (n : Nat) (α β : mkType n) : α * β = β * α
axiom fooAP2R (n : Nat) (nPrime : Prime n) (α β : mkType n) : α * β = β * α
axiom fooAP2F (n : Nat) (nPrime : Prime n) (α β : mkType n) : α / β = β / α

Also, it should already work on Lean4::master and presumably Lean3 if you make Prime an explicit class:

class Prime (p : Nat) : Prop := (spec : ...)

[Daniel Selsam]

Workaround: make prime a class ...

I called this a "workaround" last night but I now think it is actually a good solution. Suppose you tried to write (x y : Z/<huge concrete number>Z) and then wrote x / y. Would you really want / to do primality testing behind the scenes?

[Patrick Massot]

Primality testing is much easier than prime factorization, but it's still a valid point.

[Mario Carneiro]

Doesn't it cache instance searches?

[Daniel Selsam]

Primality testing is much easier than prime factorization, but it's still a valid point.

(updated)

[Daniel Selsam]

Doesn't it cache instance searches?

We don't know yet when and whether to cache typeclass resolution results in Lean4. We may not need to cache at all, since the resolution itself will be so much faster than in Lean3, but we'll see. Either way, it is bad style to depend on caching policies for reasonable performance when there exists a simple, reliable solution: instance : Prime <huge concrete number> := by primality_test.

[Patrick Massot]

Daniel, among all those wonders of type class resolution, could you also try to improve error reporting? When Lean 3 fails to infer an instance then most of the time we don't even know which instance it was trying to infer.

[Daniel Selsam]

Daniel, among all those wonders of type class resolution, could you also try to improve error reporting? When Lean 3 fails to infer an instance then most of the time we don't even know which instance it was trying to infer.

Thanks for pointing this out. There is low-hanging fruit in improving these messages, but reliable debugging probably requires more than just better error messages, e.g. much better tracing. We still don't have a plan for tracing in general but we are actively discussing it.

[Daniel Selsam]

By low-hanging fruit, I mean improvements that can be made relatively locally, independent of any major refactor such as tracing. And yes, we will make those improvements no matter what we decide about tracing.