Stream: Coq workshop 2020

Topic: [M3] Developing sequence and tree fintypes in MathComp


view this post on Zulip Théo Zimmermann (Jun 24 2020 at 11:20):

This is the topic to ask questions on the talk "Developing sequence and tree fintypes in MathComp".

view this post on Zulip Cyril Cohen (Jul 06 2020 at 08:45):

Are you aware of the type tree here https://github.com/math-comp/math-comp/blob/e71aecf4fbb829accba495e2e7cdba1a1ddc836a/mathcomp/ssreflect/choice.v#L156 ?

Inductive tree := Leaf of T | Node of nat & seq tree.

view this post on Zulip Yves Bertot (Jul 06 2020 at 08:46):

@Cyril, can you make the question more self-contained (explain the link)?

view this post on Zulip Cyril Cohen (Jul 06 2020 at 08:47):

Yves Bertot said:

@Cyril, can you make the question more self-contained (explain the link)?

I am pointing to the definition of tree finType in mathcomp.

view this post on Zulip Enrico Tassi (Jul 06 2020 at 08:48):

This would be the doc of that tree: https://github.com/math-comp/math-comp/blob/e71aecf4fbb829accba495e2e7cdba1a1ddc836a/mathcomp/ssreflect/choice.v#L40-L46

(*      GenTree.tree T == generic n-ary tree type with nat-labeled nodes and  *)
(*                        T-labeled leaves, for example GenTree.Leaf (x : T), *)
(*                        GenTree.Node 5 [:: t; t']. GenTree.tree is equipped *)
(*                        with canonical eqType, choiceType, and countType    *)
(*                        instances, and so simple datatypes can be similarly *)
(*                        equipped by encoding into GenTree.tree and using    *)
(*                        the mixins above.                                   *)

view this post on Zulip Enrico Tassi (Jul 06 2020 at 08:51):

@Cyril Cohen the doc does not talk about finiteness

view this post on Zulip Cyril Cohen (Jul 06 2020 at 08:52):

Enrico Tassi said:

Cyril Cohen the doc does not talk about finiteness

Ah true, it handles choice and count but not finite, my mistake...

view this post on Zulip Cyril Cohen (Jul 06 2020 at 08:52):

I am thinking It could be extended in the same way as tuples...

view this post on Zulip Enrico Tassi (Jul 06 2020 at 08:53):

Agree, maybe you should formulate that as a question/suggestion for Yves to read ;-)

view this post on Zulip Reynald Affeldt (Jul 06 2020 at 08:57):

We needed trees with bounded degree when developing error-correcting codes (https://github.com/affeldt-aist/infotheo/blob/master/ecc_modern/degree_profile.v#L212-L215)

view this post on Zulip Cyril Cohen (Jul 06 2020 at 08:57):

OK I have a suggestion rather than a question: in the same way Blist would be easier defined as a sub type, {s | size s <= n}, the current tree implementation could be generalized to have an arbitrary datatype for nodes and have Btree be {t | width t w} where w : A -> nat gives the arity of each node.

view this post on Zulip Reynald Affeldt (Jul 06 2020 at 08:58):

(bounded trees were important to be able to take about finite sets of trees)

view this post on Zulip Reynald Affeldt (Jul 06 2020 at 09:00):

the height is bounded with a dependent type

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 09:00):

Wouldn't blist just 'I_n.-tuple A ?

view this post on Zulip Reynald Affeldt (Jul 06 2020 at 09:00):

so it is both bounded in height and in degree

view this post on Zulip Cyril Cohen (Jul 06 2020 at 09:00):

Emilio Jesús Gallego Arias said:

Wouldn't blist just 'I_n.-tuple A ?

because it's an inequality of size (not an equality)

view this post on Zulip Christian Doczkal (Jul 06 2020 at 09:01):

I needed length bounded lists at some point and I {s : seq T | size s < n} naturally injects into {'I_n & n.-tuple A}, which is finite by construction.

view this post on Zulip Cyril Cohen (Jul 06 2020 at 09:01):

Cyril Cohen said:

OK I have a suggestion rather than a question: in the same way Blist would be easier defined as a sub type, {s | size s <= n}, the current tree implementation could be generalized to have an arbitrary datatype for nodes and have Btree be {t | width t w} where w : A -> nat gives the arity of each node.

@Pierre-Léo Bégay did you see my suggestion?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 09:01):

Not a question, but a comment, but I guess the way I'd go proving finitiness of the tree is to have the bound be itself a tree of the corresponding ordinals

view this post on Zulip Reynald Affeldt (Jul 06 2020 at 09:02):

we also needed a type such as {s | size s <= n} to represent codewords (so my point is that such datatypes are useful for error-correcting code in particular)

view this post on Zulip Cyril Cohen (Jul 06 2020 at 09:05):

I think @affeldt-aist using a dependent type in the signature could be done using a finfun nowadays.

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:07):

Cyril Cohen said:

OK I have a suggestion rather than a question: in the same way Blist would be easier defined as a sub type, {s | size s <= n}, the current tree implementation could be generalized to have an arbitrary datatype for nodes and have Btree be {t | width t w} where w : A -> nat gives the arity of each node.

1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.

2) That's obviously a better way to defined Btrees. However, as "quick'n dirty" as it sounds, we really just needed a clearly finite tree type to use as a support to the more interesting type Utree.

view this post on Zulip Cyril Cohen (Jul 06 2020 at 09:08):

Can you share a pointer to your source code. I already forgot the definition of Utree

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:08):

affeldt-aist said:

(bounded trees were important to be able to take about finite sets of trees)

Yes, for us also! (the semantics of Datalog is defined as a set of facts, so we wanted to defined the trace semantics as a set of traces)

view this post on Zulip Reynald Affeldt (Jul 06 2020 at 09:11):

To be more precise, our application is a theorem about some class of error-correcting codes (see Sect. VI of https://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf)

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:11):

Emilio Jesús Gallego Arias said:

Not a question, but a comment, but I guess the way I'd go proving finitiness of the tree is to have the bound be itself a tree of the corresponding ordinals

I'm not sure I get what you mean, you mean a tree of 'I_n where n is the maximal degree? How is that finite?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):

The bound can be a choiceType tree itself

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):

then the bound implies finiteness by induction

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):

I think

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 09:12):

just an idea

view this post on Zulip Christian Doczkal (Jul 06 2020 at 09:13):

Pierre-Léo Bégay said:

1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.

I ran into this a while ago, one can use pickle/unpickle to encode the type at hand into the fixed node type.

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:13):

Cyril Cohen said:

Can you share a pointer to your source code. I already forgot the definition of Utree

It's not online yet (and there are legal issues (thèse CIFRE)), but I can send you the sources.

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:16):

Christian Doczkal said:

Pierre-Léo Bégay said:

1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.

I ran into this a while ago, one can use pickle/unpickle to encode the type at hand into the fixed node type.

Yup, I realized that when writing my message, I was unfortunately unaware of this at the time. But it feels weird to have to rely on this rather than just be able to simply use any choiceType. Even considering this option, I'm not sure if putting nat as the node type of tree was a design decision.

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:18):

affeldt-aist said:

To be more precise, our application is a theorem about some class of error-correcting codes (see Sect. VI of https://staff.aist.go.jp/reynald.affeldt/documents/rs_isita2016_author_version.pdf)

It somehow feels great too hear that we were not the only ones missing such a structure, and that it was used for something so different from what we have done, thanks for the pointer, I'll look into that more closely later!

view this post on Zulip Cyril Cohen (Jul 06 2020 at 09:26):

Pierre-Léo Bégay said:

Christian Doczkal said:

Pierre-Léo Bégay said:

1) I would actually have loved for the datatypes of nodes of tree (in choice.v) to be generalized so that we could use it rather than making our own general tree type. I guess I should have asked you guys about it.

I ran into this a while ago, one can use pickle/unpickle to encode the type at hand into the fixed node type.

Yup, I realized that when writing my message, I was unfortunately unaware of this at the time. But it feels weird to have to rely on this rather than just be able to simply use any choiceType. Even considering this option, I'm not sure if putting nat as the node type of tree was a design decision.

The initial (and only current real use) of tree is to encode other datatypes to show eqType, countType, choiceType, etc

view this post on Zulip Christian Doczkal (Jul 06 2020 at 09:27):

Yes, I just checked my own (old) code and indeed I only use the "nat" part for enumerating constructors. But my syntax does not carry data on internal nodes, some other syntaxes may.

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:29):

@Cyril Cohen , I just sent you the code via email.

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:30):

Cyril Cohen said:

The initial (and only current real use) of tree is to encode other datatypes to show eqType, countType, choiceType, etc

Ok, that makes more sense in that case, thanks.

view this post on Zulip Cyril Cohen (Jul 06 2020 at 09:33):

Pierre-Léo Bégay said:

Cyril Cohen , I just sent you the code via email.

OK, I will take a look later

view this post on Zulip Pierre-Léo Bégay (Jul 06 2020 at 09:33):

Emilio Jesús Gallego Arias said:

just an idea

Ok, I think I see what you mean, it looks more intricate than what I would come up with myself, thanks for the feedback!


Last updated: Feb 06 2023 at 05:03 UTC