Add uninterpreted Map implementation to Prelude.lean

[JuanCoRo]

Tackling #4725, this PR adds an uninterpreted implementation for the Map sort.

This PR's goal is to iron out how we want these uninterpreted implementations to be before proceeding with the rest of the hooked functions in domains.md.

[JuanCoRo]

We can write things like

open MapHookDef
noncomputable def map := mapImpl SortInt SortInt
noncomputable def exmpl : map.map := map.cons 3 4 map.unit

[tothtamas28]

In general, I'm fine with any implementation that models the functions over these data types faithfully.

In addition, it should be checked how implementation can be combined with the sort module:

• Order sort declarations topologically #4735

I.e. what additional changes need to be made to the program to make it compile if

inductive SortMap : Type where
  | mk (coll : List (SortKItem × SortKItem)) : SortMap

is replaced by

inductive SortMap : Type where
  | mk (coll : (mapImpl SortKItem SortKItem).map) : SortMap

(assuming that's the intended use).

[tothtamas28]

Would this work as well?

Suggested change

	noncomputable def mapImpl (K V : Type) : MapHookSig K V :=
	axiom mapImpl : MapHookSig

[JuanCoRo]

I don't think so since axiom mapImpl : MapHookSig K V doesn't provide concrete elements for mapImpl. So we cannot access it's components like mapImpl.map:

axiom mapImpl : MapHookSig K V
#check mapImpl.map

returns

unknown constant 'MapHookDef.mapImpl.map'

[JuanCoRo]

Re: this comment

Do we want SortMap as an inductive wrapping over the implementation? I thought we would use instead something along these lines:

noncomputable abbrev SortMap := mapImpl KItem KItem

defining SortMap right after KItem or as soon as possible

[tothtamas28]

I thought we would use instead something along these lines:

noncomputable abbrev SortMap := mapImpl KItem KItem

That would be ideal, but I couldn't make the sort module compile that way, so I went with the most straightforward approach for now.

[JuanCoRo]

Ah yes! It seems Lean does not allow (definitions/abbrevs/theorems) and inductives in the same mutual block, just found out!