Stream: Coq users

Topic: ✔ Weakness in FMaps

Yves Bertot (Sep 06 2022 at 12:14):

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?

Yves Bertot (Sep 06 2022 at 12:15):

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.

Pierre-Marie Pédrot (Sep 06 2022 at 12:30):

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.

Li-yao (Sep 06 2022 at 12:32):

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

Pierre-Marie Pédrot (Sep 06 2022 at 12:40):

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.

Yves Bertot (Sep 06 2022 at 12:42):

Oh, thanks!

Notification Bot (Sep 06 2022 at 12:42):

Yves Bertot has marked this topic as resolved.

Last updated: Apr 19 2024 at 22:01 UTC