Stream: Coq users

Topic: Finite Types & Finite Graphs in MathComp


view this post on Zulip Notification Bot (Nov 13 2020 at 12:08):

This topic was moved by Théo Zimmermann to #math-comp users > Finite Types & Finite Graphs in MathComp

view this post on Zulip Jinoh Kang (Jun 06 2023 at 08:19):

Is there a "best practice" way of induction over tuples, other than defining my own induction principle? Should I just take the seq/list out of it and start from O for (size t)?

view this post on Zulip Jinoh Kang (Jun 06 2023 at 08:21):

(Side note: I admit that it took me a bit to realize that seq ?T is finite, since it's an inductive type, not a coinductive type à la streams)

view this post on Zulip Jinoh Kang (Jun 06 2023 at 08:24):

It appears to me that naïvely destructing the tval leads to impossible goals since e.g., it asserts that [::] is an n.+1-tuple

view this post on Zulip Paolo Giarrusso (Jun 06 2023 at 09:51):

From skimming the library as an outsider, induction on the length n + tuple0 and tupleP seem a candidate

view this post on Zulip Notification Bot (Jun 06 2023 at 11:43):

4 messages were moved from this topic to #math-comp users > Finite Types & Finite Graphs in MathComp by Karl Palmskog.


Last updated: Mar 29 2024 at 10:01 UTC