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.
Yves Bertot has marked this topic as resolved.
Last updated: Jan 29 2023 at 06:02 UTC