walker (Oct 28 2022 at 14:40): 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):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
walker (Oct 28 2022 at 15:31):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.
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.
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: Oct 03 2023 at 21:01 UTC