Stream: math-comp users

Topic: computing variant of `ord_enum`


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2020 at 16:49):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Christian Doczkal (Oct 13 2020 at 08:49):

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

view this post on Zulip 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