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

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.

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

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`

.

@Cyril Cohen , this should be moved to `math-comp users`

. Thanks in advance.

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

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 here from #Coq users > Finite Types & Finite Graphs in MathComp by Karl Palmskog.

Last updated: Jul 25 2024 at 15:02 UTC