Hello, I wanted to write an introductory example about finite maps, in which I found it more convenient to describe total functions: one can view a finite map as a total function if one provides a default value for all keys where the map does not contain a binding. Unfortunately, there is no theorem that states that F.find ... = None <-> ~MapsTo ...

Any opinion on why this is like that? Is there a a good reason to make the interface that weak?

Just as added information, I just prove the following lemma:

```
key1 <> key2 ->
F.find key2 m = None -> F.find key2 (F.add key1 v m) = None
```

But I had to go through a full proof by induction on trees to do it.

I haven't used the FMap API in a long time, but I'm pretty sure you can prove this with the available theorems already, without having to resort to low-level reasoning on trees.

Seems to be the contrapositive of `add_3 : ~ E.eq x y -> MapsTo y e (add x e' m) -> MapsTo y e m`

.

as a matter of fact:

```
Require Import FMapInterface.
Declare Module E : DecidableType.
Declare Module F : WSfun(E).
Lemma find_None_1 : forall elt k (v : elt) m,
F.find k m = None -> F.MapsTo k v m -> False.
Proof.
intros elt k v m He H.
apply F.find_1 in H; congruence.
Qed.
Lemma find_None_2 : forall elt k m,
(forall (v : elt), F.MapsTo k v m -> False) -> F.find k m = None.
Proof.
intros elt k m H.
remember (F.find k m) as v.
destruct v as [v|]; [exfalso|reflexivity].
symmetry in Heqv; apply F.find_2 in Heqv; eauto.
Qed.
Goal forall elt k1 k2 m (v : elt), ~ E.eq k1 k2 -> F.find k2 m = None -> F.find k2 (F.add k1 v m) = None.
Proof.
intros elt k1 k2 m v Hk H.
apply find_None_2; intros w Hm.
apply F.add_3 in Hm; [|assumption].
eapply find_None_1; eassumption.
Qed.
```

Oh, thanks!

Yves Bertot has marked this topic as resolved.

Last updated: Jan 29 2023 at 06:02 UTC