universe unification

Stream: general

[Cyril Cohen]

Dear all (and in particular meta-programming experts @Mario Carneiro , @Johannes Hölzl , @Rob Lewis , @Simon Hudon , @Sebastian Ullrich, and whoever I might have forgotten ), I am still writing the so called parametricity tactic, and I am facing the following problem.

Since parametricity translations generate new relations, I end up generating new universes. The best way I found to do so is to create lots of meta universes. When I am facing a definition, I simply unify the inferred type of the translation of the body with the translation of the type, and then I turn all remaining meta-universes into parameter universe, and I am done.

When doing the same for inductive types, what I would like to do is
1. I compute the translated type for the inductive, and replace every remaining meta universes by parameter universes
2. in each constructor type replace the translated const of my new inductive name (which does not belong to the current environment yet) by a local_const representing the translated inductive type.
3. I launch typechecking in order to unify redundant meta-universes
4. I fix the return sort of the inductive type by computing max + 1 of the sort of the type of every constructor.
Unfortunately I am stuck at step 3... I tried many things: type_check, infer_type followed by unify, to_expr (pexpr.of_expr e), first making a lambda out of my ad-hock inductive local_const, every time followed by instatiate_mvars... And so far I am still stuck...

Would you know of a primitive, already-written meta function, technique or methodology that would ease my pain?
Best wishes!

[Cyril Cohen]

I think I just managed, but at the price of exploring the return type of every constructor by hand, picking the list of arguments to the inductive type and performing individual type-checking with the list of abstract parameters, doing all the substitutions by hand... which seems to me redundant with what lean elaborate is capable of...

[Cyril Cohen]

and my manual check is so slow that I timeout on the translation of list...

[Simon Hudon]

Is it possible to have a look at your code? That would make things a bit easier to follow

[Cyril Cohen]

Is it possible to have a look at your code? That would make things a bit easier to follow

It's a moving target right now... I will show you as soon as it is a bit stable (I think tomorrow morning CEST)

[Simon Hudon]

Until then, for me, the way I handle the universes is by creating the universe parameters by hand. I calculate ahead of time how many universes a construction is going to take and I make the parameters. I try to avoid type checking in the middle of program because it's slow but also, type_check seems like a more superficial type check and doesn't catch every problem.

[Simon Hudon]

mk_mapp and mk_app might be good tools to put in your toolbox though. When you have a definition that you're trying to apply to arguments, it will do the type checking and unification for you

[Rob Lewis]

Yeah, it's tough to make a suggestion without seeing the code. My intuition is that unify followed by instantiate_mvars should work. It's normally willing to match universe mvars. If I'm understanding your description right, this is kind of similar to what you're trying to do, right?

run_cmd
do l ← mk_meta_univ,
   m ← mk_meta_univ,
   let c := @expr.const tt `list [l],
   let d := @expr.const tt `list [m],
   trace c.to_raw_fmt, trace d.to_raw_fmt,
   unify c d,
   expr.to_raw_fmt <$> instantiate_mvars c >>= trace,
   expr.to_raw_fmt <$> instantiate_mvars d >>= trace

[Rob Lewis]

type_check seems like a more superficial type check and doesn't catch every problem.

infer_type is superficial, but I thought type_check checks the entire term, no? Which is why it can be expensive sometimes.

[Simon Hudon]

I've had trouble with type check in the past where I would type_check just before adding a declaration, type_check would succeed but the declaration would fail for typing reason (if I remember correctly, some meta vars had not been unified yet)

[Cyril Cohen]

here is a self contained example:

run_cmd do
  u ← mk_meta_univ, v ← mk_meta_univ,
  let t : expr := mk_app (const (`list.nil) [u]) [const `punit [v]],
  /- fill in with some stuff here to trigger universe meta variable unification -/
  t ← instantiate_mvars t,
  trace $ to_raw_fmt t

[Rob Lewis]

This is trickier than I expected. If you can build enough of the pexpr structure of t, you can use that to force the universe levels to unify.

run_cmd do
  u ← mk_meta_univ, v ← mk_meta_univ,
  let t : expr := mk_app (const (`list.nil) [u]) [const `punit [v]],
  to_expr ``(list.nil) >>= unify t,
  t ← instantiate_mvars t,
  trace $ to_raw_fmt t

But this does feel like a gap in the API.

[Simon Hudon]

Have you tried mk_mapp?

[Cyril Cohen]

Have you tried mk_mapp?

I can't because I already have a big term so it would involve rebuilding the whole term (and a lot of time I guess)... moreover mk_app takes a name and list expr instead of an expr and a list expr

[Cyril Cohen]

This is trickier than I expected. If you can build enough of the pexpr structure of t, you can use that to force the universe levels to unify.

run_cmd do
  u ← mk_meta_univ, v ← mk_meta_univ,
  let t : expr := mk_app (const (`list.nil) [u]) [const `punit [v]],
  to_expr ``(list.nil) >>= unify t,
  t ← instantiate_mvars t,
  trace $ to_raw_fmt t

But this does feel like a gap in the API.

My use-case is to do this unification on a big term that I already generated by some other means, so it is not appropriate to rebuild a skeleton and unify with it... I wouldn't know how to build such a skeleton...

[Cyril Cohen]

And I tried converting to a pexpr and back, it does not work...

[Rob Lewis]

Would it make sense to build that big term as a pexpr and elaborate it at the end? Or do you need more control over the universe levels than that allows?

[Rob Lewis]

Actually, you should be able to build the pexpr skeleton automatically. I don't think this is 100% right, but I need to run in a sec.

meta def pexpr_skeleton : expr → tactic pexpr
| (var a) := return $ var a
| (sort a) := do i ← mk_meta_univ, return $ sort i
| (const a a_1) := return $ const a []
| (mvar a a_1 a_2) := mvar a a_1 <$> pexpr_skeleton a_2
| (local_const a a_1 a_2 a_3) := local_const a a_1 a_2 <$> pexpr_skeleton a_3
| (app a a_1) := app <$> (pexpr.mk_explicit <$> pexpr_skeleton a) <*> pexpr_skeleton a_1
| (lam a a_1 a_2 a_3) := lam a a_1 <$> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (pi a a_1 a_2 a_3) := pi a a_1 <$> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (elet a a_1 a_2 a_3) := elet a <$> pexpr_skeleton a_1 <*> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (macro a a_1) := macro a <$> a_1.mmap pexpr_skeleton

run_cmd do
  u ← mk_meta_univ, v ← mk_meta_univ,
  let t : expr := mk_app (const (`list.nil) [u]) [const `punit [v]],
  pe ← pexpr_skeleton t,
  to_expr pe >>= unify t,
  t ← instantiate_mvars t,
  trace $ to_raw_fmt t

[Rob Lewis]

(Yes, there should be a better way to do this.)

[Simon Hudon]

I'm not sure if that will work. Have you tried it? Without using the @ macro, the elaborator will think the type parameters are regular terms, will try to elaborate the type parameter using their types and the whole thing will fail.

[Rob Lewis]

All applications use the mk_explicit macro, which inserts @ everywhere.

[Rob Lewis]

It works on this example anyway.

[Simon Hudon]

All applications use the mk_explicit macro, which inserts @ everywhere.

I don't understand the syntax tree as well as I thought then. How do you get it to not use mk_explicit?

[Rob Lewis]

Sorry, I phrased that badly. All applications created by pexpr_skeleton use it. | (app a a_1) := app <$> (pexpr.mk_explicit <$> pexpr_skeleton a) <*> pexpr_skeleton a_1

[Rob Lewis]

The goal is that this should be a pexpr with the same structure as the input expr, except each universe is a meta universe.

[Simon Hudon]

Ah! I missed that! Thanks!

[Cyril Cohen]

@Rob Lewis thanks for your suggestion! It works in some cases, and for other cases the manual typechecking works better...
While trying to unify I had a new problem, I will post it in a different thread though.

[Cyril Cohen]

cf https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unify.20fails.20in.20the.20presence.20of.20binders

[Rob Lewis]

Here's a slight update that might fix some of the cases where it didn't work. (I noticed this while trying to investigate the other thread.)

meta def pexpr_skeleton : expr → tactic pexpr
| (var a) := return $ var a
| (sort a) := sort <$> mk_meta_univ
| (const a a_1) := return $ const a []
| p@(mvar a a_1 a_2) := mvar a a_1 <$> (infer_type p >>= pexpr_skeleton)
| p@(local_const a a_1 a_2 a_3) := local_const a a_1 a_2 <$> (infer_type p >>= pexpr_skeleton)
| (app a a_1) := app <$> (pexpr.mk_explicit <$> pexpr_skeleton a) <*> pexpr_skeleton a_1
| (lam a a_1 a_2 a_3) := lam a a_1 <$> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (pi a a_1 a_2 a_3) := pi a a_1 <$> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (elet a a_1 a_2 a_3) := elet a <$> pexpr_skeleton a_1 <*> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (macro a a_1) := macro a <$> a_1.mmap pexpr_skeleton

[Cyril Cohen]

Here's a slight update that might fix some of the cases where it didn't work. (I noticed this while trying to investigate the other thread.)

meta def pexpr_skeleton : expr → tactic pexpr
| (var a) := return $ var a
| (sort a) := sort <$> mk_meta_univ
| (const a a_1) := return $ const a []
| p@(mvar a a_1 a_2) := mvar a a_1 <$> (infer_type p >>= pexpr_skeleton)
| p@(local_const a a_1 a_2 a_3) := local_const a a_1 a_2 <$> (infer_type p >>= pexpr_skeleton)
| (app a a_1) := app <$> (pexpr.mk_explicit <$> pexpr_skeleton a) <*> pexpr_skeleton a_1
| (lam a a_1 a_2 a_3) := lam a a_1 <$> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (pi a a_1 a_2 a_3) := pi a a_1 <$> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (elet a a_1 a_2 a_3) := elet a <$> pexpr_skeleton a_1 <*> pexpr_skeleton a_2 <*> pexpr_skeleton a_3
| (macro a a_1) := macro a <$> a_1.mmap pexpr_skeleton

it still does not fix my other usecases...