Preimage/inverse image of finite maps

It would be nice to have some theory for taking inverse images of finite maps. For example, if I have a map m : gmap nat string, then I want to obtain an inverse m^-1 : gmap string (gset nat) such that

m^-1 !! s = Some X ↔ (∀ x, x ∈ X ↔ m !! x = Some s) 

Here is my initial attempt at defining a preimage function, but I think it might have the property above only for injective mappings:

Section gmap_preimage.
  Context `{FinMap K M}.
  Context `{!EqDecision K, !Countable K, !EqDecision A, !Countable A}.
  Context `{FinMap A M'}.

  Local Definition prei : K * A → M' (gset K) → M' (gset K) :=
    λ '(k, a) m', <[a := {[k]} ∪ (m' !!! a)]>m'.

  Definition preimage (m : M A) : M' (gset K).
  Proof.
    pose (ls := map_to_set pair m : gset (K * A)).
    refine (set_fold prei ∅ ls).
  Defined.

End gmap_preimage.

This would indeed be cool! I've written a preimage function for functions from finite types in https://gist.github.com/Blaisorblade/e57f263840cd8ff2263a4a493b17e2b5, and it has the property in general. Without Finite A you can probably iterate over the codomain of m instead of enum A to get the same properties. Most relevant section:

Section finite_preimage.
  Context `{Finite A} `{EqDecision B}.
  Implicit Types (a : A) (b : B) (f : A → B).

  Definition finite_preimage f b : list A := filter (λ a, f a = b) (enum A).

  Lemma elem_of_finite_preimage f a b :
    a ∈ finite_preimage f b ↔ f a = b.
  Proof. apply: elem_of_filter_enum. Qed.

  (** Teach [set_solver] to use [elem_of_finite_preimage]! *)
  #[global] Instance set_unfold_finite_preimage f a b P :
    SetUnfold (f a = b) P →
    SetUnfoldElemOf a (finite_preimage f b) P.
  Proof. split. rewrite elem_of_finite_preimage. set_solver. Qed.

  Lemma finite_preimage_inj_singleton `{!Inj eq eq f} a :
    finite_preimage f (f a) = [a].
  Proof.
    apply list_singleton_eq_ext. { apply NoDup_filter, NoDup_enum. }
    set_solver.
  Qed.

  Definition finite_inverse f b : option A := head $ finite_preimage f b.

  Lemma finite_inverse_Some_inv f a b :
    finite_inverse f b = Some a → f a = b.
  Proof. intros Hof%head_Some_elem_of. set_solver. Qed.

  Lemma finite_inverse_is_Some f a b :
    f a = b → is_Some (finite_inverse f b).
  Proof.
    intros Heq%elem_of_finite_preimage%elem_of_not_nil.
    exact /head_is_Some.
  Qed.

  Lemma finite_inverse_None_equiv f b :
    finite_inverse f b = None ↔ ¬(∃ a, f a = b).
  Proof.
    rewrite eq_None_not_Some. f_equiv.
    split. { intros [a ?%finite_inverse_Some_inv]. by exists a. }
    by intros [a ?%finite_inverse_is_Some].
  Qed.

  #[global] Instance set_unfold_finite_inverse_None f b P :
    (∀ a, SetUnfold (f a = b) (P a)) →
    SetUnfold (finite_inverse f b = None) (¬ (∃ a, P a)).
  Proof. constructor. rewrite finite_inverse_None_equiv. set_solver. Qed.

  Section finite_preimage_inj.
    Context `{Hinj : !Inj eq eq f}.
    #[local] Set Default Proof Using "Type*".

    Lemma finite_inverse_inj_cancel a :
      finite_inverse f (f a) = Some a.
    Proof. by rewrite /finite_inverse finite_preimage_inj_singleton. Qed.

    Lemma finite_inverse_inj_Some_equiv a b :
      finite_inverse f b = Some a ↔ f a = b.
    Proof.
      naive_solver eauto using finite_inverse_Some_inv, finite_inverse_inj_cancel.
    Qed.

    #[global] Instance set_unfold_finite_inverse_inj_Some a b P :
      SetUnfold (f a = b) P →
      SetUnfold (finite_inverse f b = Some a) P.
    Proof. constructor. rewrite finite_inverse_inj_Some_equiv. set_solver. Qed.
  End finite_preimage_inj.
End finite_preimage.

The gist has more code, and https://github.com/bedrocksystems/BRiCk is the underlying source but it's probably outdated. Note the above is not BSD-licensed for reasons, but we always relax the license when we upstream things.

I forgot to post the functions for the set -> set preimage:

  Definition set_concat_map (f : A → list B) (xs : C) : D :=
    list_to_set (elements xs ≫= f).
  Definition finite_preimage_set (f : A → B) (bs : D) : C :=
    set_concat_map (finite_preimage f) bs.

I wrote it this way, avoiding set_fold/map_fold, because IME proofs about bind are nice and proofs about fold are very annoying. Proofs on set_concat_map proceed by set_solver with a few extra instances :-)

• https://github.com/bedrocksystems/BRiCk/blob/8880586cecb52c759000841425724230230b4193/theories/prelude/finite.v is now up-to-date.

• A possible common abstraction: you can invert a (partial) mapping f from A to B, with the constructions I use above, if the domain of f is finite:

Class FiniteDomain {A B M} `{Lookup A B (M B)} (m : M B) := {
  enum_domain : list A;
  finite_mapping (a : A) (b : B) :
    m !! a = Some b -> a ∈ enum_domain;
}.
Arguments enum_domain {A B M _} m {_} : assert.
Section fin_domain.
  Context `{EqDecision B}.
  Context {A M} (m : M B) `{FiniteDomain A B M m}.
  Definition preimage (b : B) : list A :=
    filter (λ a, m !! a = Some b) (enum_domain m).

  Context `{FinSet A C} `{FinSet B D}.

  Definition preimage_set (bs : D) : C :=
    set_concat_map preimage bs.
End fin_domain.

Section finite_preimage.
  Context `{Finite A} {B : Type} (f : A -> B).
  #[local] Set Default Proof Using "Type*".

  Require Import stdpp.functions.
  (* Instance fn_lookup_total : LookupTotal A B (A -> B) := λ a f, f a. *)
  Instance fn_lookup : Lookup A B (A -> B) := λ a f, Some (f a).
  #[refine] Instance finite_finitedomain : FiniteDomain (M := λ B, A -> B) f :=
  { enum_domain := enum _ }.
  Proof. set_solver. Qed.
End finite_preimage.

Section map_preimage.
  Context {K A : Type} `{FinMap K M} (m : M A).
  #[local] Set Default Proof Using "Type*".
  #[refine] Instance gmap_finitedomain : FiniteDomain m :=
  { enum_domain := fst <$> map_to_list m }.
  (* XXX fix set_solver. *)
  Proof. move=> k a /elem_of_map_to_list. apply: elem_of_list_fmap_1. Qed.
End map_preimage.

I cannot say that I fully understand the code, but I will try to play around with it. Thanks!

I guess set_concat_map is another function you have from your standard library?

FWIW it is very easy to prove the lemma I wanted with your definition of preimage:

Section fin_domain.
  Context `{EqDecision B}.
  Context {A M} (m : M B) `{FiniteDomain A B M m}.
  Definition preimage (b : B) : list A :=
    filter (λ a, m !! a = Some b) (enum_domain m).

  Lemma preimage_eq_1 a b :
    b ∈ preimage a → m !! b = Some a.
  Proof. rewrite /preimage elem_of_list_filter. naive_solver. Qed.

  Lemma preimage_eq_2 a b :
    m !! b = Some a → b ∈ preimage a.
  Proof.
    rewrite /preimage elem_of_list_filter. intros ?; split; auto.
    by eapply finite_mapping.
  Qed.

  Lemma preimage_eq a b :
    b ∈ preimage a ↔ m !! b = Some a.
  Proof. split; [ apply preimage_eq_1 | apply preimage_eq_2 ]. Qed.
End fin_domain.

Those proofs are good, and a bit more work can probably reduce them all to set_solver; for that, I should probably fix finite_mapping — right now it allows enum_domain to contain too many elements. FinMapDom gets that right, but it bundles a lot more things.

About set_concat_map: its body appears above — https://github.com/bedrocksystems/BRiCk/blob/8880586cecb52c759000841425724230230b4193/theories/prelude/fin_sets.v#L164 has the full definition.

@dfrumin regarding "ease of proof" — did you also run into trouble with folds? That's my experience and the lemmas look harder, but I'm curious if others have different experiences.

Sorry, I am not sure I understand -- what folds are you talking about? If you mean the use of set_fold in my original proposal, then yeah it was painful to work with.

By the way, since I actually wanted to compute with preimages, I found it useful to make all the main FiniteDomain instances transparent

Yeah, my current draft now has:

Class FinDom K A KA KS `{Lookup K A KA} `{Dom KA KS} `{ElemOf K KS} := {
  elem_of_dom_nomap (k : K) (m : KA) :
    k ∈ dom KS m ↔ is_Some (m !! k);
}.

and if you only care about gmaps you can just use FinMapDom. I'll try to post my version, but it's less clear how to best include functions.

mentioned in merge request !382 (merged)

!382 (merged) added a preimage function to std++. (Someone should have mentioned this here before merging. Sorry for that.)

However, it seems there are concerns that the API could be improved:

@Blaisorblade

This interface seems to complicate any code sharing with function inverses, compared to the version in #140. The proofs also look more complex due to the use of folds, but maybe there’s a reason for it? The remaining question there is that FinMapDom cannot be “just” instantiated for functions currently, so one would need to add more instances to use functions as maps, or to generalize FinMapDom to domains of non-maps.

@robbertkrebbers

The main reason why the code of this MR is a bit more complex is that our preimage is actually a finite map, not just an ordinary function. Finite maps are quite a bit harder to construct but are "nicer" since they have a better equality and can more easily be used as ghost state in Iris.

(I personally have no skin in this game, I just hope y'all can reach consensus. :) I would be fine with reverting the MR for now to avoid having a "default" solution that some people are unhappy with.)

The main reason why the code of this MR is a bit more complex is that our preimage is actually a finite map, not just an ordinary function. Finite maps are quite a bit harder to construct but are "nicer" since they have a better equality and can more easily be used as ghost state in Iris.

I think I didn't explain properly which code I'm discussing, and maybe I should send an MR — above I have a definition that works for maps just fine — let me highlight the core:

Definition preimage (m : M B) (b : B) : list A :=
  filter (λ a, m !! a = Some b) (dom m).

That is, the preimage of b in map m is computed by taking the domain of m, and filter the elements that map to b. Since the theory of filter is much better than the theory of map_fold (and folds in general), proofs become much easier assuming FinMapDom. However, does map_fold have better constant factors than filter somehow?

Your code is producing an ordinary function B -> list A, not a finite map M (list A) where M could be gmap B.

Good point... avoiding folds might be possible but is not as easy, and the advantage is less clear.

And my overall goal is to reuse this preimage to invert functions on finite domains — bedrock.prelude supports that but with a different setup.

One option is to actually prove Finite A -> FinMap A (fun B => A -> B), or at least a large part of it (basically, dom (f : A -> B) := enum A). But would Coq infer such instances robustly? (I am tempted to wrap functions in a newtype). With my alternative definitions, fewer "map" instances for finite functions were required, and everything worked fine.