`gen_tree` should use `positive` instead of `nat`

I have a rose-tree-like datatype that I am generating a Countable instance for by giving an injection into gen_tree:

Inductive vty : Set :=
  | vty_int : vty
  | vty_real : vty
  | vty_var: typevar -> vty
  | vty_cons: typesym -> list vty -> vty.

And I wrote the following injection:

Definition vty_nonind := ((unit + unit)%type + typevar)%type.
Fixpoint vty_to_gen_tree (v: vty) : countable.gen_tree vty_nonind :=
  match v with
  | vty_int => countable.GenLeaf (inl (inl tt))
  | vty_real => countable.GenLeaf (inl (inr tt))
  | vty_var v => countable.GenLeaf (inr v)
  | vty_cons ts tys => countable.GenNode (Pos.to_nat (countable.encode ts)) (map vty_to_gen_tree tys)
  end.

It is straightforward to prove that this is an injection.

The problem is that I cannot compute with this; since the encoding of typesym often happens to produce a positive whose nat representation causes a stack overflow in Coq. Is there a reason that gen_tree takes a nat argument rather than positive, as it seems better for computation to avoid natural numbers entirely? Or is there a better way to inject into gen_tree?

I wouldn't object to using a positive instead of a nat if someone makes a merge request for it.

However, I think you are not using gen_tree in the way intended. The nat is meant to represent the constructor. See https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_heap_lang/lang.v#L319 for an example.

Yeah, that nat should always be small. The recommended way to encode vty_cons would be to also turn ts into a GenLeaf, and then add it to the list of children of the node you are building.

mentioned in merge request !587 (merged)

Thank you, that is helpful and I have changed my definition to be consistent with the example.

Separately, why does std++ block reduction on concrete gmaps, and is there any way to disable this? I would like to be able to simplify gmaps/gsets in proofs without using vm_compute; is there a way to do this? (Also, is there a std++ Zulip channel or better place to ask these questions? Thanks)

Separately, why does std++ block reduction on concrete gmaps

Because simpl never is broken...

https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/stdpp/gmap.v?ref_type=heads#L152

Also, is there a std++ Zulip channel or better place to ask these questions?

https://mattermost.mpi-sws.org/iris/channels/stdpp

Fixed by !587 (merged). Thanks for bringing this up!

closed