Zulip Chat Archive

Stream: general

Topic: instances and parameters


view this post on Zulip Sebastien Gouezel (Oct 20 2019 at 18:57):

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?

view this post on Zulip Kenny Lau (Oct 20 2019 at 19:01):

I don't think it's solvable

view this post on Zulip Kevin Buzzard (Oct 20 2019 at 19:02):

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

view this post on Zulip Kevin Buzzard (Oct 20 2019 at 19:02):

Oh I see, this is the point

view this post on Zulip Sebastien Gouezel (Oct 20 2019 at 19:07):

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...

view this post on Zulip Sebastien Gouezel (Oct 20 2019 at 19:11):

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?

view this post on Zulip Patrick Massot (Oct 20 2019 at 19:16):

That would be really nice.

view this post on Zulip Kevin Buzzard (Oct 20 2019 at 19:48):

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!

view this post on Zulip Reid Barton (Oct 20 2019 at 20:44):

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.

view this post on Zulip Reid Barton (Oct 20 2019 at 20:45):

(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.)

view this post on Zulip Patrick Massot (Oct 20 2019 at 20:46):

Where did you see that in Lean 4?

view this post on Zulip Reid Barton (Oct 20 2019 at 20:46):

I was at MSR for the past week.

view this post on Zulip Patrick Massot (Oct 20 2019 at 20:47):

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

view this post on Zulip Reid Barton (Oct 20 2019 at 20:48):

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.

view this post on Zulip Patrick Massot (Oct 20 2019 at 20:50):

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

view this post on Zulip Reid Barton (Oct 20 2019 at 20:50):

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

view this post on Zulip Patrick Massot (Oct 20 2019 at 20:52):

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

view this post on Zulip Mario Carneiro (Oct 20 2019 at 20:53):

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)

view this post on Zulip Reid Barton (Oct 20 2019 at 20:55):

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.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 21:03):

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

view this post on Zulip Daniel Selsam (Oct 21 2019 at 03:51):

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.

view this post on Zulip Mario Carneiro (Oct 21 2019 at 04:02):

I assume tactics can still call apply_instance?

view this post on Zulip Daniel Selsam (Oct 21 2019 at 04:03):

I assume tactics can still call apply_instance?

Yes, that direction is fine.

view this post on Zulip Mario Carneiro (Oct 21 2019 at 04:05):

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

view this post on Zulip Mario Carneiro (Oct 21 2019 at 04:11):

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

view this post on Zulip Mario Carneiro (Oct 21 2019 at 04:15):

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

view this post on Zulip Daniel Selsam (Oct 21 2019 at 04:18):

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.

view this post on Zulip Daniel Selsam (Oct 21 2019 at 04:19):

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.

view this post on Zulip Daniel Selsam (Oct 21 2019 at 04:34):

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.

view this post on Zulip Mario Carneiro (Oct 21 2019 at 05:44):

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.

view this post on Zulip Johan Commelin (Oct 21 2019 at 07:03):

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

view this post on Zulip Patrick Massot (Oct 21 2019 at 07:48):

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

view this post on Zulip Daniel Selsam (Oct 21 2019 at 13:45):

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 : ...)

view this post on Zulip Daniel Selsam (Oct 21 2019 at 13:52):

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?

view this post on Zulip Patrick Massot (Oct 21 2019 at 13:58):

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

view this post on Zulip Mario Carneiro (Oct 21 2019 at 14:06):

Doesn't it cache instance searches?

view this post on Zulip Daniel Selsam (Oct 21 2019 at 14:13):

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

(updated)

view this post on Zulip Daniel Selsam (Oct 21 2019 at 14:19):

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.

view this post on Zulip Patrick Massot (Oct 21 2019 at 15:00):

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.

view this post on Zulip Daniel Selsam (Oct 21 2019 at 15:09):

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.

view this post on Zulip Daniel Selsam (Oct 21 2019 at 15:15):

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.


Last updated: May 13 2021 at 04:21 UTC