Hi, I want to fold over a Map but haven't found fold* in the Map Theory, or did I miss something? :)

A Map is at its core just a function and thus not really a structure you can directly fold over. But you should be able to use Finite_Set.fold to do it, provided you can proof that the domain of the map is actually finite:

```
definition map_fold :: "('b ⇒ 'c ⇒ 'a ⇒ 'a) ⇒ 'a ⇒ ('b ⇒ 'c option) ⇒ 'a"
where "map_fold f z m ≡ Finite_Set.fold (λk acc. f k (the (m k)) acc) z (dom m)"
```

Remark that you have to prove that the order of the fold does not matter.

It doesn't matter if the keys are linearly ordered since the dom function is (piecewise) injective.

In most cases it is probably easiest to just express whatever you want to do in a less "operational" way without a fold. Once you move to actually implementing these maps with a more concrete datastructure, you can then prove that a fold works out.

I actually proved all of this already but you will have to wait until the next release.

I don't understand. How can the order of the fold not matter in general? Surely it depends on what the fold operation actually does.

Ah, the fold as the defined here doesn't work. But you can use `List.fold`

over `List.sorted_list_of_set`

of `dom m`

.

In any case, my point was that "fold" is a very operational way to think about things, and `'a ⇒ 'b option`

is a very abstract view of maps, so the two don't go together easily.

In all likelihood, the "fold" aspect should really only come in when you're trying to get this whole thing executable with a more concrete representation of maps.

Both RBTs and AList can implement this fold

Lukas Stevens said:

Ah, the fold as the defined here doesn't work. But you can use

`List.fold`

over`List.sorted_list_of_set`

of`dom m`

.

That can work, but only if you have an ordering on your elements and that is indeed the order that you want to fold over.

In the end, it probably depends on the exact application.

With RBTs in mind, that would be the natural order. In general, it is not so clear.

In any case, it is generally good advice to try not to mix operational aspects into the abstract reasoning. Whether or not that applies here is difficult to say without knowing the exact use case.

One should probably only add this operation to `mapping`

and not to `map`

.

In fact, that is exactly what I did in my changes.

Indeed, `Mapping`

is intended to be something of a first step of refining "mathematical maps" (i.e. partial functions) to actual implementations

Thank you for the amount of comments. Still, I'm not able to follow most comments. See below for a minimal example of my current issue. Basically, I have a finite map containing id's and their corresponding object. The folding function should accumulate some state.

```
fun test1 :: "(nat, bool) fmap ⇒ bool" where
"test1 m = (let t = fmdom m in ffold (λv a. the (fmlookup m v) ∧ a) True t)"
value "test1 (fmupd 1 False fmempty)"
```

I guess, the error reports, `nat`

is not finite.

```
Wellsortedness error
(in code equation test1 ?m ≡ Let (fmdom ?m) (ffold (λv. (∧) (the (fmlookup ?m v))) True),
with dependency "Pure.dummy_pattern" -> "test1"):
Type nat not of sort finite
No type arity nat :: finite
```

I expect

```
ffold (λv a. v ∧ a) True (fmran mymap)
```

to be easier to manipulate than your `ffold+fmlookup`

definition, but it is not executable either.

Here is a way to make it work, by providing a characterization directly over the fset, but that might not be applicable to your real example:

```
definition myfold where
‹myfold = ffold (λv a. v ∧ a)›
lemma [code]:
‹myfold b A ⟷ b ∧ False |∉| A›
proof -
interpret comp_fun_commute ‹(λv a. v ∧ a)›
by standard auto
show ?thesis
unfolding myfold_def
by (induction A) auto
qed
value "myfold True ((fmran (fmupd (1::nat) False fmempty))) "
```

Following up on this, even the more simplified version fails to be executed. See:

```
definition bla1 :: "nat fset ⇒ bool" where
"bla1 n = (ffold (λeid a. True ∧ a) True n)"
value "bla1 {|1,2,3|}"
```

with

```
Wellsortedness error
(in code equation bla1 ?n ≡ ffold (λeid. (∧) True) True ?n,
with dependency "Pure.dummy_pattern" -> "bla1"):
Type nat not of sort finite
No type arity nat :: finite
```

From the error message, I assume it is expected that `nat`

is finite?

Last updated: Jun 20 2024 at 12:31 UTC