Map structure where the values are strictly positive

Stream: Is there code for X?

[Mai]

Is there a Map/Dictionary structure where the values are in strictly positive positions, such that you could use it inductively, like so?

inductive Foo
  | mk : Map Key Foo -> Foo

[Arthur Adjedj]

Not that I'm aware of, although you could reimplement Rocq's gmap, which can be used in nested types.

[Mai]

Hmm, might take a shot at that

[Mai]

Is there a reason the standard HashMap/TreeMap can't be used this way?

[Mai]

I guess it's because the underlying structures are Dependent

[Robin Arnez]

The Raw versions (i.e. docs#Std.HashMap.Raw, docs#Std.TreeMap.Raw, etc.) work here but their wellformedness is unbundled in e.g. docs#Std.HashMap.Raw.WF

[Mai]

What's the implication of the wellformedness being unbundled?

[Robin Arnez]

Well it's a little more inconvenient for proofs since you need to get the wellformedness from somewhere else

[Robin Arnez]

And you'll most likely want a wellformedness predicate for Foo to get those recursively

[Violeta Hernández]

You could make your inductive type take both an unbundled map and a proof of well-foundedness, and then make the public accessor return the bundled version.

[Mai]

@Violeta Hernández no? because WF will indirectly depend on the type being defined

[Markus Himmel]

The reference manual has a worked example of using docs#Std.HashMap.Raw in a nested inductive: https://lean-lang.org/doc/reference/latest/Basic-Types/Maps-and-Sets/#raw-data