To reiterate what I said in the call just now: there are two improvements that I think would make canonical structures with function fields more useful:

- requiring fewer casts in situations where the solution should be unique and obvious. https://github.com/coq/coq/issues/11189 is one example.
- allowing dependent functions. I've started working on this but my understanding of the code is.. minimal at best. Here's the diff so far: https://github.com/Janno/coq/commit/4f6a31c87fcd28a0ad3d2a200b8fd420e39d4415. That commit also has a test case that I think should eventually pass.

(That branch contains a renaming of `Prod_cs`

to `Impl_cs`

so that I can use `Prod_cs`

for dependent functions. It's a bit confusing, I must admit!)

Okay, maybe it wasn't so difficult after all: https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun seems to make the test pass. I wonder if it makes any sense :D

Is the comment of Georges correct? Because this has an impact on point 2.

His observation is that stuff like `noccurn`

is not exactly what you may want. Take this product `forall x : nat, vector nat _`

. The `_`

is an evar that potentially sees `x`

, eg `?e[x := x]`

. If you want the code to make a choice there between Prod_cs and Impl_cs (as you want in 2) then it is not clear what to choose. You could say it is the dependent space (since `x`

occurs, this is what `noccurn`

returns), or prune `?e`

saying that is cannot use `x`

. Both are possible. Also, it may be the case a little change in the input term fixes `?e`

to a concrete term that does not use `x`

. Making the choice quite fragile.

This is why I've asked if 1 would be enough: having a single `AnyFunctionspace_cs`

for both the dependent and non-dependent space seems a way more robust behavior, but maybe it is not enough for your use cases.

I.. actually don't quite know. But I am beginning to understand what Georges wrote (as usual, it takes me a few months)

In my branch above I kept two variants just because I thought it might have a performance impact otherwise but I would prefer just having one. I can't really speak to the consequences, though.

I'm a bit surprised it "just works" as we must be comparing terms in the wrong environment at some point

I would prefer if the decomposition of Prod was `[a; (fun x : a => b)]`

instead.

And then keeping a single `Prod_cs`

should be enough, we don't need to know about the dependency apparently.

The `noccurn`

test would just be an "early" optimization in this case

I don't suppose I can just change `[a; b]`

to `[a; mkLambda (x,a,b)]`

, can I? (It doesn't seem to work.)

My understanding is that today Coq does an `noccurn`

and if it says "it occurs" it does not even try to look up a canonical solution. During the call Janno said that he tried to simply disable the check, but later things broke. I think we could start from that, see why they broke.

~~IIRC when a problem like ~~`c args = proj _`

is solved by CS, then `c`

is left as it is. In our case it would be `a -> b = proj _`

, we may need to unify `a->b`

with the canonical value (unlike we do the `c args`

case, where `c`

is left alone). This unification would prune (if needed) the evars in b

Never mind, I had to change it in two places. It does seem to work.

What happens is that this [a; b] stack is compared to one coming from the left (extraargs1), at line https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun#diff-c693614a22b8a1de52bd824f20139dbfL1128

Well, some part of the stack, depending on o_TCOMPS. I'm wondering what value this o_TCOMPS has for product projections.

Sorry, I have no idea how to reply to the comments on GitHub. I see them but there is no way to do anything with them. That is one hell of a confusing interface.

@Matthieu Sozeau I re-added the line that I removed in the next commit (which, rather unhelpfully, has the same commit message).

@Enrico Tassi I have no idea how the unification algorithm works so I don't know where `a`

and `b`

end up..

Oh, sorry, got the authors mixed up. (fixed)

Ok, I see now: we should also use `[a; tLambda (na, a, b)]`

in `pattern_of_constr`

in case the variable occurs in `b`

. This is what gets compared to sk2/effective_sk2 during unification

We could keep the special case for non-dependent products to avoid unifying things twice. Or actually always return just `[tLambda (na, a, b)]`

uniformly

I think that now I understand the code and why it needs the product to be non dependent. It sees `a -> b`

as (pardon my OCaml), `(->) a b`

.

But this makes sense only if `b`

does not see `a`

, hence the "delift" performed on b.

I guess Matthieu was already on the right track, I just could not understand it ;-) I agree with what he proposes.

I haven't removed the non-dependent case yet but here's the what I did with the `mkLambda`

: https://github.com/coq/coq/commit/40f10e41df7af734bb2798a2a989f29d3c25b92d

Cool, we all agree :)

I suppose two of us know what they are talking about and one (that would be me) will agree with whatever you two decide :)

I'd be curious to try the variant where it is uniform and we just translate `tProd (na, a, b) -> Prod_cs, None, [tProd (na, a, b)]`

actually, and do away with the special case for `->`

. If it benchmarks well, it would be simpler. Otherwise said I don't think it needs to deconstruct the arrow as `(->) a b`

at all.

As in https://github.com/coq/coq/commit/57e8dc718cbd54ee584994f0b2be2005cd296102?

Almost, no need to have `[a`

at the head of the lists as the lambda domains will be compared anyway

And I think we can just put the products instead of rebuilding lambdas

This avoids also a decomposition.

Ah, now I get it. I just assumed you meant Lambda, not Prod!

This is the current diff: https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun. It does seem to do the right thing, too.

Now, how would I go about tackling https://github.com/coq/coq/issues/11189?

Trying to implement this myself but I am stuck trying to determine if a term is in fact an unfolded (non-primitive) projection. Is there a function for this?

How do I even get the fields of a non-primitive record? Also, how do I find out if an inductive is a record?

I feel like there is a module that I am missing that contains all the record-related functions that I can't find

No, there is no such a functionality (recognize unfolded canonical projs). Actually evarconv tries hard not to unfold canonical projections, exactly for that reason.

`Recordops.lookup_projections`

lets you get the projections of a record

Ah, just what I was looking for! Thanks!

The reason I am dealing with unfolded projections is that I am extending this match here: https://github.com/coq/coq/blob/master/pretyping/pretyping.ml#L849

It seemed like a reasonable place to add this new feature

As far as I can tell, `check_evar_record`

(my only example for code relying on `lookup_canonical_conversion`

) never introduces new evars for the arguments of the canonical structure. How does that work? My naive intuition says that to continue with unification, the arguments need to be filled by evars (or by the appropriate parameters of the record, if that's generally possible).

Janno said:

This is the current diff: https://github.com/coq/coq/compare/master...Janno:janno/cs_dep_fun. It does seem to do the right thing, too.

As far as I understand, the current approach/diff does not distinguish dependent product from implications. I think this is good, since a a dependent product can become an implication by reduction, and having two distinct case in canonical instance resolution might introduce some impredictability....

Now, while we are at it, could we add a `Lambda`

key in canonical inference to have lambda abstraction behave as a key?

I think I thought about adding `Lambda`

many times but I never come up with a good use case. Do you have one?

Oh I have a few...

e.g. functions that are canonically positive.

I can try to implement that, I guess. I'm stuck with the other feature anyway and I am not as intimidated by the `Lambda`

thing. (Not yet, anyway.)

It would be great if you could give me a small test case so that I know I am working toward something that makes sense!

Janno said:

It would be great if you could give me a small test case so that I know I am working toward something that makes sense!

I'll try maybe on Monday...

This is what I have now:

```
Structure cs_lambda := { cs_lambda_key : nat -> nat }.
Canonical Structure cs_lambda_func := {| cs_lambda_key := fun x => x+1 |}.
Example cs_lambda_ex0 := eq_refl : (cs_lambda_key _) = (fun x => x + 1).
```

Or, somewhat less specific:

```
Example cs_lambda_ex0 := eq_refl : (cs_lambda_key _) = (fun _ => _).
Print cs_lambda_ex0. (* eq_refl : cs_lambda_key cs_lambda_func = (fun H : nat => H + 1) *)
```

(Working on the documentation of CS.) This following sentence from the canonical structure docs really confuses me

Otherwise said, qualid is canonically used to extend the field cᵢ into a complete structure built on cᵢ.

Is this a typo? The equation above it really makes me think this is supposed to read "extend the field xᵢ" instead of cᵢ. But I don't really know the terminology here.

Well, as xi and ci are convertible, one could use both, no?

Well, yes, because the documentation pretends that the canonical extension will only happen when we are looking for a term `xᵢ _`

that matches `cᵢ`

literally. But that's not always the case, is it?

Okay, sure, it will only *succeed* if they are unifiable. But an instance might also be considered if the terms don't match perfectly (with `_ -> _`

projections, for example)

In that case we might be looking at `xᵢ _ ~ nat -> nat`

but our instance has `cᵢ := bool -> bool`

. How does that fit into the picture?

I guess the paragraph is technically correct but just very confusing for me. Maybe I simultaneously know too much about the implementation and too little about how people think about canonical structures.

Maybe we should add, ", when ci unifies with xi _" to be clearer

Where exactly do you want to add this? I don't see a good place but I might be missing something.

I would suggest rephrasing "to extend the field xi into a complete structure build on ci, when ci unifies with xi _" ?

Matthieu Sozeau said:

I would suggest rephrasing "to extend the field xi into a complete structure build on ci, when ci unifies with xi _" ?

Done. (Not yet pushed because I want to have other comments resolved before I push my rebased commits.)

Could somebody start a benchmark for https://github.com/coq/coq/pull/12349? Removing the restriction to non-dependent functions could potentially have a negative performance impact, I think.

Or can I start benchmarks myself? Where can I find documentation about that?

go https://ci.inria.fr/coq/ and get an account

(someone will have to approve your request)

then pendulum > benchmark-par-of-the-branch > build-with-parameters

fill in the form and click build

Is there a signup option? I guessed a probable url and got this:

Sign up

This is not supported in the current configuration.

I can't find a register/sign up link or button

try from https://ci.inria.fr/

(not sure, but there is a sign-up button there)

then you should probably join the Coq project, which will require validation

Done!

you should be in now

Cool, thanks!

try to follow my instructions. Btw, you can select a smaller set of packages for the bench, eg start with the ones you are most likely to hit (math-comp, iris & co) since if you run all packages it will take a lot of time, but you can do as you prefer

I don't see "build-with-parameters" anywhere when clicking on "benchmark-part-of-the-branch"

I think I have neither "admin" nor "slave admin" permissions. Could that be a problem? (All other members have at least one of these, as far as I can tell.)

did you log in again (in ci.inria.fr/coq) ? (top right corner)

I logged out and logged back in again but nothing changes.

I made you admin (we all are), please try again

Yup, that fixed it!

well, happy benchmarking

Thanks :)

Oh, and 1% difference in time is typically noise

Hehe, I mostly ignore time measurements and cycles. I've done too much benchmarking to put any faith in N=1 time or cycle benchmarks.

anyway, it is running fine... lets see

The benchmark results seem reasonably indistinguishable from noise. I don't have enough coffee grounds to properly interpret the results but my gut says there's a tiny tiny slowdown in coq-lambdarust. Probably not too bad, though. I'll post the results in the PR.

I made some progress on my next goal for improving canonical structures: https://github.com/coq/coq/pull/12383

I could use feedback on whether this is a good idea, how to best do this (my attempt is rather naive) and anything else really!

@Gaëtan Gilbert regarding https://github.com/coq/coq/pull/12383 and moving the app case into `inh_app_fun`

: I see that `inh_app_fun`

and `inh_app_fun_core`

interact with coercions, program mode, and type classes. Should CS search be triggered before all these things? (The current state of the patch triggers it after.) I don't understand exactly how, for example, program mode interaction works here. Will the choice of what to do first impact what kind of obligations arise?

Your PR seems about equivalent to unifying with `forall x:_, _`

(but maybe a bit more efficient) so I would put it first

I finished moving the code for the app case to coercions.ml and that seems to work fine. I am also moving the `fun`

code into `split_tycon`

but now I wonder where I should move `split_tycon`

to? I can't call `Evarconv.unify`

from Evardefine because that yields a module dependency cycle.

I'd make split_tycon internal to pretyping

Okay, I'll do that!

nice response time ;)

Next question: I am currently checking for a `Prod_cs`

instance to avoid unnecessary unification but I completely forgot about `Default_cs`

. I suppose either would be reason enough to try unification?

I don't know how the _cs stuff works, maybe someone else does.

It may work to unify without looking up coercions (keeping the optimised version for when it"s already a product and when it's an evar)? failing paths may be slower but not necessarily by a lot

Hm, I don't understand what you are proposing. How do coercions figure into it? Is there an option for unification that I can/should set?

sorry I get confused between canonical structures and coercions (_cs sounds like coercion to me somehow)

Ah, I see!

Last updated: Feb 01 2023 at 17:04 UTC