## Stream: math-comp users

### Topic: computing variant of `ord_enum`

#### Christian Doczkal (Oct 12 2020 at 12:14):

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

#### Christian Doczkal (Oct 12 2020 at 12:35):

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.

#### Emilio Jesús Gallego Arias (Oct 12 2020 at 16:49):

@Christian Doczkal you also have `insub_eq`, maybe that works for you?

#### Emilio Jesús Gallego Arias (Oct 12 2020 at 16:49):

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

#### Christian Doczkal (Oct 13 2020 at 08:49):

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!

#### Christian Doczkal (Oct 13 2020 at 08:49):

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

#### Emilio Jesús Gallego Arias (Oct 13 2020 at 16:28):

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