Declaring record constructor as Canonical · Coq users

Stream: Coq users

Topic: Declaring record constructor as Canonical

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.

Ali Caglayan (Mar 31 2022 at 14:47):

I would have thought that would work.

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.

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).

Paolo Giarrusso (Mar 31 2022 at 14:52):

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

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).

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.

Pierre Roux (Mar 31 2022 at 14:53):

(just like Canonical Structure and Canonical)

Paolo Giarrusso (Mar 31 2022 at 14:53):

Manual agrees. TIL.

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.

Ali Caglayan (Mar 31 2022 at 14:56):

I get (as expected):

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

Ali Caglayan (Mar 31 2022 at 14:57):

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

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?

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

Pierre Roux (Mar 31 2022 at 15:07):

Ok, so here is what happens:

you give A : Type where ?x : pType is expected
no coercion Sortclass >-> pType but (according to Print Graph) we have [pointed_type] : pType ↣ Sortclass (reversible)
so reversible coercions look for ?x : pType such that pointed_type ?x = A
and canonical structure mechanism infers ?x = Build_pType' A _
finally, typeclass resolution fills the last _ with a

Sounds fine, congrats!

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.

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.

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.

Ali Caglayan (Mar 31 2022 at 15:18):

Ali Caglayan (Mar 31 2022 at 15:19):

Alright pushed

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.

Pierre Roux (Mar 31 2022 at 15:35):

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

Gaëtan Gilbert (Mar 31 2022 at 15:35):

you can use Type instead of Check to forbid evars

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?

Ali Caglayan (Mar 31 2022 at 15:41):

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

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

Ali Caglayan (Mar 31 2022 at 16:06):

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

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)

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 .

Ali Caglayan (Mar 31 2022 at 16:26):

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

Pierre Roux (Mar 31 2022 at 16:28):

Not that I know.

Notification Bot (Mar 31 2022 at 16:33):

Ali Caglayan has marked this topic as resolved.

Notification Bot (Apr 04 2022 at 09:32):

Cyril Cohen has marked this topic as unresolved.

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 := ....

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.

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.

Ali Caglayan (Apr 04 2022 at 13:26):

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

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'.

Ali Caglayan (Apr 04 2022 at 13:27):

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

Ali Caglayan (Apr 04 2022 at 13:32):

I guess pretyping maintainers?

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.

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.

Ali Caglayan (Apr 04 2022 at 14:10):

Pierre Roux said:

Ok, so here is what happens:

you give A : Type where ?x : pType is expected

no coercion Sortclass >-> pType but (according to Print Graph) we have [pointed_type] : pType ↣ Sortclass (reversible)

so reversible coercions look for ?x : pType such that pointed_type ?x = A

and canonical structure mechanism infers ?x = Build_pType' A _

finally, typeclass resolution fills the last _ with a

Sounds fine, congrats!

And here is the explanation.

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

Ali Caglayan (Apr 04 2022 at 14:15):

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

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.

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.

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.

Enrico Tassi (Apr 04 2022 at 14:24):

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

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).

Ali Caglayan (Apr 04 2022 at 14:27):

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

Enrico Tassi (Apr 04 2022 at 14:28):

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

Enrico Tassi (Apr 04 2022 at 14:28):

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

Ali Caglayan (Apr 04 2022 at 14:29):

(deleted bc confused)

Ali Caglayan (Apr 04 2022 at 14:32):

Why is the eta expansion bad?

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.

Ali Caglayan (Apr 04 2022 at 14:41):

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

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).

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: Oct 01 2023 at 18:01 UTC