## Stream: new members

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

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

#### Rob Lewis (Oct 25 2019 at 10:00):

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

#### Rob Lewis (Oct 25 2019 at 10:00):

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

Thanks!

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

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

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

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

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

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

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

#### Rob Lewis (Oct 25 2019 at 13:30):

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

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

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

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

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

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

#### Rob Lewis (Oct 25 2019 at 13:39):

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

#### Marko Grdinić (Oct 25 2019 at 13:47):

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?

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

#### 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?

#### Marko Grdinić (Oct 25 2019 at 14:19):

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

#### 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?

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

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

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

#### Reid Barton (Oct 25 2019 at 14:37):

preorder.to_has_lt extracts the has_lt instance from a preorder instance

#### Reid Barton (Oct 25 2019 at 14:38):

it's automatically generated by that class preorder declaration

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

#### 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?

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