How to use a type alias without breaking typeclass synthesis

Stream: new members

[Marko Grdinić]

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]

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

[Rob Lewis]

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

[Marko Grdinić]

Thanks!

[Marko Grdinić]

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ć]

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ć]

@[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]

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

[Kevin Buzzard]

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

[Marko Grdinić]

@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]

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]

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

[Rob Lewis]

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ć]

@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ć]

@[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ć]

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]

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]

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

[Marko Grdinić]

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?

[Marko Grdinić]

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ć]

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ć]

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

[Reid Barton]

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]

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ć]

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]

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]

preorder.to_has_lt extracts the has_lt instance from a preorder instance

[Reid Barton]

it's automatically generated by that class preorder declaration

[Marko Grdinić]

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ć]

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]

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.