I'm trying to compute a few simple properties on concrete objects (graphs) that are defined using finite ordinals and a concrete relation (i.e., one that reduces to `true`

or `false`

for any two ordinals of the shape `Ordinal k _`

. Unfortunately, the algorithm needs an enumeration of all the vertices of the graph, that is an enumeration of `'I_n`

that is a concrete list where every element is of the shape `Ordinal k _`

. Unfortunately,

```
ord_enum = fun n : nat => pmap insub (iota 0 n)
```

relies on `insub`

and therefore evaluation gets stuck on `idP`

.

answering my own question, it looks like replacing the generic insub with

```
Definition oinord (m : nat) : option 'I_k :=
(match m < k as b return m < k = b -> option 'I_k with
| true => fun p => Some (Ordinal p)
| false => fun _ => None
end) erefl.
```

should do the trick. Sorry for the noise.

@Christian Doczkal you also have `insub_eq`

, maybe that works for you?

```
Definition ord_enum_eq n : seq 'I_n := pmap (insub_eq _) (iota 0 n).
Lemma ex : map val (ord_enum_eq 3) = [:: 0; 1; 2].
Proof. by []. Qed.
```

Emilio Jesús Gallego Arias said:

Christian Doczkal you also have

`insub_eq`

, maybe that works for you?

Indeed, I was not aware of `insub_eq`

and the only lemma mentioning it (`insub_eqE`

) merely states the equivalence with `insub`

. I guess this could be seen as a hint that the relevant properties of `insub_eq`

are reduction properties that are not expressible inside the theory. On the other hand, the pattern I used is standard and completely generic, so it should not come as a surprise that it's to be found in mathcomp. Thanks!

So asking here wasn't for naught after all. :+1:

I recall seeing some more information about `insub_eq`

, likely from @Assia Mahboubi , but I'm afraid a long time has passed and I remember zero. Maybe indeed it was some discussion about if `insubd_eq`

behavior should become the default

Last updated: Jul 15 2024 at 20:02 UTC