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

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)?

(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)

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

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

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

Last updated: Oct 03 2023 at 04:02 UTC