Reversible coercions by gares · Pull Request #15693 · rocq-prover/rocq

gares · 2022-02-16T10:43:49Z

Intro:
This PR implements a feature along the lines of https://arxiv.org/abs/1103.3320 where any term t (even a type) can be elaborated to another term s whenever t ~c~> t' via regular a coercion path c (even of length 0) and t' <~rc~ s via a reversible coercion path rc. Reversible coercions are coercions that are also equipped with canonical inference. The elaboration is obtained by solving the unification problem c t ==?== rc ?s (t' is c t, rc is a canonical projection).

As a result a function f taking a record argument (eg an eqType) can be passed a naked type (eg nat) and be elaborated to f nat_eqType (in this case c has length 0, t' is nat already). In the usual coercion jargon this is Sortclass >-> eqType which cannot be a type theoretic function (you can't match on inhabitants of Type), hence the unification and its hints are defining how this "coercion" is computed.

In the presence of a hierarchy with a diamond (made of left right bottom top), a function can expect the left structure and be passed the an inhabitant of the right structure, since that term can be directly coerced to the bottom structure and enriched back (reverse coerced) to the left one. We try to compute the pushout if it exists, that is, if bottom has a coercion to a simpler structure lower (bottom inherits lower), we don't coerce to lower and enrich back to left (we try to lose as little information as possible via direct coercions).

       top
   /        \
left      right
  \          /
     bottom
      |
     lower

TODO:

fix the trace: add a constructor that means (fun _ => the_new_term)
attribute syntax, then filter the reverse path search using only allowed (flagged as reverse) coercions
tests for parameters
doc
changelog

MAYBE another PR:

interleave regular coercions and reverse coercions as in (x : R) >-> S <~< T to enrich x to T lowering it down first to S.

SkySkimmer · 2022-02-16T15:25:29Z

bench https://gitlab.com/coq/coq/-/jobs/2100592270

coqbot-app · 2022-02-16T16:57:58Z

🔴 CI failure at commit 246cc44 without any failure in the test-suite

✔️ Corresponding job for the base commit 3786a4a succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-elpi

You can also pass me a specific list of targets to minimize as arguments.

SkySkimmer · 2022-02-16T17:03:00Z

Quite high compatibility (elpi is testing the absence of this feature)

coqbot-app · 2022-02-17T04:04:35Z

🔴 CI failure at commit 246cc44 without any failure in the test-suite

✔️ Corresponding job for the base commit 3786a4a succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-elpi

You can also pass me a specific list of targets to minimize as arguments.

gares · 2022-02-17T05:47:52Z

The bench is noise, indeed we cover a case which was a hard failure in developments with no ltac proof search.

gares · 2022-02-17T12:50:55Z

pretyping/coercion.ml

+  (* XXX this order relation is not total ... *)
+  let r = List.sort (fun c1 c2 -> if ClTypSet.mem c1 (reachable_from c2) then 1 else -1) r in


@pi8027 do you know what happens if List.sort is given an "non order" relation (like this one, which is not total and not anti-symmetric)?

There is a stable_sort close to sort https://ocaml.org/api/List.html#VALsort so List.sort may or may not be stable, that's unspecified.

In some sense, if it returns a permutation of the input given a random relation, it is still ok, if it asserts false... it is not

That should be fine (the above doc doesn't expect a total order, any preorder is fine).

And looking at the current implementation, it cannot throw an exception https://github.com/ocaml/ocaml/blob/trunk/stdlib/list.ml#L320

There is a stable_sort close to sort https://ocaml.org/api/List.html#VALsort so List.sort may or may not be stable, that's unspecified.

@proux01 Well if we start trusting implementations rather than specifications now, we see that sort = stable_sort... 😆

gares · 2022-02-17T13:30:45Z

@charguer this PR also makes your example in this discourse post by declaring a default canonical structure (the eta expansion of the record) (plus the magic done here).

CohenCyril · 2022-02-17T13:44:55Z

test-suite/success/reverse_coercions_ac.v

+
+(* Above, it would be nice to write [eapply (T A)], or just [eapply T].
+   For that, we'd need to coerce [A:Type] to the type [IType]
+   by applying on-the-fly the operation [IType_make A _]. Thus, we need something like:
+   [Coercion (fun (A:Type) => IType_make A _) : Sortclass >-> IType.] 
+  Would that be possible?
+
+  I understand that [IType_type] is already a reverse coercion from [IType] to [Type],
+  but I don't see why it would necessarily cause trouble to have cycles
+  in the coercion graphs. *)
+
+


We can remove this part of the test file :)

(FTR, you can push to this branch on my GH space)

CohenCyril · 2022-02-17T13:45:15Z

test-suite/success/reverse_coercions_ac.v

+
+Arguments IType_make IType_type {IType_inhab}.


This is unnecessary

gares · 2022-02-17T14:59:19Z

I broke this test Check (nat : Type) : Set. which now passes but should not.
Maybe we manage to coerce Type -> Set since the class is the same and now we consider identity coercions from a type to itself as a path?

gares · 2022-02-17T15:49:14Z

And we broke mathcomp, but I did not investigate why.

CohenCyril · 2022-02-18T10:55:23Z

And we broke mathcomp, but I did not investigate why.

actually... the test suite is broken ;)

gares · 2022-02-18T16:33:53Z

This last commit is the fix I had initially in mind. It just avoids to use reverse coercions if the two endpoints are the same

coqbot-app · 2022-02-18T17:49:34Z

🔴 CI failure at commit 1ff839b without any failure in the test-suite

✔️ Corresponding job for the base commit dc5e355 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-elpi

You can also pass me a specific list of targets to minimize as arguments.

gares · 2022-02-18T17:56:43Z

We re back on track, maybe you can play a bit more with mathcomp to test this better?

coqbot-app · 2022-02-18T20:10:46Z

🔴 CI failure at commit 1ff839b without any failure in the test-suite

✔️ Corresponding job for the base commit dc5e355 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-elpi

You can also pass me a specific list of targets to minimize as arguments.

CohenCyril · 2022-02-21T05:21:51Z

We re back on track, maybe you can play a bit more with mathcomp to test this better?

Sure, I'd like to play a bit with mathcomp on HB & categories on HB actually... but I'm struggling to compile coq-elpi on my computer 😢

gares · 2022-02-21T08:42:08Z

Hum, the PR was just accepted in nixpkgs. For coq-elpi master you need a new elpi

CohenCyril · 2022-02-21T16:48:05Z

For coq-elpi master you need a new elpi

Which one?

gares · 2022-02-21T16:51:27Z

1.14.x (it should be the default on nix as well since that PR)

CohenCyril · 2022-02-22T16:21:53Z

Do you know what I am doing wrong?

File "src/coq_elpi_vernacular.ml", line 767, characters 8-36:
767 |     try ComExtraDeps.query_extra_dep id
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Unbound module ComExtraDeps
make[1]: *** [Makefile.coq:735: src/coq_elpi_vernacular.cmo] Error 2
make[1]: *** Waiting for unfinished jobs....
make: *** [Makefile:38: build] Error 2

gares · 2022-02-22T16:49:53Z

you are using the coq-master branch of coq elpi against coq 8.15 I guess

gares · 2022-02-23T08:48:30Z

No, the problem is that elpi-master moved because of a PR, but this branch was not rebased. I'm doing it now

gares · 2022-04-28T13:51:03Z

rebased together with the overlay

gares · 2022-04-29T15:16:28Z

ping

ppedrot · 2022-04-29T15:34:16Z

You should probably ping @mattam82 directly. If he doesn't answer soon, I can take over if needed. It's just a matter of merging it so...

gares · 2022-05-02T12:15:19Z

ping @mattam82 @ppedrot

doc/changelog/02-specification-language/15693-reverse-coercions.rst

doc/sphinx/addendum/implicit-coercions.rst

ppedrot · 2022-05-02T14:48:25Z

@gares OK, I'm taking over, but before merging I'll wait for the doc tweaks.

mattam82 · 2022-05-02T15:06:28Z

@ppedrot I was waiting for the doc changes as well, so whoever comes first when they're here can merge :)

gares · 2022-05-02T15:52:04Z

I'm fine with the changes but I won't be able to work on them today, not tomorrow. @CohenCyril @proux01 if you could step in for that last change...

gares · 2022-05-03T05:15:49Z

Thanks

ppedrot · 2022-05-03T06:34:40Z

@coqbot merge now

coqbot-app · 2022-05-03T06:34:41Z

@ppedrot: You can't merge the PR because it hasn't been approved yet.

ppedrot · 2022-05-03T06:35:13Z

@coqbot merge now

coqbot-app · 2022-05-03T06:35:16Z

@ppedrot: Please take care of the following overlays:

15693-gares-reverse-coercions.sh

Adapt to rocq-prover/rocq#15693

356: Adapt to rocq-prover/rocq#15693 r=Janno a=proux01 To be merged in sync with the upstream PR rocq-prover/rocq#15693 Co-authored-by: Pierre Roux <pierre@roux01.fr>

Adapt to rocq-prover/rocq#15693

gares force-pushed the reverse-coercions branch from 4647a9c to 06afcfd Compare February 17, 2022 12:48

gares commented Feb 17, 2022

View reviewed changes

CohenCyril reviewed Feb 17, 2022

View reviewed changes

gares force-pushed the reverse-coercions branch 2 times, most recently from 481345b to 1a29053 Compare February 23, 2022 09:06

gares added a commit to gares/hierarchy-builder that referenced this pull request Feb 23, 2022

adapt to rocq-prover/rocq#15693

4d4bdb9

gares added the kind: feature New user-facing feature request or implementation. label Feb 23, 2022

gares added this to the 8.16+rc1 milestone Feb 23, 2022

gares mentioned this pull request Feb 23, 2022

[DO NOT MERGE] test reverse coercions math-comp/math-comp#853

Closed

gares mentioned this pull request Apr 28, 2022

[ci] bump elpi (goodbye camlp5, hello menhir) #15948

Merged

gares added a commit to gares/hierarchy-builder that referenced this pull request Apr 28, 2022

adapt to rocq-prover/rocq#15693

873c18f

gares added 2 commits April 28, 2022 14:07

[elaborator] reversible coercions

71f6dc9

test suite

1d20385

gares force-pushed the reverse-coercions branch from 516cef9 to 5cf4262 Compare April 28, 2022 12:07

Zimmi48 reviewed May 2, 2022

View reviewed changes

doc/changelog/02-specification-language/15693-reverse-coercions.rst Outdated Show resolved Hide resolved

doc/sphinx/addendum/implicit-coercions.rst Outdated Show resolved Hide resolved

ppedrot self-assigned this May 2, 2022

gares added 2 commits May 2, 2022 23:15

documentation

ececf11

overlay

306c320

proux01 force-pushed the reverse-coercions branch from 5cf4262 to 306c320 Compare May 2, 2022 21:15

ppedrot approved these changes May 3, 2022

View reviewed changes

coqbot-app bot merged commit b2750f9 into rocq-prover:master May 3, 2022

gares added a commit to LPCIC/coq-elpi that referenced this pull request May 3, 2022

Merge pull request #355 from proux01/coq_15693

ee028f5

Adapt to rocq-prover/rocq#15693

ppedrot mentioned this pull request May 3, 2022

adapt to coq/coq#15693 math-comp/hierarchy-builder#289

Merged

bors bot added a commit to Mtac2/Mtac2 that referenced this pull request May 3, 2022

Merge #356

a971b4b

356: Adapt to rocq-prover/rocq#15693 r=Janno a=proux01 To be merged in sync with the upstream PR rocq-prover/rocq#15693 Co-authored-by: Pierre Roux <pierre@roux01.fr>

bors bot added a commit to Mtac2/Mtac2 that referenced this pull request May 3, 2022

Merge #356

a0c3a25

356: Adapt to rocq-prover/rocq#15693 r=Janno a=proux01 To be merged in sync with the upstream PR rocq-prover/rocq#15693 Co-authored-by: Pierre Roux <pierre@roux01.fr>

Janno pushed a commit to Mtac2/Mtac2 that referenced this pull request May 3, 2022

Merge pull request #356 from proux01/coq_15693

4ae6345

Adapt to rocq-prover/rocq#15693

herbelin mentioned this pull request Jul 26, 2023

Record coercion allows bad function definitions #17863

Closed

		(* XXX this order relation is not total ... *)
		let r = List.sort (fun c1 c2 -> if ClTypSet.mem c1 (reachable_from c2) then 1 else -1) r in

Conversation

gares commented Feb 16, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Overlays to be merged after the PR

Overlays to be merged before the PR

Overlays to be merged in sync with the PR

Uh oh!

SkySkimmer commented Feb 16, 2022

Uh oh!

coqbot-app bot commented Feb 16, 2022

Uh oh!

SkySkimmer commented Feb 16, 2022

Uh oh!

coqbot-app bot commented Feb 17, 2022

Uh oh!

gares commented Feb 17, 2022

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gares commented Feb 17, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gares commented Feb 17, 2022

Uh oh!

gares commented Feb 17, 2022

Uh oh!

CohenCyril commented Feb 18, 2022

Uh oh!

gares commented Feb 18, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

coqbot-app bot commented Feb 18, 2022

Uh oh!

gares commented Feb 18, 2022

Uh oh!

coqbot-app bot commented Feb 18, 2022

Uh oh!

CohenCyril commented Feb 21, 2022

Uh oh!

gares commented Feb 21, 2022

Uh oh!

CohenCyril commented Feb 21, 2022

Uh oh!

gares commented Feb 21, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

CohenCyril commented Feb 22, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

gares commented Feb 22, 2022

Uh oh!

gares commented Feb 23, 2022

Uh oh!

gares commented Apr 28, 2022

Uh oh!

gares commented Apr 29, 2022

Uh oh!

ppedrot commented Apr 29, 2022

Uh oh!

gares commented May 2, 2022

Uh oh!

Uh oh!

Uh oh!

ppedrot commented May 2, 2022

gares commented Feb 16, 2022 •

edited

Loading

gares commented Feb 17, 2022 •

edited

Loading

gares commented Feb 18, 2022 •

edited

Loading

gares commented Feb 21, 2022 •

edited

Loading

CohenCyril commented Feb 22, 2022 •

edited

Loading