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

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

Enzo Crance has marked this topic as resolved.

Enzo Crance has marked this topic as unresolved.

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.

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

So This is follow for this thread:https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Strange.20behavior.20in.20.20Canonical.20structures/near/306677018

```
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

I manually moved the thread to https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/Struggle.20with.20using.20canonical.20structures.20mathcomp.20style/near/306685070

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

walker has marked this topic as resolved.

Cyril Cohen has marked this topic as unresolved.

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

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

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.

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

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

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

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

Last updated: Jun 24 2024 at 00:02 UTC