Stream: Coq users

Topic: new bug in cannonical structures?

walker (Nov 15 2022 at 20:40):

(sorry for not minimizing the issue, I am totally drained for trying to identify the issue)

So I am importing those files:
https://gitlab.com/thewalker77/ssrmap/-/blob/main/theories/gmap.v
https://gitlab.com/thewalker77/ssrmap/-/blob/main/theories/fin_maps.v
https://gitlab.com/thewalker77/ssrmap/-/blob/main/theories/serde.v

And The general assumption here is that equal types may be replaced by equal types, where equal as in Compute T1 and Compute T2 results in the same value

So here is the situation:

We have a record for CS:

Module FinMap.
(*stuff*)
Structure type (K: eqType):=  Pack{
    MT: eqType -> Type -> Type;
    ops: operations K MT;
    lms: lemmas ops;
}.

End FinMap.

Definition finMap := FinMap.type.
Notation MapType K V e:= ((FinMap.MT e) K V).

We have a type for trie based maps along side with the implementation of its cannonical structure:

Definition GTrie (K V: Type) := Trie.Trie V.

Canonical Structure trie_is_fin_map (K: serDeEqType) :=
    FinMap.Pack (GTrie.trie_finmap_lemmas K).

Trie.Trie does not matter same are the most of what goes inside FinMap.Pack. Worth noting that serDeEqType is another CS

Then there is the reality check:

Compute (MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq)).
(*
     = Trie.Trie bool
     : Type
*)
Compute (GTrie nat bool).
(*
     = Trie.Trie bool
     : Type
*)

(MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq)), GTrie nat bool and Trie.Trie bool are the same thing:

But then this is the problem

Check ({[1 := true]}). (*makes sense that the type has holes *)
(*
{[1 := true]}
     : MapType nat_eqType bool ?e
where
?e : [ |- FinMap.type nat_eqType]
*)
Check ({[1 := true]} : MapType _ _ (trie_is_fin_map nat_is_serde_eq)). (* Should work and does work!*)
(*
{[1 := true]} : MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq)
     : MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq)
*)
Fail Check ({[1 := true]} : GTrie nat bool). (* ??? should work but does not work! *)
(*
The command has indeed failed with message:
The term "{[1 := true]}" has type "MapType nat_eqType bool ?e"
while it is expected to have type "GTrie nat bool".
*)
Fail Check ({[1 := true]} : Trie.Trie bool). (* I get why this one fails, but equal types should be replacable, right ? *)
(*
The term "{[1 := true]}" has type "MapType nat_eqType bool ?e"
while it is expected to have type "Trie.Trie bool".
*)

Once again, I apologize for not minimizing the bug, but this one took a toll to find out

Also assuming that it is a bug, I would really like to see this one fixed asap so is this a beginner friendly bug that someone like me can work on ?

Enrico Tassi (Nov 15 2022 at 21:02):

I did not try your code but:

• CS are indexed using the declared value and projection syntactically (no quotient)
• you can declare the same (morally) CS multiple times on convertible (but different) keys

Use Print Canonical Projections to see the data base. IMO you should always pass the second argument to Pack explicitly, that is tune the implicits, since that is the key used for indexing.

walker (Nov 15 2022 at 21:13):

Well I passed the arguments manually to see if it makes a difference, and it worked! all four cases

But I don't understand the things you are trying to explain in the two points.

Also I am not sure what should I be looking for in the output of Print Canonical Projections

Enrico Tassi (Nov 15 2022 at 21:16):

Here the key value is GTrie, which is the "lowest" term all other computes to.
Unification faces problems like projection ?CS = value, and if value is a canonical key for projection then ?CS is taken from the DB

Enrico Tassi (Nov 15 2022 at 21:16):

if value is not a canonical key, it is unfolded, and then it loops

Enrico Tassi (Nov 15 2022 at 21:16):

so if you canonical value is the normal form, eventually value will be reduced to it

walker (Nov 15 2022 at 21:17):

my mistake ... it didn't actually work, it was Fail Check that was green but I was too excited to double-check fast time.

Enrico Tassi (Nov 15 2022 at 21:17):

The command prints,in an odd way, the mapping (projection,value) -> CS_instance

Enrico Tassi (Nov 15 2022 at 21:20):

But now that I look again at your script, I'm not so sure I get what you are testing

walker (Nov 15 2022 at 21:20):

So we have this:

GTrie.gtrie_finmap_ops <- FinMap.ops ( trie_is_fin_map )
GTrie.trie_finmap_lemmas <- FinMap.lms ( trie_is_fin_map )
GTrie <- FinMap.MT ( trie_is_fin_map )

Enrico Tassi (Nov 15 2022 at 21:21):

In the first example, MapType is a projection, but you also pass the projected, so there is no inference

walker (Nov 15 2022 at 21:22):

yes first example works as expeced, the problem is with this case:

Fail Check ({[1 := true]} : GTrie nat bool). (* ??? should work but does not work! *)

which is the same as the projection but less verbose

Enrico Tassi (Nov 15 2022 at 21:22):

You should try stuff lile Check (eq_refl _ : GTrie = FinMap.MT _) roughly

Enrico Tassi (Nov 15 2022 at 21:23):

the second _ is what CS fill in

Enrico Tassi (Nov 15 2022 at 21:23):

(I may not have passed all argumnets, but the heads must be that)

walker (Nov 15 2022 at 21:23):

Goal GTrie nat bool = MapType nat_eqType bool (trie_is_fin_map nat_is_serde_eq).
Proof.
by [].
Qed.

Enrico Tassi (Nov 15 2022 at 21:23):

The last line of the DB is giving a solution for that exact problem

Enrico Tassi (Nov 15 2022 at 21:24):

OK, then

Check (eq_refl _ : GTrie nat bool = MapType nat_eqType bool _)

should also work

walker (Nov 15 2022 at 21:24):

That proof is goes through.

walker (Nov 15 2022 at 21:25):

not the check one!

Enrico Tassi (Nov 15 2022 at 21:25):

Since the missing piece is the canonical solution

walker (Nov 15 2022 at 21:25):

(cannot unify "bool" and "Type").

walker (Nov 15 2022 at 21:27):

The error message in complete is :

The term "eqxx ?x" has type "is_true (?x == ?x)"
while it is expected to have type
 "GTrie nat bool = MapType nat_eqType bool ?t"
(cannot unify "bool" and "Type").

Enrico Tassi (Nov 15 2022 at 21:28):

Hum, try Check (erefl _ : ......),

Enrico Tassi (Nov 15 2022 at 21:28):

I must have done a mistake, I don't have a running Coq now

Enrico Tassi (Nov 15 2022 at 21:29):

or maybe (erefl : ... = ...), whatever types

Enrico Tassi (Nov 15 2022 at 21:30):

The idea is that you want the unification engine to solve the equation.

walker (Nov 15 2022 at 21:30):

erefl ?x
     : ?x = ?x

Enrico Tassi (Nov 15 2022 at 21:31):

great, so

Check (erefl _ : GTrie nat bool = MapType nat_eqType bool _)

walker (Nov 15 2022 at 21:32):

well it is strange, it failed again but with different error message:

The term "erefl (GTrie nat bool)" has type
 "GTrie nat bool = GTrie nat bool"
while it is expected to have type
 "GTrie nat bool = MapType nat_eqType bool ?t".

walker (Nov 15 2022 at 21:32):

but apparently coq cannot solve it

walker (Nov 15 2022 at 21:33):

once I start filling in the _ coq is able to solve it.

Enrico Tassi (Nov 15 2022 at 21:35):

can you post again you Canonical declaration with all parameters explicit?

walker (Nov 15 2022 at 21:37):

Canonical Structure trie_is_fin_map (K: serDeEqType) :=
    @FinMap.Pack (SerDeEqType.to_eq K) GTrie (GTrie.gtrie_finmap_ops K) (GTrie.trie_finmap_lemmas K).

walker (Nov 15 2022 at 21:39):

now that we are at it the SerDeEqType inherits from something called serde and eqType (at least as per my understanding of inheritence:

Module SerDeEqType.

Record mixin T := Mixin {
    Eq_type: Equality.mixin_of T;
    SerDe_ops: SerDe.operations T;
    SerDe_lemmas: SerDe.lemmas SerDe_ops;
}.

Record type := Class {
    SEQ: Type;
    ops: mixin SEQ;
}.

Definition to_eq (t: type) : eqType :=
    Equality.Pack (Eq_type (ops t)).

Definition to_serde (t: type) : serDe :=
    SerDe.Pack (SerDe_lemmas (ops t)).

End SerDeEqType.

Canonical Structure SerDeEqType.to_eq.
Canonical Structure SerDeEqType.to_serde.

walker (Nov 15 2022 at 21:39):

and nat have this implemented.

Enrico Tassi (Nov 15 2022 at 21:41):

walker said:

Canonical Structure trie_is_fin_map (K: serDeEqType) :=
    @FinMap.Pack (SerDeEqType.to_eq K) GTrie (GTrie.gtrie_finmap_ops K) (GTrie.trie_finmap_lemmas K).

something is fishy, GTrie : Type -> Type -> Type, but Pack wants a eqType -> Type -> Type...

Enrico Tassi (Nov 15 2022 at 21:42):

I'm a bit lost without a running Coq

walker (Nov 15 2022 at 21:48):

I tried doing GTrie : serDeEqType -> Type -> Type but apparently it does (and shouldn't) not work in this case and coq failed to convert it to

The term "GTrie" has type "serDeEqType -> Type -> Type"
while it is expected to have type "eqType -> Type -> Type"
(cannot unify "eqType" and "serDeEqType").

Which makes sense.

walker (Nov 15 2022 at 21:49):

in any case we can continue debugging tomorrow if you would like to.

walker (Nov 15 2022 at 21:49):

it is also getting late here.

walker (Nov 16 2022 at 10:04):

Hello again, I was able to create a relatively small self contained reproducer:

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Module SerDeEqType.
Record mixin T := Mixin {
    Eq_type: Equality.mixin_of T;
    Serialize: T -> unit;
}.
Record type := Class {
    SEQ: Type;
    ops: mixin SEQ;
}.
Definition to_eq (t: type) : eqType :=
    Equality.Pack (Eq_type (ops t)).
End SerDeEqType.
Canonical Structure SerDeEqType.to_eq.

Definition nat_serde_ops: SerDeEqType.mixin nat.
Proof.
constructor.
    apply nat_eqMixin.
intros. apply tt. Defined.
Canonical Structure nat_is_serde_eq := @SerDeEqType.Class nat nat_serde_ops.

Module FinMap.
Record operations (K: eqType) (M: eqType -> Type -> Type) := Operations {
    Empty V : M K V;
}.
Structure type (K: eqType):=  Pack{
    MT: eqType -> Type -> Type;
    ops: operations K MT;
}.
End FinMap.
Definition map_empty {K V} {e: FinMap.type K}: FinMap.MT e K V := (FinMap.Empty (FinMap.ops e) V).

Definition GTrie (K V: Type) : Type := unit.
Definition gtrie_finmap_ops (K :SerDeEqType.type):
    FinMap.operations (SerDeEqType.to_eq K) GTrie.
Proof. constructor. intros. apply tt. Defined.
Canonical Structure trie_is_fin_map (K: SerDeEqType.type) := FinMap.Pack (gtrie_finmap_ops K).

Check (map_empty : FinMap.MT (trie_is_fin_map nat_is_serde_eq) (SerDeEqType.to_eq nat_is_serde_eq) nat).
Check  (map_empty: FinMap.MT (trie_is_fin_map nat_is_serde_eq) nat_eqType nat). (* works as well*)
Fail Check (map_empty : GTrie nat nat). (* <----- I want this one to work *)

Kenji Maillard (Nov 16 2022 at 10:11):

I'm am not knowledgeable on CS, but I find suspicious that nat_serde_ops is defined with Qed: if I'm not mistaken, it means that the eqType instance contained in that definition won't be convertible to nat_eqType.

walker (Nov 16 2022 at 10:13):

right! my bad this is a bug in this minimal reproducer that was not in the original code, and fixing this makes the second check works! I edited the reproducer.

walker (Nov 16 2022 at 20:05):

via trial and error I discovered that :

Module FinMap.
Record operations (K: eqType) (M: Type -> Type -> Type) := Operations {
    Empty V : M K V;
}.
Structure type (K: eqType):=  Pack{
    MT: Type -> Type -> Type;
    ops: operations K MT;
}.
End FinMap.

Should make things work,

That said, I still believe the old FinMap module should also work and having it not working is some kind of bug in the unification algorithm.

Last updated: Sep 26 2023 at 13:01 UTC