walker (Oct 29 2022 at 19:16): walker (Oct 29 2022 at 19:16):So I am trying to do some stuff for key/value data types (maps/ trees ..etc) using cannonical structures,
The current situation is as follows:
We have canonical structure paremetrized by A, B, and type M which depends on both A and B (map from A to B)
Module FinMap.
Record operations (A B: eqType) (M: eqType -> eqType -> Type) := Operations {
Empty : M A B;
}.
Structure type := Pack{
AT: eqType;
BT: eqType;
MT: eqType -> eqType -> Type;
ops: operations AT BT MT;
}.
Definition empty (e: type): (MT e (AT e) (BT e)) := (Empty (ops e)).
Arguments empty {e} : simpl never.
End FinMap.
Here is a toy type that should implement that structure above, with toy lemma foo
(* Tree from nat to type A *)
Inductive NTree (A: eqType): Type :=
| Nempty : NTree A
(*root with stuff follows here*).
Definition ntree_finmap_ops (A: eqType): FinMap.operations nat_eqType A (fun _ x => NTree x).
Proof.
constructor.
apply Nempty.
Qed.
Canonical Structure ptree_is_finmap {A}:= FinMap.Pack (ntree_finmap_ops A).
Lemma foo: forall A, exists (x: NTree A ), x = @FinMap.empty ptree_is_finmap.
Proof. intros; eauto. Qed.
Note how foo is very annotated I assume that CS goal is to avoid this kind of annotations ?
So if I try to redo the lemma without it:
Lemma foo1: forall A, exists (x: NTree A ), x = FinMap.empty.
Admitted.
Coq complains with error
In environment
A : eqType
x : NTree A
The term "FinMap.empty" has type
"FinMap.MT ?e (FinMap.AT ?e) (FinMap.BT ?e)"
while it is expected to have type "NTree A".
It is not clear why coq fails to do the unification. if ?e is replaced by ptree_is_finmap issue should be solved. Can any one offer some insights ?
Cyril Cohen (Oct 29 2022 at 22:02):Nice, this also looks like a bug and is probably related to coq/coq#14041
Here is what I think is a minimisation of the bug:
Structure type := Pack { sort: Type -> Type }.
Canonical unit_type : type := Pack (fun _ => unit).
Check (eq_refl : sort _ = fun _ => unit).
Check (eq_refl : sort unit_type _ = unit).
Fail Check (eq_refl : sort _ _ = unit).
(maybe it's related to coq/coq#16031)
Cyril Cohen (Oct 29 2022 at 22:20):Opened issue coq/coq#16755
walker (Oct 30 2022 at 08:06):one day I will have the sufficient knowledge to send pull request to coq!
Last updated: Oct 13 2024 at 01:02 UTC