Generalized coercions

[Tragicus]

This PR adds better support for coercions:

• declares the constructor of the class as an elpi coercion, using elaborate-skeleton to fill in the holes,
• declares the sort projection as an elpi coercion when there is no coercion target,
• declares axioms_ as a typeclass (enables inference in the first coercion)

[gares]

I have one question: do we really need the coercions to use unification to see if we are from/to a structure? I don't see the point of aliasing a structure.

If the clauses were of the form

pi bla bla bla\ coercion ctx v (app[Structure|RevArgs]) e r :-

they could be indexed much better (we have some deep indexing features in the pipes). This rule would trigger only if the type is syntactically the structure type constructor applied to the list of arguments. The body can still use unification if needed.

[gares]

@CohenCyril LGTM. Can you double check and merge?

[CohenCyril]

That's great @Tragicus thanks for pushing.

I have a general question: how does it compose with coq coercions?
e.g. reusing your test-suite file (coercion.v), this is what happens if I have

Axioms (A B B' C : Type) (AtoB : A -> B) (BtoB' : B -> B').
Axioms (P : A -> Prop) (CtoAP : C -> sigType A P). 
Coercion AtoB : A >-> B.
Coercion BtoB' : B >-> B'.
(* does postcompose automatically with Coq coercions*) 
Check fun (x : sigType A P) => x : B.
Check fun (x : sigType A P) => x : B'.

(* testing a Coq coercion to sigType *)
Coercion CtoAP : C >-> sigType.
Check fun (x : C) => x : sigType A P.

(* does not precompose automatically with Coq coercions *)
Fail Check fun (x : C) => x : A.
Check fun (x : C) => (x : sigType A P) : A.
Check fun (x : C) => (x : sigType A P) : B.

[CohenCyril]

This looks really nice! But...

• it is a bit more than generalized coercions, for which I would expect this coercion to work only when (x : T) has been endowed with a HB.instance of isSigma. e.g.

Axioms (A : Type) (P : A -> Type) (x : A) (Px : Sig A P x).

(* should not work indeed *)
Fail Check (x : sigType A P).

(* this works though ...*)
Succeed Check (let Px' := Px in x : sigType A P).

(* This should works but does not *)
HB.instance Definition _ := Px.
Fail Check x : sigType A P.

In comparison, the analogous code, but on Type works:

HB.mixin Record isSigmaT (P : Type -> Prop) (x : Type) := { _ : P x }.
#[short(type="sigTType"), verbose]
HB.structure Definition SigT (P : Type -> Prop) := {x of isSigmaT P x}.

Axioms (X : Type) (PT : Type -> Prop) (PX : SigT PT X).

(* should not work indeed *)
Fail Check (X : sigTType A PT).

(* this works though now ... cf my next point*)
Succeed Check (let PX' := PX in X : sigTType PT).

(* This is what should work and does *)
HB.instance Definition _ := PX.
Succeed Check X : sigTType PT.

• I cannot find what exactly in the code makes this work, I was wondering what makes it work even when the coercion is not handled by elpi and but by Coq. In comparison, on master the following fails:

From Coq Require Import ssreflect.
From HB Require Import structures.

HB.mixin Record isSigmaT (P : Type -> Prop) (x : Type) := { _ : P x }.

#[short(type="sigTType"), verbose]
HB.structure Definition SigT (P : Type -> Prop) := {x of isSigmaT P x}.

Fail Check fun (P : Type -> Prop) (x : Type) (Px : SigT P x) => x : sigTType P.
Fail Check (let PX' := PX in X : sigTType PT).

[gares]

I think the code just above does not work because the whole business does not kick in since the coercion sort is handled by Coq (the tgt is a supported one in this case), so nobody triggers the TC search.

[Tragicus]

I am extremely confused as to why it works in Type but not in Prop. In both cases, HB.instance declares canonical structures and not typeclasses, so it should not work.

[Tragicus]

Your tests with a let work and not the previous ones because (afaict) the elaborator sees the local context but not the global context.

[Tragicus]

As your tests show, the sort coercion postcomposes and does not precompose with Coq's coercions. This is because when the algorithm sees that the type of the input term is a structure, it applies the projection and then asks for a coercion to the target type.
The converse holds for the reverse coercion: it precomposes and does not postcompose with Coq's coercions. This is because when the algorithm sees that the target type is a structure, it tries to build the package and lets the elaborator find the missing class. I assume that the elaborator also catches the type mismatch of the subjects and looks for a coercion.

[gares]

About post composition, the code does not look at the expected type. If the inferred type is a structure it elaborates (sort t) against the expected type. So Coq can insert further coercions.

If the inferred type is not a structure, then it does nothing.

In your last examples I think that the first coercion from C to sigType is inserted by Coq, then elpi goes to A and then Coq goes to C.

I'm not so sure I see a use case for something (that is not a structure) coercing to a structure.

[CohenCyril]

I'm not so sure I see a use case for something (that is not a structure) coercing to a structure.

One way to test it on a large scale would be to systematically replace Coq coercions by elpi coercions even for structures in Type and see if/where it breaks.

[Tragicus]

A use case for something that is not a structure coercing to a structure is when you have an object that satisfies properties that would promote it to a structure, e.g. morphisms and subobjects. This coercion allows you to skip the packaging phase.

[gares]

IMO, the only missing bit is a documentation, et least in the changelog.

[gares]

@CohenCyril can you look at the PR again and decide what to do?

[CohenCyril]

Isn't this completely ortogonal to the coercion part?
To me these raises yet unresolved nontrivial. I have nothing against merging it, but, just in case, I would prefer that it is a distinct commit/PR so that we can revert easily if something goes wrong.

[gares]

maybe an #[predicate_subtype] default to false?

[CohenCyril]

Yes or rather #[typeclass]

[Tragicus]

Sorry for the delay, I rewrote the history as suggested and added a typeclass option.

[gares]

Suggested change

	From elpi Require Import elpi coercion.
	From elpi Require Import elpi.
	From elpi.apps Require Import coercion.

[gares]

Suggested change

	mk-reverse-coercion-aux (prod _N _T Body) Structure G Args Clause :-
	Clause = (pi x\ C x),
	pi x\ mk-reverse-coercion-aux (Body x) Structure G [x | Args] (C x).
	mk-reverse-coercion-aux (prod _N _T Body) Structure G Args (pi x\ C x) :-
	pi x\ mk-reverse-coercion-aux (Body x) Structure G [x | Args] (C x).

[gares]

Suggested change

	coq.typecheck (global Structure) T ok,
	coq.env.typeof Structure T,

[gares]

Suggested change

	coq.typecheck Structure T ok,
	std.assert-ok! (coq.typecheck Structure T) "anomaly: mk-sort-coercion",

[gares]

I did a couple of suggestions, to be tested. Other than that it looks OK. @CohenCyril ?

[CohenCyril]

Taking a look this afternoon

[CohenCyril]

Could you squash and rebase?
I am considering backtracking on the default status of #[typeclass], would you mind running a bench to check the impact on MC and MCA in both scenarios?

[Tragicus]

Do we have tools to do a benchmark?

[gares]

I think it would be enough to time make -j1.
You can also make TIMED=1 to get a per file compilation time.

[Tragicus]

Ok thanks, I will do that tonight or tomorrow.

[Tragicus]

It took forever, but the bench is done. Interestingly enough, the version with typeclasses by default is slightly slower and uses slightly less memory, though the difference is negligible.
bench.ods Should I compare with a bench of master?

[Tragicus]

Well, I did it anyway, and master is about 3x faster than proto-coercion.
bench.ods.

[Tragicus]

Here is the new bench, proto-coercion is a little less than 2x slower than master. The profiling might be complicated since the slowdown occurs in tactics like apply:.
benchcoe.ods

[gares]

Damn, I guess we will have to wait for some speedup in the bootstrap time of elpi... or disable coercion in apply: but I don't know if the api makes it easy.