quantify over universes in build iota

[patrick-nicodemus]

No description provided.

[patrick-nicodemus]

Hm, no. This is still not correct because lines 165 and 166 assume that GR and NGR are globals.

expand-spine (info _ GR NGR _ _ _) X Y AccL AccR Premises Clause :-
  expand X Y, !,
  % we build "app[f,x1..xn|rest]"
  (pi rest1\ coq.mk-app (global GR)  {std.append {std.rev AccL} rest1} (L rest1)),
  (pi rest2\ coq.mk-app (global NGR) {std.append {std.rev AccR} rest2} (R rest2)),
  % we can now build the clause "expand (app[f,L1..Ln|Rest1]) (app[f1,R1..Rn|Rest2])"
  % here we quantify only the tails, the other variables were quantified during
  % expand-*
  Clause = (pi rest1 rest2\ expand (L rest1) (R rest2) :- [!, std.map rest1 expand rest2 | Premises]).

[patrick-nicodemus]

Had the idea of adding

expand-spine (info _ GR NGR _ _ _) X Y AccL AccR Premises Clause :-
  coq.env.global GR (pglobal _ _),
  expand X Y, !,
  (pi rest1 U\ coq.mk-app (pglobal GR U) {std.append {std.rev AccL} rest1} (L rest1 U)),
  (pi rest2 U\ coq.mk-app (pglobal NGR U) {std.append {std.rev AccR} rest2} (R rest2 U)),
  Clause = (pi rest1 rest2 U\ expand (L rest1 U) (R rest2 U) :- [!, std.map rest1 expand rest2 | Premises]).

but this fails on expand_g.

[patrick-nicodemus]

Elpi Print record.expand "elpi_examples/record.expand".
This command no longer really works correctly, do you know what this should be?

Edit: I found it, it was printing in my installed directory, .opam/lib/coq/user-contrib/elpi_examples

[patrick-nicodemus]

So, this attempted fix fails because the clause is added to expand with a specific universe constant for the constructor Build_r which causes a unification failure later on. My hunch is that all the universe variables occurring in the clause should be universally quantified.

expand (app [pglobal (const «f») A9, A0, A2, A5 | A7]) 
 (app [pglobal (const «expanded_f») A10, A1, A3, A4, A6 | A8]) :- !, 
 std.map A7 expand A8, expand A5 A6, 
 expand A2 
  (app
    [pglobal (indc «Build_r») 
      «elpi.examples.example_record_expansion.468», A3, A4]), expand A0 A1.

[patrick-nicodemus]

Okay. The function now works for expanded_g. Great! I'm not sure my solution is robust, just because there's a lot of subtlety with universes, but at least it works on the test case.

I notice that expanded_g is parameterized over two universes.

expanded_f@{u} =
fun (b : bool) (T : Type@{u}) =>
let X := T in...

expanded_g@{u u0} =
fun T : Type@{u} =>
let X := T in
fun (op : T -> X -> bool) (l s : list T) (h : bool) =>
(forall (x : T) (y : X), op x y = false) /\ expanded_f@{u0} true T op l s = h
     : forall T : Type@{u}, (T -> T -> bool) -> list T -> list T ->
bool -> Prop
(* u u0 |= u <= u0 *)

Would it be better to modify the code to restrict the number of universes? I can't think of a situation where you would need the universes to be different.

[patrick-nicodemus]

I think I have a decent idea of why it's happening. The expand clause
maps f b t to expanded_f b T X op, where there's a fresh universe instance associated to expanded_f. Later this gets unified with the universes for T, X, op,
but it's only a <= constraint rather than an = constraint by cumulativity.

I don't know how to fix this appropriately, but it seems important to fix this or there will be a proliferation of universes.

[patrick-nicodemus]

Yes! I'm very happy with this.
This PR is ready for review and stylistic comments.
I haven't paid much attention yet to code duplication issues between global and pglobal, as I was just trying to solve the problem correctly. But if you see some code that can be made more concise / refactored together so that global and pglobal are treated similarly, then I will give this a try.

[gares]

This is part of the reason why I suggested to make a copy of the file in apps/derive/.
I think it is worth writing some tests, eg about the universe-arity of the generated constants. I can imagine Universe X. Check f_expanded@{X}. or similar.

But the current file is a simple proof of concept and the main role of this file is to explain how to build rules, accumulate them, and implement a "global substitution" thingy.

I'm afraid I lack a decent POC using universes, so maybe the delta of this file can serve for that, dunno.

[patrick-nicodemus]

I think it is worth writing some tests, eg about the universe-arity of the generated constants. I can imagine Universe X. Check f_expanded@{X}. or similar.

Is there some kind of expect-test for this? I don't know how to make it an actual test.

[patrick-nicodemus]

This is part of the reason why I suggested to make a copy of the file in apps/derive/.

Yeah I agree. (Or it could be its own app, unbundle? is it better to group it in with derive?)

[gares]

The test above checks that f_expanded has only one universe quantification.
To ensure more I think you have to write something Definition test_f@{ u v | u < v} := f@{u v}. but I think you can only test an "upper bound" to the constraint set, not really that they are as you prescribe.

[patrick-nicodemus]

Okay. I have addressed the changes you suggested but I added another test (the identity id (t :r@{u0 u1}) := t and got a failure for reasons unbeknownst to me. That is a bug that I will address.

[patrick-nicodemus]

@gares

I think I fixed the bug, but it could probably use more tests.

Any further work I do on this will be in a different PR, in apps.

[gares]

Suggested change

	if (coq.env.global (const C) (pglobal _ _ ))
	(@univpoly! => coq.env.add-const Name NewBo _ _ NC)
	(coq.env.add-const Name NewBo _ _ NC),
	if (coq.env.global (const C) (pglobal _ _ )) (FLAGS = @univpoly!) (FLAGS = true),
	FLAGS ==> coq.env.add-const Name NewBo _ _ NC,

[gares]

Suggested change

	expand-spine (info R _ _ Projs K as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r\ Clause r) :- coq.env.global (indt R) LTy, LTy = global _, !,
	coq.env.indt R _ _ _ _ _ [KTY],
	expand-spine (info R _ _ Projs K as Info) (fun _ (global (indt R)) Bo) Result AccL AccR Premises (pi r\ Clause r) :- !,
	coq.env.indt R _ _ _ _ _ [KTY],

[gares]

Suggested change

	expand-spine (info R _ _ Projs K as Info) (fun _ LTy Bo) Result AccL AccR Premises (pi r U\ Clause r U) :-
	coq.env.global (indt R) LTy, LTy = pglobal _ UL , !, % U is a subset of the universes in the main term to be expanded.
	(@uinstance! UL ==> coq.env.indt R _ _ _ _ _ [KTY]), % Be sure that K is instantiated with the same universe instance UL occurring in the binder LTy
	expand-spine (info R _ _ Projs K as Info) (fun _ (pglobal (indt R) UL) Bo) Result AccL AccR Premises (pi r U\ Clause r U) :- !, % UL is a subset of the universes in the main term to be expanded.
	(@uinstance! UL ==> coq.env.indt R _ _ _ _ _ [KTY]), % Be sure that K is instantiated with the same universe instance UL occurring in the binder