unification hints

Stream: general

[Johan Commelin]

Can we use unification hints to make sure that we can just write ℤ if we want to view the integers as an object of the category CommRing?

[Simon Hudon]

I don't think so. Unification hints seem more useful for unbundling a bundled structure than bundling an unbundled one

[Johan Commelin]

Too bad... I really liked the notation (-;

[Joseph Corneli]

Is there a canonical example of unification hints being used in Lean that someone can point to?

[Mario Carneiro]

Cyril and Assia had a demonstration at Lean Together, I wonder if that file is available somewhere

[Mario Carneiro]

It's never been used in lean core or mathlib outside one example in init.core

[Joseph Corneli]

I emailed them to ask about the file!

[Cyril Cohen]

Hi! Both the Coq demo and the Lean equivalent are available on https://lean-forward.github.io/lean-together/2019/

[Cyril Cohen]

Assia Mahboubi: unification hints (in Coq) https://lean-forward.github.io/lean-together/2019/slides/coq_cs_demo.v
Cyril Cohen: unification hints (in Lean) https://lean-forward.github.io/lean-together/2019/slides/demo_structures.lean

[Cyril Cohen]

@Johan Commelin

Can we use unification hints to make sure that we can just write ℤ if we want to view the integers as an object of the category CommRing?

We, in mathcomp, usually explicitly wrap them e.g. [CommRing of ℤ] to denote the canonical structure associated to a carrier. In Coq there is no way to automate this further to my knowledge. But maybe in Lean you could use some special kind of coercion. Indeed, since coercions are fused with the typeclass system, you could make a coercion from Type that finds the structure and packages it with the type to give you the structure as a result.

[Joseph Corneli]

thanks!

[Johan Commelin]

@Cyril Cohen I don't follow... you want a coercion from Type to CommRing? But then it has to turn every type into a commutative ring...

[Cyril Cohen]

@Johan Commelin only when the inference succeeds in finding a CommRing typeclass on the argument. I'm not sure it works, I'm just guessing it might, given how coercions are implemented in lean.

[Cyril Cohen]

@Johan Commelin on second thought, I do not think it is possible ... sorry for the false hopes...

[Johan Commelin]

No problem...

[Chris Hughes]

How does the coe from Prop to bool work? That's a partial coercion.

[Kenny Lau]

@Chris Hughes which files did you import?

[Chris Hughes]

I'm afk, but I think it's in core. It only works on decidable props.

[Kenny Lau]

to_bool : Π (p : Prop) [h : decidable p], bool

[Chris Hughes]

But I don't have to write to_bool

[Kenny Lau]

interesting

[Andrew Ashworth]

bool to Prop is a special case handled in the C++ code, iirc

[Andrew Ashworth]

this will change in some way in lean 4, but I don't remember where I read that