Stream: math-comp users

Topic: Finite Types & Finite Graphs in MathComp

Quim (Nov 13 2020 at 11:02):

I am a newbie in Coq trying to get familiarized with the MathComp lib.

I am trying to prove the following:

Definition K n := fun x y : ordinal n => y \in (rem x (ord_enum n)).
Lemma CompleteGraph n : forall x y : ordinal n, x <> y -> K x y.

The problem I am facing is that I don't know how to reason about (rem x (ord_enum n)). How can I recover the list of nats less than n that are not equal to x? (i.e the enumeration of ordinal n with one particular member removed).

Guillaume Melquiond (Nov 13 2020 at 11:25):

You are trying to prove a property relating \in and rem. If you type Search _ "\in" rem, Coq will list a few lemmas, including mem_rem_uniq, which is what you want.

Christian Doczkal (Nov 13 2020 at 11:39):

You may want to have a look at our graph-theory library, which is based on mathcomp and formalizes complete graphs as part of the library on simple graphs (digraphs with a symmetric and irreflexive edge relation).

Christian Doczkal (Nov 13 2020 at 11:41):

In particular, I would write the "full" irreflexive and symmetric relation on 'I_n (which is the usual syntax for ordinal n) as [rel x y : 'I_n | x != y]. There is no need to talk about the enumeration or rem.

Christian Doczkal (Nov 13 2020 at 11:53):

@Cyril Cohen , this should be moved to math-comp users. Thanks in advance.

Notification Bot (Nov 13 2020 at 12:08):

This topic was moved here from #Coq users > Finite Types & Finite Graphs in MathComp by Théo Zimmermann

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

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)

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

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

Notification Bot (Jun 06 2023 at 11:43):

4 messages were moved here from #Coq users > Finite Types & Finite Graphs in MathComp by Karl Palmskog.

Last updated: Apr 16 2024 at 08:02 UTC