Here are a two examples that seem to require some kind of conditional coercions:

```
Check z ⨯ z^* > 0. (* where z is in C, ^* is conjugation, > 0 is in R *)
Check (n * (n + 1)) / 2 = 0 (* where n and 0 are in N, but / in Q or R *)
```

Are there already standard techniques to deal with them? Would otherwise a notion of "conditional coercion" make sense, where, here, we could e.g. have things like:

```
Coercion RealPart (x : C) : R when ImPart x = 0.
Coercion IntPart (x : Q) : Z when FracPart x = 0.
Coercion PosPart (x : Z) : nat when x > 0.
```

[Incidentally, what would be the best stream to talk about library design and formalisation techniques in general?]

We do have a *very experimental* feature for this in HB, namely https://github.com/math-comp/hierarchy-builder/pull/420

CC @Quentin VERMANDE

In our case the side condition must be a Class (as in HB slang) and be solvable by the TC inference engine, that in this case amounts to roughly "assumption".

In a way, the predicate must be a well known one, one for which a class exists. It seems to fit your use case, since your predicates are what defines the sub type of reals (out of complex) and integers (out of rationals). But I let Quentin or @Cyril Cohen to better explain the use case they have.

Could you give a working example in HB?

As an experiment, in the following obligation-tactic-based code, we would like `int_part`

to be declarable as a coercion:

```
Fixpoint sum n := match n with 0 => 0 | S n => sum n + n end.
Require Import QArith.
Coercion N_to_Q x := inject_Z (Z.of_nat x) : Q.
Axiom frac_part : Q -> Q.
Axiom int_part : forall q:Q, frac_part q = 0 -> nat.
Arguments int_part q {_}.
Axiom cond : forall x, frac_part ((x * (x+1)) / 2 ) = 0.
#[global] Obligation Tactic := apply cond.
Program Theorem Gauss n : sum n = int_part ((n * (n + 1)) / 2).
```

Note: There is also the issue that `=`

decides too early the type of the equality so that, conversely, `Program Theorem Gauss n : int_part ((n * (n + 1)) / 2) = sum n.`

fails if we don't explicitly give type `nat`

to `n`

.

Our running example is the following one :

```
Structure set (T : Type) := MkSet {
set_to_pred : T -> Prop
}.
Notation "[ 'set' x : T | P ]" := (@MkSet _ (fun x : T => P)) : set_scope.
Notation "[ 'set' x | P ]" := (@MkSet _ (fun x => P)) : set_scope.
Notation "[ 'set!' P ]" := (@MkSet _ P)
(P at level 200, format "[ 'set!' P ]") : set_scope.
HB.mixin Record mem T (X : set T) (x : T) : Prop :=
Mem { IsMem : set_to_pred X x }.
#[short(type="memType")]
HB.structure Definition MemType T (X : set T) := {x of mem T X x}.
Notation "x \in X" := (@MemType _ X x).
Notation memP := MemType.class.
Coercion memType : set >-> Sortclass.
Check fun (T : Type) (X : set T) (x : X) => x : T.
Check fun (T : Type) (X : set T) (x : T) (xX : x \in X) => x : X.
```

This depends on PR https://github.com/math-comp/hierarchy-builder/pull/420. There are two coercions that have been declared in Elpi and would not work in Coq. The first one coerces on object of type `@set T X`

to `T`

. This would not work in Coq since `T`

is not a global reference. The second one takes an element `x`

of `T`

and calls the elaborator on `@MemType.Pack T X x _`

. If the elaboration succeeds, the elaborated term has type `X`

and is returned.

In your case, the only way I see how to do it is through elpi, since the coercions you write are metaprograms. Although this means that you lose the composition of coercions. Something like that would work:

```
From elpi.apps Require Import coercion.
Axiom A B : Type.
Axiom P : A -> Prop.
Axiom f : forall a, P a -> B.
Elpi Accumulate coercion lp:{{
coercion _ V {{ A }} {{ B }} R :-
R = {{ @f lp:V _ }},
coq.ltac.collect-goals R Gs [],
std.forall Gs (g\ coq.ltac.open (coq.ltac.call-ltac1 "trivial") g []),
coq.ltac.collect-goals R [] [].
}}.
Elpi Typecheck coercion.
Check fun (a : A) (aP: P a) => a : B.
```

Thanks a lot! If I understand correctly, this is elaborated to:

```
Structure set (T : Type) := MkSet { set_to_pred : T -> Prop }.
Arguments set_to_pred {T} _ x.
Record mem {T} (X : set T) (x : T) : Prop := Mem { IsMem : set_to_pred X x }.
Record memType {T} (X : set T) := Pack { sort : T ; class : mem X sort }.
Arguments sort {T X} _.
Arguments Pack {T X}.
Check fun (T : Type) (X : set T) (x : memType X) => x.(sort) : T.
Check fun (T : Type) (X : set T) (x : T) (xX : mem X x) => (Pack x xX) : memType X.
```

where the two special treatments are applied.

I have virtually plenty of questions, if I may. For instance:

Is the `mem`

indirection important?

Can it be chained? E.g. taking the `set`

of a `set`

?

Do you have plans to provide a composition of coercions?

That is basically it. `mem`

is a class, not a record, so that the elaborator finds the instance in the context on the last line. This is the only reason why the `mem`

indirection is important for the inference. If you write your own coercions in elpi, you can choose a different method (as in the second example above) which does not go through the typeclass solver.

It can be chained. In fact, taking the set of a set works already in this PR. What happens is that when the type of the input is a structure (and the coercions are declared in elpi), I insert the projection and elaborate the projected term to the expected type, which relaunches a coercion search if needed.

In general, declaring a coercion in elpi amounts to writing a metaprogram that searches for the correct term to return (which may even be something else than a function applied to the input term). The way you define your search determines how coercions compose. For instance, you can ask for a term to be elaborated (as I do), which may trigger another coercion problem, or you can ask elpi directly if it is able to find a coercion.

In passing, what are the long-term plans around coercions in Elpi compared to what Coq already provide? Is the idea that Elpi is used for experiments before re-implementing on top of the current Coq coercion infrastructure? Or is the idea that Elpi is eventually integrated to Coq and that the current code for coercions is redone in Elpi?

I'm asking because, on one side, adding conditions to coercions would be relatively easy to do already on top of the current system (and probably the same for another feature request which is pattern-based coercions). On the other side, people currently interested in extending coercions seem to work with Elpi (even if I know someone working at the level of Coq). So, I'm curious about what vision to carry?

Thanks in advance for feedback.

It's indeed much easier to carry experiments in elpi. I don't see much point in reimplementing then into OCaml, except if it becomes needed for performance reasons, but we are not there yet.

Yes, that's my question. It is not clear to me at the moment how the OCaml implementation would interact with the Elpi implementation, and it is not clear to me that implementing in OCaml would be more complicated that implementing in Elpi (at least as far as conditional coercions are concerned, even if taste and colors vary regarding programming languages appetence, and that's healthy and normal).

So, shortly, I'm trying to collect facts and opinions about what would be best to do. In particular, I know someone interested to work on coercions at the OCaml level, and I'm trying to understand what to tell this person.

Yes, writing that kind of code in OCaml is definitely more work (because the interface is much lower level). In elpi you could directly write gallina terms whereas in OCaml you would have to deal with constr.mli, that's much lower level.

Sure, but in both cases you have to learn a language (e.g. learning how to write the `Elpi Accumulate coercion`

code above also requires some expertise).

For instance, could have reverse coercions been written in Elpi? And if yes, how would the implementation differ from what has been done in OCaml?

On this subject, I have been told by many people that learning Elpi is not that hard and that compare to ocaml or metacoq, it enables to do real stuffs and experiment much faster

Note that the person already knows a bit of OCaml and of the code of Coq, so the cost of learning Coq code does not really matter here. My question is more about the long-term vision regarding coercions. For instance, should we think at redoing the current OCaml implementation for coercions in a "higher-level" "meta" language? E.g., could the current implementation of coercions already be fully delegated to Elpi?

It's not so much a matter of learning, it's rather like programming in assembly code vs a high level compiled language. Except for very specific things, the latter is always going to be much faster.

At the moment, it is true that Elpi seems much better for basic meta-programming.

But at the same time, MetaCoq has little if not no API for meta-programming so it is normal that it is a bit tedious. It will be much better on the longer run once good api, in particular for dealing with debruijn indices will have been developer. If could generate derivation nicely in MetaCoq that would be great.

If the claim is that "high-level" programming languages supporting fast, easy and fully-fledged development of Coq features are useful (and needed), I agree.

Regarding coercions, has someone already considered moving the whole current existing OCaml infrastructure to one of the high-level programming (meta)language? How much work would it be?

Right now calling Elpi to solve coercion is much more expensive that doing it in Coq. I plan to make it less expensive in the fall, but it will never be as fast as OCaml so it really depends what one wants. I mean, if we replace the Coq mechanism by an Elpi one *always* then we surely get a visible slowdown, also for projects that don't need any fancy coercion system. In particular there are many places where coercions may be triggered without the user even noticing, eg: https://github.com/coq/coq/pull/19372

Last updated: Oct 13 2024 at 01:02 UTC