Zulip Chat Archive

Stream: new members

Topic: How to use a type alias without breaking typeclass synthesis


view this post on Zulip Marko Grdinić (Oct 25 2019 at 09:58):

def History : Type* := {die // die  dice} × list {i //  v, claims.read i = v}

def ha : HistoryToActions ({die // die  dice} × list {i //  v, claims.read i = v}) Action
    | (_, []) :=  actions.begin.1, actions.begin.read 
    | (_, x :: xs) := let v := actions.later.drop (x.1 + 1) in  v.1, v.read 

structure Particle (α : Type*) := mk ::
    (state : α)
    (probability : )
    (infosets : Infosets ha)
    (is_updateable : bool)

This piece of code typechecks as written above, but when I replace {die // die ∈ dice} × list {i // ∃ v, claims.read i = v} with History in ha's type, I get an error that it cannot synthesize the typeclass instances for (infosets : Infosets ha). The particular typeclass instance is has_lt History. What should I do here?

instance : has_lt History := by {unfold History, }

Also, it occurred to me that I could try providing it directly, but I am not sure which tactic to use here. Even if this could work, I'd prefer it if I could instruct the compiler to inline the alias rather than doing this.

Sorry about not giving a simplified example - I gave it a shot, but there are a lot of hierarchies that I do not know how to pare down without significant effort.

view this post on Zulip Rob Lewis (Oct 25 2019 at 10:00):

instance : has_lt History := by {unfold History, apply_instance}

view this post on Zulip Rob Lewis (Oct 25 2019 at 10:00):

Alternatively, @[derive has_lt] def History : Type* := ...

view this post on Zulip Marko Grdinić (Oct 25 2019 at 10:03):

Thanks!

view this post on Zulip Marko Grdinić (Oct 25 2019 at 12:29):

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

The advice worked for my previous problem, but now I am running into this issue. I am not even sure for which typeclass instance it is looking for. How do I find that out? I tried turning on the trace, but the instance it is looking for there should be available, so I am thinking it should be something else.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 12:41):

Also, is it possible to derive decidable_rel using the first form? Something like...@[derive has_lt, derive decidable_rel] def Die := {die // die ∈ dice}? The issue with decidable_rel is that it depends on has_lt.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 13:10):

@[derive has_lt] def Die := {die // die  dice}
@[derive has_lt] def PastClaims := list {i //  v, claims.read i = v}
@[derive has_lt] def History := Die × PastClaims

I need decidable_rel for these 3, but forget about the previous question for a bit. I thought I would be able to do it once I made up my mind, but now that I am trying I find I have absolutely no idea how Lean deals with decidability of propositions. I am not even sure how it would work for regular nats and not these slightly more complex structures.

How should I do this? I could use some good examples of how decidable_rel works.

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 13:20):

It's impossible to debug a max class instance error without a fully working example demonstrating the error.

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 13:21):

You can turn certain traces on and look at debug output, but you have to know what you're looking for.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 13:25):

@Kevin Buzzard

I see. Well in this case, I am sure that the problem is because it is looking for the missing decidable_rel for History. I managed to track it down by using @ on the offending function and manually checking all the arguments.

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 13:27):

Type class inference is complicated and is going to be one of the big changes in Lean 4. There are people here who know how to work with what we have, and no doubt they could sort out your specific problem if any of them had the time, but we have also been collecting lists of when typeclass inference fails or works badly, and the devs are going to see if they can come up with something better in Lean 4. It's being implemented right now, is my understanding.

view this post on Zulip Rob Lewis (Oct 25 2019 at 13:30):

History isn't a relation, is it? You can't give it a decidable_rel instance.

view this post on Zulip Rob Lewis (Oct 25 2019 at 13:31):

You might be able to derive decidable equality. @[derive [has_lt, decidable_eq]]. You'd need this to be successful on Die and PastClaims first to have any hope on History.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 13:32):

@Rob Lewis

History isn't a relation, is it? You can't give it a decidable_rel instance.

No, I meant for the a < b where a b : History.

instance History_decidable_rel [x : has_lt History] : decidable_rel x.lt := sorry

Something like this.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 13:36):

@[derive [has_lt, decidable_eq]] def Die := {die // die  dice}
@[derive [has_lt, decidable_eq]] def PastClaims := list {i //  v, claims.read i = v}
@[derive [has_lt, decidable_eq]] def History := Die × PastClaims

This works for me. But decidable_rel is tricky in that it needs to be passed the specific has_lt instance by hand. That is how it was in the few places where I used it. So just putting @[derive [has_lt, decidable_rel]] def Die := {die // die ∈ dice} fails for me.

type mismatch at application
  decidable_rel Die
term
  Die
has type
  Type : Type 1
but is expected to have type
  ?m_1 → ?m_1 → Prop : Sort (max ? 1)

It seems this mechanism is passing it Die directly rather than the less-than function for Die.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 13:38):

def response { 𝔸 : Type*} [lt : has_lt ] [decidable_rel lt.lt]

I have a bunch of functions like this one where I declare that a type has has_lt and then also that the relation is decidable.

view this post on Zulip Rob Lewis (Oct 25 2019 at 13:38):

Ah. Yeah, the derive handler definitely won't work for that. You'll need to define it manually and unfold enough so that apply_instance sees the decidability. Something like instance History_decidable_rel : decidable_rel ((<) : History -> History -> Prop) := ...

view this post on Zulip Rob Lewis (Oct 25 2019 at 13:39):

Where ... does some unfolding and then calls apply_instance.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 13:47):

I am following your advice.

instance nat_decidable_rel : decidable_rel ((<) : nat  nat  Prop) :=
    by {
        intros a b,
        apply_instance
    }

As a sanity check this does work for nats.

@[derive has_lt] def Die := {die // die  dice}
instance Die_decidable_rel : decidable_rel ((<) : Die  Die  Prop) :=
    by {
        intros a b,
        apply_instance
    }
Tactic State
1 goal
a b : Die
⊢ decidable (a < b)
dudo.lean:29:8: error
tactic.mk_instance failed to generate instance for
  decidable (a < b)
state:
a b : Die
⊢ decidable (a < b)

For Die not so much. It cannot find the instance. I am trying to see whether I can get it to so it only compares the first argument (which is a nat), but I cannot unfold has_lt.lt here. What should I do?

view this post on Zulip Marko Grdinić (Oct 25 2019 at 14:14):

def Die := {die // die  dice}
instance Die_has_lt : has_lt Die :=  fun a b, a.val < b.val 
instance Die_decidable_rel : decidable_rel ((<) : Die  Die  Prop) := infer_instance

I get it now. I won't be sure until I go over the subtype, but it seems that the default has_lt was not good for my use case. I should be able to make this work now.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 14:17):

Hmmm...I can't find anything on has_lt for subtypes in the core library's init.data.subtype folder. There is no much there. Is it somewhere else? If so, where?

view this post on Zulip Marko Grdinić (Oct 25 2019 at 14:19):

Is there any way to track down the instance that is being inferred?

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

Hmmm...I can't find anything on has_lt for subtypes in the core library's init.data.subtype folder. There is no much there. Is it somewhere else? If so, where?

Are you using mathlib?

view this post on Zulip Reid Barton (Oct 25 2019 at 14:24):

A bit convoluted, but you can write, for example,

def x : has_lt nat := by apply_instance
#print x

which will print nat.has_lt, then

#check nat.has_lt

which will output something you don't care about, but now you can use jump-to-definition on nat.has_lt

view this post on Zulip Marko Grdinić (Oct 25 2019 at 14:33):

Apparently, the function is preorder.to_has_lt.

class preorder (α : Type u) extends has_le α, has_lt α :=
(le_refl :  a : α, a  a)
(le_trans :  a b c : α, a  b  b  c  a  c)
(lt := λ a b, a  b  ¬ b  a)
(lt_iff_le_not_le :  a b : α, a < b  (a  b  ¬ b  a) . order_laws_tac)

When I try to track it down by Ctrl + left click, it just puts me at the class definition. I am not sure where to go from there.

view this post on Zulip Reid Barton (Oct 25 2019 at 14:34):

Ah, in that case try set_option pp.all true before the #print, and try to guess where the actual instance is, or post the output here

view this post on Zulip Reid Barton (Oct 25 2019 at 14:37):

preorder.to_has_lt extracts the has_lt instance from a preorder instance

view this post on Zulip Reid Barton (Oct 25 2019 at 14:38):

it's automatically generated by that class preorder declaration

view this post on Zulip Marko Grdinić (Oct 25 2019 at 14:40):

Ah, I see. So that is why I get sent to the typeclass definition. I guess the question now becomes of how to track down where the subtype is declared as a preorder.

view this post on Zulip Marko Grdinić (Oct 25 2019 at 14:42):

Then I would be able to find the implementation of has_lt for it. What would be the best way to do this?

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 15:06):

Are you talking about why nat is a preorder? You can just use the trick Reid showed you again:

def x : preorder  := by apply_instance
#print x -- partial_order.to_preorder ℕ

The preorder on nat comes from the partial order on nat.


Last updated: May 13 2021 at 21:12 UTC