Stream: Coq users

Topic: Struggle with using canonical structures mathcomp style

Notification Bot (Oct 28 2022 at 17:44):

Cyril Cohen has marked this topic as unresolved.

Notification Bot (Oct 28 2022 at 17:47):

This topic was moved here from #Coq users > Struggle with using canonical structures mathcomp style by Cyril Cohen.

Notification Bot (Oct 28 2022 at 17:47):

This topic was moved to #math-comp users > Struggle with using canonical structures mathcomp style by Cyril Cohen.

Cyril Cohen (Oct 28 2022 at 17:58):

I blindly followed the suggestion to move this to #math-comp users but it has nothing to do with mathcomp. It's a Coq bug... So I'm moving it back.

Notification Bot (Oct 28 2022 at 17:58):

This topic was moved here from #math-comp users > Struggle with using canonical structures mathcomp style by Cyril Cohen.

Cyril Cohen (Oct 28 2022 at 18:02):

Here are three workarounds:

Structure type :=  Pack{
    MT: Type;
    ops: MT * unit;
    lms: ops = ops;
}.
(* Call already defined projections *)
Definition emtpy1 (e : type) : MT e := (ops e).1.
(* Call & reduce already defined projections *)
Definition emtpy2 (e : type) : MT e := Eval cbv [ops fst] in (ops e).1.
(* Decompile deep pattern matching manually *)
Definition empty3 (e : type) : MT e :=
    match e with {| ops := x |} => match x with (o, _) => o end end.

walker (Oct 28 2022 at 19:58):

given that this is a bug, should I open an issue on github ?

Gaëtan Gilbert (Oct 28 2022 at 20:11):

I opened https://github.com/coq/coq/issues/16749

Last updated: Jan 31 2023 at 14:03 UTC