help with instances

Stream: new members

[Paul Rowe]

Can somebody please help me understand what is going on here? I have a means of generating a preorder from a variable (2 variables in my mwe below). I would like to fix those variables for the scope of a section and introduce a preorder instance for the current scope.

inductive place : Type
| mk : ℕ → place

inductive copland : Type
| mk : ℕ → copland

variable po : place → preorder copland
variable (p : place)

#check po p -- po p : preorder copland

local attribute instance xmpl (p : place) : preorder copland := po p
#check xmpl -- xmpl : (place → preorder copland) → place → preorder copland

variables c1 c2 : copland

#check c1 ≤ c2
/-failed to synthesize type class instance for
po : place → preorder copland,
p : place,
c1 c2 : copland
⊢ has_le copland-/

So, basically, Lean knows po p : preorder copland, and I'm looking for a way of introducing that as an instance. But the only way I know of creating instances gives me a dependent type that creates instances from variables instead of the desired instance.

[Notification Bot]

Paul Rowe has marked this topic as unresolved.

[Paul Rowe]

It's not as smooth sailing as I had hoped! I actually rely heavily on the inductive structure of the underlying type for which I'm defining a type synonym. It seems the type synonym doesn't give me access to the constructors. Or rather, if I use them, Lean seems to coerce it back to the original type.

I'm too tired to generate a mwe. I'll come back sometime tomorrow. But if there's any obvious advice in the meantime, I'll take it. :smile:

[Mario Carneiro]

One way to fix that is to make copies of the constructors but with a type that uses the type synonym instead of the original

[Matt Diamond]

I assume the reducible attribute wouldn't help here, right?

[Eric Wieser]

Instead of a type synonym, can the indices be added to the inductive type itself!

[Paul Rowe]

@Matt Diamond I've never encountered the reducible attribute, but it seems to do the trick! The symptom was not being able to compare two terms of the new type synonym using ≤ if the constructors were explicit. Using reducible seems to make it work. I will look up what it does, but is there a nice explanation of what it does?

[Paul Rowe]

@Mario Carneiro Does your suggestion essentially amount to creating a duplicate type without it being a true type synonym? If not, I'm not sure what you mean.

@Eric Wieser Are you suggesting I force the original type to carry the extra parameter p? I'm not sure I like that since other results about that type truly don't need it. Sorry if I'm misunderstanding.

[Mario Carneiro]

like this:

inductive place : Type
| mk : ℕ → place

inductive copland : Type
| mk : ℕ → copland

def coplandA (p : place) := copland

def coplandA.mk {p} : ℕ → coplandA p := copland.mk

variable p : place

instance xmpl : preorder (coplandA p) := sorry

variable c2 : coplandA p

#check coplandA.mk 5 ≤ c2

[Mario Carneiro]

it's up to you whether p needs to be explicit or not in coplandA.mk

[Paul Rowe]

I see. What will happen if I try to apply cases to a term of type coplandA p? The type actually has numerous constructors.

[Matt Diamond]

@Paul Rowe I'm actually not completely sure what reducible does myself... also, I seem to have a habit of giving advice that technically works but isn't the right solution :sweat_smile: so I hope someone else can come along and verify that reducible is appropriate here

I'm curious to know if it's documented anywhere

[Paul Rowe]

One small wrinkle that I have run across with using reducible is that it breaks the separation of the type synonyms. What I mean is that if I have two type synonyms for the same type and they are both reducible, then they are in conflict. I can fix this by making the reducible attribute local, which eliminates one of the benefits of the approach. That said, I think I'll keep moving forward with this as it has provided me the least resistance so far.

[Paul Rowe]

Also found a nice reference sheet here.

From that reference:

reducible       : unfold at any time during elaboration if necessary
quasireducible  : unfold during higher order unification, but not during type class resolution
semireducible   : unfold when performance is not critical
irreducible     : avoid unfolding during elaboration

[Matt Diamond]

@Paul Rowe nice! is it possible that something like quasireducible might provide the benefits without the drawbacks?

[Matt Diamond]

I also wonder if using tactic#unfold manually would work

[Paul Rowe]

I thought about quasireducible too, but since I got unstuck, I'm having too much fun proving new things. :smile: You must be right about unfold since that's clearly what reducible is doing for me behind the scenes.

[Eric Wieser]

I don't think docs#quasireducible (note: no suggestions provided by the docs) exists in Lean 3; I've never seen it in the wild

[Paul Rowe]

Ah yes! I blew right by the comment at the top of the reference:

Note that this quick reference guide describes Lean 2 only.

[Alex J. Best]

Was it changed to instance reducible? That exists in lean 3 and isn't on that reference list.

[Matt Diamond]

Alex J. Best said:

Was it changed to instance reducible? That exists in lean 3 and isn't on that reference list.

How does that work? Is there documentation on it?

[Alex J. Best]

I was thinking of docs#tactic.transparency, but it looks like that is somehow the opposite