Are there builtin dictionary/map types in Lean 4 prover?
I'd like to use dictionaries in my program and prove properties about it, but I am not sure if there is a dictionary type in Lean 4. A similar question in SO was about whether there is a dictionary type in Idris 2. The answer was there there is no builtin type and one is provided in the
contrib called Data.SortedMap. As the linked question pointed out, dictionary is a basic data structure (so commonly used that languages like lua depend on it.)
Upon closer look, there is not much support for proofs in Idris's
Data.SortedMap. For example, the only
lookup function returns a Maybe value. There seems to be no way to provide a proof that the lookup key is
inBounds and get a value of the original type. The constructor type
M : SortedDMap k (const v) -> SortedMap k v is also a bit mysterious to a newcomer like me. Hence the question here.
A more general question is,
is it generally more difficult to construct a dictionary type in proof languages via algebraic data types and constructors like
List's and their
cons? (and what are the difficulties?)