Stream: Coq users

Topic: Declaring record constructor as Canonical


view this post on Zulip Ali Caglayan (Mar 31 2022 at 14:47):

@Pierre Roux Here is the example

Set Primitive Projections.

Class IsPointed (A : Type) := point : A.

Record pType : Type := {
  pointed_type : Type ;
  ispointed_pointed_type : IsPointed pointed_type ;
}.
#[reversible]
Coercion pointed_type : pType >-> Sortclass.
Fail Canonical Build_pType.

view this post on Zulip Ali Caglayan (Mar 31 2022 at 14:47):

I would have thought that would work.

view this post on Zulip Ali Caglayan (Mar 31 2022 at 14:47):

Especially with this message:

The command has indeed failed with message:
Could not declare a canonical structure Build_pType.
Expected an instance of a record or structure.

view this post on Zulip Pierre Roux (Mar 31 2022 at 14:51):

Indeed, my suggestion was wrong, Build_pType is not a record (that's why you had to declare fun A a => Build_pType A a as canonical instance).

view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 14:52):

is Canonical Structure supposed to work if pType isn't a Structure?

view this post on Zulip Pierre Roux (Mar 31 2022 at 14:52):

But I'm still puzzled because I don't get why your example (https://github.com/coq/coq/pull/15693#issuecomment-1084672056) works (I tried to comment out #[reversible] and it then fails but I don't see where the reversible coercion plays a role).

view this post on Zulip Pierre Roux (Mar 31 2022 at 14:53):

Paolo Giarrusso said:

is Canonical Structure supposed to work if pType isn't a Structure?

Structure and Record are perfect synonyms.

view this post on Zulip Pierre Roux (Mar 31 2022 at 14:53):

(just like Canonical Structure and Canonical)

view this post on Zulip Paolo Giarrusso (Mar 31 2022 at 14:53):

Manual agrees. TIL.

view this post on Zulip Ali Caglayan (Mar 31 2022 at 14:56):

@Pierre Roux Are you confused about what is going on here:

Set Primitive Projections.

Class IsPointed (A : Type) := point : A.

Record pType : Type := {
  pointed_type : Type ;
  ispointed_pointed_type : IsPointed pointed_type ;
}.
#[reversible]
Coercion pointed_type : pType >-> Sortclass.
Fail Canonical Build_pType.
Canonical Structure Build_pType' (A : Type) (a : IsPointed A) := Build_pType A a.

Axiom A : Type.
#[export]
Instance a : IsPointed A. Proof. Admitted.

Axiom lemma_about_ptype : forall (X : pType), Type.

Definition foo := lemma_about_ptype A.
Eval cbv in foo.

view this post on Zulip Ali Caglayan (Mar 31 2022 at 14:56):

I get (as expected):

     = lemma_about_ptype
         {|
           pointed_type := A;
           ispointed_pointed_type := a
         |}
     : Type

view this post on Zulip Ali Caglayan (Mar 31 2022 at 14:57):

My previous Canonical Structure was wrong, I needed IsPointed A rather than just A.

view this post on Zulip Ali Caglayan (Mar 31 2022 at 14:58):

It seems that the canonical structure isn't working before, but is now working correctly due to reversible coercions?

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:03):

btw if anybody else is watching we are looking at the behaviour of https://github.com/coq/coq/pull/15693

view this post on Zulip Pierre Roux (Mar 31 2022 at 15:07):

Ok, so here is what happens:

Sounds fine, congrats!

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:09):

Would you like to have my example as a test in the PR? I can push a commit if you like.

view this post on Zulip Pierre Roux (Mar 31 2022 at 15:10):

Check the already existing examples but I don't think we have one mixing CS and TC this way, so yes.

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:14):

What should I call the file? I have the same initials as Arthur so reverse_coercions_ac is already taken.

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:18):

:)

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:19):

Alright pushed

view this post on Zulip Pierre Roux (Mar 31 2022 at 15:34):

Note that in you example, the Check could enable remaining evars, maybe the last Check could be replaced by a Definition to avoid that.

view this post on Zulip Pierre Roux (Mar 31 2022 at 15:35):

(and you can put your name rather than mine ;) )

view this post on Zulip Gaëtan Gilbert (Mar 31 2022 at 15:35):

you can use Type instead of Check to forbid evars

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:38):

Gaëtan Gilbert said:

you can use Type instead of Check to forbid evars

That's amazing. Do we not document this anywhere?

view this post on Zulip Ali Caglayan (Mar 31 2022 at 15:41):

Seems not, I created an issue: https://github.com/coq/coq/issues/15881

view this post on Zulip Ali Caglayan (Mar 31 2022 at 16:04):

With regard to the canonical decleration, is this a bug?

Record A := {
  a : nat ;
}.

Record A := {
  a : nat ;
}.

Fail Canonical Build_A.
Fail Canonical Build_A' := Build_A.
Canonical Build_A' a := Build_A a.

Perhaps I should file an issue?
cc @Enrico Tassi

view this post on Zulip Ali Caglayan (Mar 31 2022 at 16:06):

Maybe the canonical command needs to be a bit smarter here?

view this post on Zulip Pierre Roux (Mar 31 2022 at 16:23):

Not a bug, neither Build_A nor Build_A' are records (Build_A 0 is for instance)

view this post on Zulip Pierre Roux (Mar 31 2022 at 16:24):

That's why the last one works, it literally means, provided some a, then Build_A a is a canonical instance .

view this post on Zulip Ali Caglayan (Mar 31 2022 at 16:26):

Is there a way to do this without the auxiliary definition however?

view this post on Zulip Pierre Roux (Mar 31 2022 at 16:28):

Not that I know.

view this post on Zulip Notification Bot (Mar 31 2022 at 16:33):

Ali Caglayan has marked this topic as resolved.

view this post on Zulip Notification Bot (Apr 04 2022 at 09:32):

Cyril Cohen has marked this topic as unresolved.

view this post on Zulip Cyril Cohen (Apr 04 2022 at 09:34):

I beg to disagree, right now I'm rooting to consider this a bug: I do not see why Canonical must be a in the form Canonical c x : r := ...where r is a record rather than Canonical c : forall x, r := ....

view this post on Zulip Cyril Cohen (Apr 04 2022 at 09:39):

Especially when Canonical c (with c being an existing global constant) works however you defined it, but does not work if it is a constructor.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 13:20):

@Cyril Cohen I was planning to open an issue for this, so I am glad to see you think it is too.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 13:26):

https://github.com/coq/coq/issues/15898

view this post on Zulip Ali Caglayan (Apr 04 2022 at 13:26):

Here is a short example of the issue:

Record A := Build_A {
  a : nat ;
}.

Fail Canonical Build_A.

Definition Build_A' a := Build_A a.

Canonical Build_A'.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 13:27):

By the way, we don't have a maintainer team for canonical structures right?

view this post on Zulip Ali Caglayan (Apr 04 2022 at 13:32):

I guess pretyping maintainers?

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:10):

@Enrico Tassi The reason I want to declare Build_A as a canonical instance is stemming from this thread.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:10):

So I had this:

Set Primitive Projections.

Class IsPointed (A : Type) := point : A.

Record pType : Type := {
  pointed_type : Type ;
  ispointed_pointed_type : IsPointed pointed_type ;
}.
#[reversible]
Coercion pointed_type : pType >-> Sortclass.
Fail Canonical Build_pType.
Canonical Structure Build_pType' (A : Type) (a : IsPointed A) := Build_pType A a.

Axiom A : Type.
#[export]
Instance a : IsPointed A. Proof. Admitted.

Axiom lemma_about_ptype : forall (X : pType), Type.

Definition foo := lemma_about_ptype A.
Eval cbv in foo.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:10):

Pierre Roux said:

Ok, so here is what happens:

Sounds fine, congrats!

And here is the explanation.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:15):

I want Coq to elaborate (for (X : Type), (X : myRecord) into (Build_myRecord X _ _ : myRecord) and fill the rest of the holes in with tc search

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:15):

A combination of reversible coercions, canonical structures and typeclasses allows us to do this

view this post on Zulip Enrico Tassi (Apr 04 2022 at 14:17):

OK, this is the only case i know in which you want to declare a constructor as canonical. It is the failsafe example at page 15 here: https://hal.inria.fr/hal-00816703v1

I think I would prefer a special command for that, a command that suggests your are not really giving a canonical solution, but rather deferring the search to another mechanism.

view this post on Zulip Enrico Tassi (Apr 04 2022 at 14:22):

In a sense, both Build_pType and Build_pType' are very weird CS instances. Their only purpose is to make unification continue without making any progress. I mean, something like:

#[never_fail_on_CS_inference] Record pType : Type := {
  #[TC_inference_key] pointed_type : Type ;
  ispointed_pointed_type : IsPointed pointed_type ;
}.

which also asserts all fields are inferrable, directly or indirectly, via TC resolution. But I don't think it is worth it.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:23):

OK, in which case we need to implement a new vernacular for declaring such instances? I suppose we could add information to the constructor case in Canonical to suggest to the user to use this new vernacular deceleration instead, or else they will probably use an auxiliary definition workaround.

view this post on Zulip Enrico Tassi (Apr 04 2022 at 14:24):

I'm OK improving the error message, pointing to the definition work around.

view this post on Zulip Enrico Tassi (Apr 04 2022 at 14:26):

In some sense, what I don't like, is that it is a choice the library designer has to do when he crafts the record.
While Canonical is a way to retrofit things into an existing library.
IMO if would be nicer for the user if the eta expansion was always rejected (be it a definition or not) unless the record type declaration is flagged in some special way (less ugly that my example above).

It is a bit like modes for TC. The user should not touch these (in a perfect world).

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:27):

I didn't follow how eta expansion comes into this.

view this post on Zulip Enrico Tassi (Apr 04 2022 at 14:28):

CS inference is triggered on unif problem like proj ?x = val

view this post on Zulip Enrico Tassi (Apr 04 2022 at 14:28):

The CS instance you wanted to declare does ?x := K _, that is eta expands the record.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:29):

(deleted bc confused)

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:32):

Why is the eta expansion bad?

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:40):

I suppose the idea we want to get across in the syntax is this kind of CS instance is "default" like you mention in the paper.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:41):

This perhaps ties in with the notion of a constructor for a class in OOP.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 14:55):

Perhaps it is relevant that you would only want to do such a CS instance in conjunction with a reversible coercion. I had many example of this exact situation in mind, not just pType. For instance, AbGroup >-> Group (reversible) could, together with a CS instance, allow somebody to elaborate a group G into an abelian group as long as Coq can find the extra parts (eg. via tc).

view this post on Zulip Enrico Tassi (Apr 04 2022 at 18:05):

Perhaps it is relevant that you would only want to do such a CS instance in conjunction with a reversible coercion.

I don't think so. As in the paper, it made sense before reversible coercions were coded.


Last updated: Feb 04 2023 at 21:02 UTC