Stream: math-comp users

Topic: Struggle with using canonical structures mathcomp style

view this post on Zulip 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

view this post on Zulip Notification Bot (Oct 28 2022 at 17:58):

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

Last updated: Feb 08 2023 at 07:02 UTC