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

[Yaël Dillies]

I have been trying to write a unification hint to get ((s : Finset α) : Set _) to work. Can anyone see what I did wrong?

import Mathlib.Data.Finset.Basic

open Lean Meta

-- @[unify] def finsetToSet {α β : Type*} (s : Finset α) (t : Set β) : UnificationHint where
--   pattern := ⟨`(s), t⟩
--   constraints := [⟨α, β⟩]

unif_hint forget_obj_eq_coe {α β : Type*} (s : Finset α) (t : Set β) where
  [α ≟ β] ⊢ s ≟ t
-- unexpected token '≟'; expected ':' or ']'

example {α : Type*} (s : Finset α) : Set.univ ⊆ s := sorry
/-
application type mismatch
  Set.univ ⊆ s
argument
  s
has type
  Finset α : Type u_1
but is expected to have type
  Set ?m.342 : Type u_1
-/

[François G. Dorais]

I think α and β need t be at the same universe level. But I don't understand what you're trying to do here.

[François G. Dorais]

Maybe you mean something like this:

unif_hint guess {α : Type*} (s : Finset α) (t : Set α) (x : α) where
  (s : Set α) =?= t ⊢ (x ∈ s) =?= (x ∈ t)

[Yaël Dillies]

I am trying to get the example in my MWE working without error

[Yaël Dillies]

I don't really understand what membership has to do with it

[Yaël Dillies]

It is a huge impediment to the finset library that we can't use s : Set alpha in a function expecting a Set ?beta unless Lean knows that ?beta := alpha. I am trying to make Lean automatically set ?beta := alpha in such a situation.

[Kyle Miller]

I'm not too familiar with unification hints, but it seems like the won't work here. The issue is that you're needing a coercion to apply, and it's the coercion that's failing to be synthesized because typeclass synthesis refuses to assign the metavariable in Set _. This assignment can't happen even with hints.

[Kevin Buzzard]

But Yael is right, I've run into this and I hardly ever use finsets, so presumably many people have. Is there anything we can do about it?

[Kyle Miller]

Coercion has special support for some similar situations, like if Finset and Set were both monads and there were a MonadLift Finset Set instance then it could do something.

It would be nice if there were a system supporting "functorial" coercions, like a coercion from the Finset to Set (not a coercion from Finset X to Set X — a coercion of the type functions themselves)

[Kyle Miller]

Somewhat related, we have support for this situation in mathlib in the form of the fbinop% elaborator for docs#SProd.sprod, to be able to elaborate products of sets/finsets/filters.

[François G. Dorais]

Yaël Dillies said:

I am trying to get the example in my MWE working without error

For a unification hint to be valid the conclusion has to unify given the unification hypotheses. Your (slightly edited) proposal

unif_hint forget_obj_eq_coe {α β : Type u} (s : Finset α) (t : Set β) where
  α ≟ β ⊢ s ≟ t

doesn't work since it says that any such s and t must unify so long as α and β unify. That doesn't make sense (except perhaps when α and β are both empty). I don't understand what you're aiming for.

[François G. Dorais]

(Also, the proposed example doesn't appear to be true.)

[François G. Dorais]

Yaël Dillies said:

It is a huge impediment to the finset library that we can't use s : Set alpha in a function expecting a Set ?beta unless Lean knows that ?beta := alpha. I am trying to make Lean automatically set ?beta := alpha in such a situation.

So you want this?

unif_hint another_guess (α β : Type u) where
  α ≟ β ⊢ Set α ≟ Set β

I don't think that's useful but it works!

[Kyle Miller]

Yael misspoke, that doesn't need a unification hint since it already follows from the usual defeq rules. It's for ((s : Finset X) : Set _), getting the coercion to work and propagating the X.

[François G. Dorais]

With an example that makes sense, I might be able to figure out the right unification hint (assuming that's what is actually needed).

[François G. Dorais]

Did anyone try a HasHSubset class? (Not clear where the extra H should go.)

[Yaël Dillies]

Actually that might be a job for a default instance?

[Yaël Dillies]

I don't just want this to work for subset notation but any function that expects a set

[Bhavik Mehta]

import Mathlib.Data.Finset.Basic

theorem annoying {s : Finset ℕ} (hs : s = ∅) : Set.Subsingleton s := sorry

Here's a massively simplified example of what gets frustrating in practice. Lean gives the error

application type mismatch
  Set.Subsingleton s
argument
  s
has type
  Finset ℕ : Type
but is expected to have type
  Set ?m.102 : Type

but - in my mind - it's clear that Set ℕ is the only sensible choice here. The current workarounds which appear are:
Set.Subsingleton s.toSet or Set.Subsingleton (s : Set ℕ), both of which seem unnecessarily wordy (especially if I have a finset in a type which is less nice to write down). It'd be really nice if I could just write Set.Subsingleton s, and Lean could automatically figure out that a finite set of naturals can be seen as a set of naturals.

[Kyle Miller]

I was mentioning earlier that if Set and Finset were both monads and you had a MonadLift instance, then there's already coercion infrastructure for this, but we intentionally disabled the Set monad instance earlier this year because it could be surprising, and it would insert some monad functions that there wasn't any theory about.

MonadLift example

import Mathlib

open Classical

attribute [local instance] Set.monad Finset.instMonad

instance : MonadLift Finset Set where
  monadLift s := s

theorem annoying {s : Finset ℕ} (hs : s = ∅) : Set.Subsingleton s := sorry
/-
annoying {s : Finset ℕ} (hs : s = ∅) : (liftM s).Subsingleton
-/

[Yaël Dillies]

And what if we made that monad function the default coercion from a finset to a set. How would that be?

[François G. Dorais]

In Bhavik's example, unification works fine and unification hints don't work. TC inference fails because the goal is CoeT (Finset Nat) s (Set ?m) but TC inference can't assign the mvar.

Kyle's example works because the TC goal is MonadLiftT Finset Set, which has no unassignable mvars. This is probably the right way to go.

[Bhavik Mehta]

Is it at all possible to make TC inference able to assign the mvar in that example?

[François G. Dorais]

To make TC inference to assign mvars they need to be semiOutParam or outParam. I'm thinking that with CoeT this is not going to play well with the complex maze of Coe* classes. This is what CoeHead is for but that won't help here, I think. The other mechanism is default instances but I'm skeptical that can be made to work.

[Daniel Weber]

Could CoeOut be useful here?

[Kyle Miller]

François G. Dorais said:

I'm thinking that with CoeT this is not going to play well with the complex maze of Coe* classes.

Also neither argument to Coe is an output. We'd soon run into examples where we want fun s : Finset _ => (s : Set Nat) to work too.

François G. Dorais said:

Kyle's example works because the TC goal is MonadLiftT Finset Set, which has no unassignable mvars.

Yes and no. That's why the MonadLiftT instance succeeds, but the key fact is that there is special elaborator support for computing coercions using monad lifts.

I would rather that we don't explore using Monad here, but instead come up with a solid proposal for functorial coercions in core. This problem crops up frequently.

[Kyle Miller]

There are two axes here:

1. Given F X and a "functor coercion" from F to G, getting a coercion F X -> G X.
2. Given F X and a coercion X to Y, getting a coercion F X -> F Y.

The monad coercion system lets you navigate both of these:

-- The monad
example [MonadLiftT m n] (x : m α) : n α := x
-- The type
example [(a : α) → CoeT α a β] [Monad m] (x : m α) : m β := x
-- Both
example [Monad m] [Monad n] [MonadLiftT m n] [(a : α) → CoeT α a β] (x : m α) : n β := x

Questions:

1. Should the system derive an automatic coercion from Finset Nat to Finset Int?
2. Should the system derive an automatic coercion from Finset Nat to Set Int?

A "yes" answer to 1 implies a "yes" to 2 by transitivity of coercions.

My own opinion is "no" to these. While it makes sense for monads (monads are values-with-context, the context should be relatively transparent), with containers this is more fraught. (1) For programming, the inserted coercion might insert a completely accidental copying of the entire data structure. (2) For math, I would expect that getting elaboration to succeed would become a lot more slippery due to all these postponed coercion problems. We disabled the Set monad instance in mathlib partly because it wasn't always anticipated. (We also disabled it because it introduced weird monad functions, but that's fixable in principle.)

[Yaël Dillies]

My answers:

1. Eh, maybe
2. No, because you could either go through Finset Int or Set Nat, and the defeq is different depending on which way you go

[Kyle Miller]

Good point re 2, that's a lot better of a reason than my justification. (And a 'no' to 2 means a 'no' to 1, since otherwise coercions aren't transitive.)

[Yaël Dillies]

Coercions don't have to be transitive, right? That's why we have so many CoeSomething typeclasses, no?

[Kyle Miller]

Yeah I suppose you're right.

If this were wired into CoeHead for example, then that would solve 2, though you could still trigger a sequence of coercions to get a coercion diamond.

Incidentally, why is Finset.instCoeTCSet a CoeTC? That's a nonstandard, since it's meant to be the transitive closure of Coe.

[Notification Bot]

6 messages were moved from this topic to #general > Why is the Finset->Set coercion instance CoeTC? (Was: uni... by Kyle Miller.