## Stream: Coq users

### Topic: Struggle with using canonical structures mathcomp style

#### walker (Oct 28 2022 at 14:40):

So this snippet follows the default example from "Canonical structures for the working Coq user paper".

``````Record operations (A B: eqType) (M: Type) := Operations {
Empty : M;
Lookup : A -> M -> option B;
}.

Structure type :=  Pack{
AT: eqType;
BT: eqType;
MT: Type;
ops: operations AT BT MT;
}.

Definition empty (e: type): (MT e) :=
let 'Pack _ _ _ (Operations x _):= e in x.
(* lookup works the same way*)
``````

However, when I try to extend the `type` structure with another element that holds lemmas as follows:

``````Record lemmas (A B: eqType) (M: Type) (ops: operations A B M) := Lemmas {
Extensionality: forall m1 m2,
(forall i , Lookup ops i m1 = Lookup ops i m2) ->
m1 = m2
}.
Structure type :=  Pack{
AT: eqType;
BT: eqType;
MT: Type;
ops: operations AT BT MT;
lms: lemmas ops;
}.
``````

Things break all the sudden:

trying to define the `empty` method fails:

``````Definition empty (e: type): (MT e) :=
let 'Pack _ _ _ (Operations x _) _:= e in x.
``````

gives the following error message:

``````In environment
e : type
t : eqType
t0 : eqType
T : Type
o : operations t t0 T
l : lemmas o
x : T
o0 : t -> T -> option t0
The term "x" has type "T" while it is expected to have type
"MT
?t@{e1:={|
AT := t;
BT := t0;
MT := T;
ops := {| Empty := x; Lookup := o0 |};
lms := l
|}}".
``````

There are error messages which I don't understand at all, this one I actually understand what the error is saying.

It thinks that "MT {.... MT:=T.....}" and "T" are not the same thing but they are it is just beta reduction from direction to the other.

I was actually able to convince coq with that using as follows:

``````Definition empty (e: type): (MT e).
Proof.
destruct e.
destruct ops0.
apply Empty0.
Defined.
``````

So here are my questions:

A- Why does coq rejecteced the first definition?
B- How to make coq accept a definition without ltac?
C- is that the idiomatic way to do things (if not what it is the idiomatic way)?

#### Gaëtan Gilbert (Oct 28 2022 at 15:05):

smaller example:

``````Structure type :=  Pack{
MT: Type;
ops: MT * unit;
lms: ops = ops;
}.

Definition empty (e: type): (MT e) :=
match e with {| ops := (x, _) |} => x end.
``````

this works if the `lms : ops = ops;` line is removed
we may also note that with it present,

``````Definition empty (e: type): (MT e) :=
match e return MT e with {| ops := (x, _) |} => x end.
``````

produces a strange error

``````Error: Illegal application:
The term "Pack" of type "forall (MT : Type) (ops : MT * unit), ops = ops -> type"
cannot be applied to the terms
"MT" : "Type"
"ops0" : "(MT * unit)%type"
"lms" : "ops = ops"
The 3rd term has type "ops = ops" which should be coercible to "ops0 = ops0".
``````

and using `return _` produces an error which mentions `(cannot satisfy constraint "T" == "MT ?t@{e0:=e; e:={| MT := T; ops := (x, u) |}}")` regardless of having `lms`

pattern matching elaboration has 2 strategies that it tries to produce the return clause, my guess is that without `lms` it succeeds with one that is close to what happens with explicit `return M e`, but with `lms` that fails and then you get the error for the other strategy which is more like `return _`
The "illegal application" error with `lms` and explicit `return MT e` seems like a bug to me

#### Notification Bot (Oct 28 2022 at 15:06):

Enzo Crance has marked this topic as resolved.

#### Notification Bot (Oct 28 2022 at 15:06):

Enzo Crance has marked this topic as unresolved.

#### walker (Oct 28 2022 at 15:17):

The error message gets better when we import the following:

``````From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
``````

before the `Structure` and the `Definition`

It is similar to my old error message:

``````The term "x" has type "T" while it is expected to have type
"MT ?t@{e1:={| MT := T; ops := (x, u); lms := e0 |}}".
``````

I am not sure how to fix it here either, I will move the question to math-com stream since they use similar patterns in the library.

#### Gaëtan Gilbert (Oct 28 2022 at 15:21):

There are error messages which I don't understand at all, this one I actually understand what the error is saying.

It thinks that "MT {.... MT:=T.....}" and "T" are not the same thing but they are it is just beta reduction from direction to the other.

no, it thinks that `MT ?t@{e1 := {| ... MT := T ... |} }` and `T` are not the same thing

#### walker (Oct 28 2022 at 15:30):

``````From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Record operations (A B: eqType) (M: Type) := Operations {
Empty : M;
Lookup : A -> M -> option B;
}.

Structure type :=  Pack{
AT: eqType;
BT: eqType;
MT: Type;
ops: operations AT BT MT;
}.

Definition empty (e: type): (MT e) :=
let 'Pack _ _ _ (Operations x _):= e in x.
``````

If I try to define a structure that depends on operations for specifying lemmas for those operations:
as follows:

``````Record lemmas (A B: eqType) (M: Type) (ops: operations A B M) := Lemmas {
Extensionality: forall m1 m2,
(forall i , Lookup ops i m1 = Lookup ops i m2) ->
m1 = m2
}.
Structure type :=  Pack{
AT: eqType;
BT: eqType;
MT: Type;
ops: operations AT BT MT;
lms: lemmas ops;
}.

Definition empty (e: type): (MT e) :=
let 'Pack _ _ _ (Operations x _) _:= e in x.
``````

Coq rejects the definition of empty, it cannot unify `(MT e)` with the type of the expression, even though it should have,

My main questions are how to fix it, and what would be the mathcomp idiomatic way of doing what I am trying to do, I tried reading code from mathcomp library but I got lost

#### walker (Oct 28 2022 at 15:31):

I don't have permissions to move threads around. please lets take the discussion there.

#### Notification Bot (Oct 28 2022 at 15:31):

walker has marked this topic as resolved.

#### 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):

Last updated: Oct 03 2023 at 21:01 UTC