Module collections

This file collects definitions and theorems on collections. Most importantly, it implements some tactics to automatically solve goals involving collections.
Require Export base tactics orders.

Theorems

Section simple_collection.
  Context `{SimpleCollection A C}.

  Lemma elem_of_empty x : x ∈ ∅ ↔ False.
  Proof. split. apply not_elem_of_empty. done. Qed.
  Lemma elem_of_union_l x X Y : xXxXY.
  Proof. intros. apply elem_of_union. auto. Qed.
  Lemma elem_of_union_r x X Y : xYxXY.
  Proof. intros. apply elem_of_union. auto. Qed.

  Global Instance collection_subseteq: SubsetEq C := λ X Y,
    ∀ x, xXxY.
  Global Instance: BoundedJoinSemiLattice C.
  Proof. firstorder auto. Qed.

  Lemma elem_of_subseteq X Y : XY ↔ ∀ x, xXxY.
  Proof. done. Qed.
  Lemma elem_of_equiv X Y : XY ↔ ∀ x, xXxY.
  Proof. firstorder. Qed.
  Lemma elem_of_equiv_alt X Y :
    XY ↔ (∀ x, xXxY) ∧ (∀ x, xYxX).
  Proof. firstorder. Qed.
  Lemma elem_of_subseteq_singleton x X : xX ↔ {[ x ]} ⊆ X.
  Proof.
    split.
    * intros ??. rewrite elem_of_singleton. intro. by subst.
    * intros Ex. by apply (Ex x), elem_of_singleton.
  Qed.

  Global Instance singleton_proper : Proper ((=) ==> (≡)) singleton.
  Proof. repeat intro. by subst. Qed.
  Global Instance elem_of_proper: Proper ((=) ==> (≡) ==> iff) (∈) | 5.
  Proof. intros ???. subst. firstorder. Qed.

  Lemma elem_of_union_list (Xs : list C) (x : A) :
    x ∈ ⋃ Xs ↔ ∃ X, XXsxX.
  Proof.
    split.
    * induction Xs; simpl; intros HXs.
      + by apply elem_of_empty in HXs.
      + setoid_rewrite elem_of_cons.
        apply elem_of_union in HXs. naive_solver.
    * intros [X []]. induction 1; simpl.
      + by apply elem_of_union_l.
      + intros. apply elem_of_union_r; auto.
  Qed.


  Lemma non_empty_singleton x : {[ x ]} ≢ ∅.
  Proof. intros [E _]. by apply (elem_of_empty x), E, elem_of_singleton. Qed.

  Lemma not_elem_of_singleton x y : x ∉ {[ y ]} ↔ xy.
  Proof. by rewrite elem_of_singleton. Qed.
  Lemma not_elem_of_union x X Y : xXYxXxY.
  Proof. rewrite elem_of_union. tauto. Qed.

  Context `{∀ X Y : C, Decision (XY)}.

  Global Instance elem_of_dec_slow (x : A) (X : C) : Decision (xX) | 100.
  Proof.
    refine (cast_if (decide_rel (⊆) {[ x ]} X));
      by rewrite elem_of_subseteq_singleton.
  Defined.

End simple_collection.

Ltac decompose_empty := repeat
  match goal with
  | H : __ ≡ ∅ |- _ => apply empty_union in H; destruct H
  | H : __ ≢ ∅ |- _ => apply non_empty_union in H; destruct H
  | H : {[ _ ]} ≡ ∅ |- _ => destruct (non_empty_singleton _ H)
  end.

Tactics

The first pass consists of eliminating all occurrences of (∪), (∩), (∖), map, , {[_]}, (≡), and (⊆), by rewriting these into logically equivalent propositions. For example we rewrite AxX ∪ ∅ into AxXFalse.
Ltac unfold_elem_of :=
  repeat_on_hyps (fun H =>
    repeat match type of H with
    | context [ __ ] => setoid_rewrite elem_of_subseteq in H
    | context [ __ ] => setoid_rewrite subset_spec in H
    | context [ __ ] => setoid_rewrite elem_of_equiv_alt in H
    | context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty in H
    | context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton in H
    | context [ ___ ] => setoid_rewrite elem_of_union in H
    | context [ ___ ] => setoid_rewrite elem_of_intersection in H
    | context [ ___ ] => setoid_rewrite elem_of_difference in H
    | context [ __ <$> _ ] => setoid_rewrite elem_of_fmap in H
    | context [ _mret _ ] => setoid_rewrite elem_of_ret in H
    | context [ __ ≫= _ ] => setoid_rewrite elem_of_bind in H
    | context [ _mjoin _ ] => setoid_rewrite elem_of_join in H
    end);
  repeat match goal with
  | |- context [ __ ] => setoid_rewrite elem_of_subseteq
  | |- context [ __ ] => setoid_rewrite subset_spec
  | |- context [ __ ] => setoid_rewrite elem_of_equiv_alt
  | |- context [ _ ∈ ∅ ] => setoid_rewrite elem_of_empty
  | |- context [ _ ∈ {[ _ ]} ] => setoid_rewrite elem_of_singleton
  | |- context [ ___ ] => setoid_rewrite elem_of_union
  | |- context [ ___ ] => setoid_rewrite elem_of_intersection
  | |- context [ ___ ] => setoid_rewrite elem_of_difference
  | |- context [ __ <$> _ ] => setoid_rewrite elem_of_fmap
  | |- context [ _mret _ ] => setoid_rewrite elem_of_ret
  | |- context [ __ ≫= _ ] => setoid_rewrite elem_of_bind
  | |- context [ _mjoin _ ] => setoid_rewrite elem_of_join
  end.

The tactic solve_elem_of tac composes the above tactic with intuition. For goals that do not involve , , map, or quantifiers this tactic is generally powerful enough. This tactic either fails or proves the goal.
Tactic Notation "solve_elem_of" tactic3(tac) :=
  simpl in *;
  unfold_elem_of;
  solve [intuition (simplify_equality; tac)].
Tactic Notation "solve_elem_of" := solve_elem_of auto.

For goals with quantifiers we could use the above tactic but with firstorder instead of intuition as finishing tactic. However, firstorder fails or loops on very small goals generated by solve_elem_of already. We use the naive_solver tactic as a substitute. This tactic either fails or proves the goal.
Tactic Notation "esolve_elem_of" tactic3(tac) :=
  simpl in *;
  unfold_elem_of;
  naive_solver tac.
Tactic Notation "esolve_elem_of" := esolve_elem_of eauto.

Given a hypothesis H : __, the tactic destruct_elem_of H will recursively split H for (∪), (∩), (∖), map, , {[_]}.
Tactic Notation "decompose_elem_of" hyp(H) :=
  let rec go H :=
  lazymatch type of H with
  | _ ∈ ∅ => apply elem_of_empty in H; destruct H
  | ?x ∈ {[ ?y ]} =>
    apply elem_of_singleton in H; try first [subst y | subst x]
  | ___ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_union in H;
    destruct H as [H1|H2]; [go H1 | go H2]
  | ___ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_intersection in H;
    destruct H as [H1 H2]; go H1; go H2
  | ___ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_difference in H;
    destruct H as [H1 H2]; go H1; go H2
  | ?x_ <$> _ =>
    let H1 := fresh in apply elem_of_fmap in H;
    destruct H as [? [? H1]]; try (subst x); go H1
  | __ ≫= _ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_bind in H;
    destruct H as [? [H1 H2]]; go H1; go H2
  | ?xmret ?y =>
    apply elem_of_ret in H; try first [subst y | subst x]
  | _mjoin _ ≫= _ =>
    let H1 := fresh in let H2 := fresh in apply elem_of_join in H;
    destruct H as [? [H1 H2]]; go H1; go H2
  | _ => idtac
  end in go H.
Tactic Notation "decompose_elem_of" :=
  repeat_on_hyps (fun H => decompose_elem_of H).

Section collection.
  Context `{Collection A C}.

  Global Instance: LowerBoundedLattice C.
  Proof. split. apply _. firstorder auto. Qed.

  Lemma intersection_singletons x : {[x]} ∩ {[x]} ≡ {[x]}.
  Proof. esolve_elem_of. Qed.
  Lemma difference_twice X Y : (XY) ∖ YXY.
  Proof. esolve_elem_of. Qed.

  Lemma empty_difference X Y : XYXY ≡ ∅.
  Proof. esolve_elem_of. Qed.
  Lemma difference_diag X : XX ≡ ∅.
  Proof. esolve_elem_of. Qed.
  Lemma difference_union_distr_l X Y Z : (XY) ∖ ZXZYZ.
  Proof. esolve_elem_of. Qed.
  Lemma difference_intersection_distr_l X Y Z : (XY) ∖ ZXZYZ.
  Proof. esolve_elem_of. Qed.

  Lemma elem_of_intersection_with_list (f : AAoption A) Xs Y x :
    xintersection_with_list f Y Xs ↔ ∃ xs y,
      Forall2 (∈) xs XsyYfoldrx, (≫= f x)) (Some y) xs = Some x.
  Proof.
    split.
    * revert x. induction Xs; simpl; intros x HXs.
      + eexists [], x. intuition.
      + rewrite elem_of_intersection_with in HXs.
        destruct HXs as (x1 & x2 & Hx1 & Hx2 & ?).
        destruct (IHXs x2) as (xs & y & hy & ? & ?); trivial.
        eexists (x1 :: xs), y. intuition (simplify_option_equality; auto).
    * intros (xs & y & Hxs & ? & Hx). revert x Hx.
      induction Hxs; intros; simplify_option_equality; [done |].
      rewrite elem_of_intersection_with. naive_solver.
  Qed.


  Lemma intersection_with_list_ind (P Q : AProp) f Xs Y :
    (∀ y, yYP y) →
    ForallX, ∀ x, xXQ x) Xs
    (∀ x y z, Q xP yf x y = Some zP z) →
    ∀ x, xintersection_with_list f Y XsP x.
  Proof.
    intros HY HXs Hf.
    induction Xs; simplify_option_equality; [done |].
    intros x Hx. rewrite elem_of_intersection_with in Hx.
    decompose_Forall. destruct Hx as (? & ? & ? & ? & ?). eauto.
  Qed.


  Context `{∀ X Y : C, Decision (XY)}.

  Lemma not_elem_of_intersection x X Y : xXYxXxY.
  Proof.
    rewrite elem_of_intersection.
    destruct (decide (xX)); tauto.
  Qed.

  Lemma not_elem_of_difference x X Y : xXYxXxY.
  Proof.
    rewrite elem_of_difference.
    destruct (decide (xY)); tauto.
  Qed.

  Lemma union_difference X Y : XYYXYX.
  Proof.
    split; intros x; rewrite !elem_of_union, elem_of_difference.
    * destruct (decide (xX)); intuition.
    * intuition.
  Qed.

  Lemma non_empty_difference X Y : XYYX ≢ ∅.
  Proof.
    intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
    destruct (decide (xX)); esolve_elem_of.
  Qed.

End collection.

Sets without duplicates up to an equivalence

Section no_dup.
  Context `{SimpleCollection A B} (R : relation A) `{!Equivalence R}.

  Definition elem_of_upto (x : A) (X : B) := ∃ y, yXR x y.
  Definition no_dup (X : B) := ∀ x y, xXyXR x yx = y.

  Global Instance: Proper ((≡) ==> iff) (elem_of_upto x).
  Proof. intros ??? E. unfold elem_of_upto. by setoid_rewrite E. Qed.
  Global Instance: Proper (R ==> (≡) ==> iff) elem_of_upto.
  Proof.
    intros ?? E1 ?? E2. split; intros [z [??]]; exists z.
    * rewrite <-E1, <-E2; intuition.
    * rewrite E1, E2; intuition.
  Qed.

  Global Instance: Proper ((≡) ==> iff) no_dup.
  Proof. firstorder. Qed.

  Lemma elem_of_upto_elem_of x X : xXelem_of_upto x X.
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
  Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅.
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
  Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y.
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.

  Lemma elem_of_upto_union X Y x :
    elem_of_upto x (XY) ↔ elem_of_upto x Xelem_of_upto x Y.
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.
  Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, yX → ¬R x y.
  Proof. unfold elem_of_upto. esolve_elem_of. Qed.

  Lemma no_dup_empty: no_dup ∅.
  Proof. unfold no_dup. solve_elem_of. Qed.
  Lemma no_dup_add x X : ¬elem_of_upto x Xno_dup Xno_dup ({[ x ]} ∪ X).
  Proof. unfold no_dup, elem_of_upto. esolve_elem_of. Qed.
  Lemma no_dup_inv_add x X : xXno_dup ({[ x ]} ∪ X) → ¬elem_of_upto x X.
  Proof.
    intros Hin Hnodup [y [??]].
    rewrite (Hnodup x y) in Hin; solve_elem_of.
  Qed.

  Lemma no_dup_inv_union_l X Y : no_dup (XY) → no_dup X.
  Proof. unfold no_dup. solve_elem_of. Qed.
  Lemma no_dup_inv_union_r X Y : no_dup (XY) → no_dup Y.
  Proof. unfold no_dup. solve_elem_of. Qed.
End no_dup.

Quantifiers

Section quantifiers.
  Context `{SimpleCollection A B} (P : AProp).

  Definition cforall X := ∀ x, xXP x.
  Definition cexists X := ∃ x, xXP x.

  Lemma cforall_empty : cforall ∅.
  Proof. unfold cforall. solve_elem_of. Qed.
  Lemma cforall_singleton x : cforall {[ x ]} ↔ P x.
  Proof. unfold cforall. solve_elem_of. Qed.
  Lemma cforall_union X Y : cforall Xcforall Ycforall (XY).
  Proof. unfold cforall. solve_elem_of. Qed.
  Lemma cforall_union_inv_1 X Y : cforall (XY) → cforall X.
  Proof. unfold cforall. solve_elem_of. Qed.
  Lemma cforall_union_inv_2 X Y : cforall (XY) → cforall Y.
  Proof. unfold cforall. solve_elem_of. Qed.

  Lemma cexists_empty : ¬cexists ∅.
  Proof. unfold cexists. esolve_elem_of. Qed.
  Lemma cexists_singleton x : cexists {[ x ]} ↔ P x.
  Proof. unfold cexists. esolve_elem_of. Qed.
  Lemma cexists_union_1 X Y : cexists Xcexists (XY).
  Proof. unfold cexists. esolve_elem_of. Qed.
  Lemma cexists_union_2 X Y : cexists Ycexists (XY).
  Proof. unfold cexists. esolve_elem_of. Qed.
  Lemma cexists_union_inv X Y : cexists (XY) → cexists Xcexists Y.
  Proof. unfold cexists. esolve_elem_of. Qed.
End quantifiers.

Section more_quantifiers.
  Context `{Collection A B}.

  Lemma cforall_weaken (P Q : AProp) (Hweaken : ∀ x, P xQ x) X :
    cforall P Xcforall Q X.
  Proof. unfold cforall. naive_solver. Qed.
  Lemma cexists_weaken (P Q : AProp) (Hweaken : ∀ x, P xQ x) X :
    cexists P Xcexists Q X.
  Proof. unfold cexists. naive_solver. Qed.
End more_quantifiers.

Fresh elements

We collect some properties on the fresh operation. In particular we generalize fresh to generate lists of fresh elements.
Section fresh.
  Context `{FreshSpec A C} .

  Definition fresh_sig (X : C) : { x : A | xX } :=
    exist (∉ X) (fresh X) (is_fresh X).

  Global Instance fresh_proper: Proper ((≡) ==> (=)) fresh.
  Proof. intros ???. by apply fresh_proper_alt, elem_of_equiv. Qed.

  Fixpoint fresh_list (n : nat) (X : C) : list A :=
    match n with
    | 0 => []
    | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
    end.

  Global Instance fresh_list_proper: Proper ((=) ==> (≡) ==> (=)) fresh_list.
  Proof.
    intros ? n ?. subst.
    induction n; simpl; intros ?? E; f_equal.
    * by rewrite E.
    * apply IHn. by rewrite E.
  Qed.


  Lemma fresh_list_length n X : length (fresh_list n X) = n.
  Proof. revert X. induction n; simpl; auto. Qed.

  Lemma fresh_list_is_fresh n X x : xfresh_list n XxX.
  Proof.
    revert X. induction n; intros X; simpl.
    * by rewrite elem_of_nil.
    * rewrite elem_of_cons. intros [?| Hin]; subst.
      + apply is_fresh.
      + apply IHn in Hin. solve_elem_of.
  Qed.


  Lemma fresh_list_nodup n X : NoDup (fresh_list n X).
  Proof.
    revert X.
    induction n; simpl; constructor; auto.
    intros Hin. apply fresh_list_is_fresh in Hin.
    solve_elem_of.
  Qed.

End fresh.

Definition option_collection `{Singleton A C} `{Empty C} (x : option A) : C :=
  match x with
  | None => ∅
  | Some a => {[ a ]}
  end.

Section collection_monad.
  Context `{CollectionMonad M}.

  Global Instance collection_guard: MGuard M := λ P dec A x,
    if dec then x else ∅.

  Global Instance collection_fmap_proper {A B} (f : AB) :
    Proper ((≡) ==> (≡)) (fmap f).
  Proof. intros X Y E. esolve_elem_of. Qed.
  Global Instance collection_ret_proper {A} :
    Proper ((=) ==> (≡)) (@mret M _ A).
  Proof. intros X Y E. esolve_elem_of. Qed.
  Global Instance collection_bind_proper {A B} (f : AM B) :
    Proper ((≡) ==> (≡)) (mbind f).
  Proof. intros X Y E. esolve_elem_of. Qed.
  Global Instance collection_join_proper {A} :
    Proper ((≡) ==> (≡)) (@mjoin M _ A).
  Proof. intros X Y E. esolve_elem_of. Qed.

  Lemma collection_fmap_compose {A B C} (f : AB) (g : BC) X :
    gf <$> Xg <$> (f <$> X).
  Proof. esolve_elem_of. Qed.
  Lemma elem_of_fmap_1 {A B} (f : AB) (X : M A) (y : B) :
    yf <$> X → ∃ x, y = f xxX.
  Proof. esolve_elem_of. Qed.
  Lemma elem_of_fmap_2 {A B} (f : AB) (X : M A) (x : A) :
    xXf xf <$> X.
  Proof. esolve_elem_of. Qed.
  Lemma elem_of_fmap_2_alt {A B} (f : AB) (X : M A) (x : A) (y : B) :
    xXy = f xyf <$> X.
  Proof. esolve_elem_of. Qed.

  Lemma elem_of_mapM {A B} (f : AM B) l k :
    lmapM f kForall2x y, xf y) l k.
  Proof.
    split.
    * revert l. induction k; esolve_elem_of.
    * induction 1; esolve_elem_of.
  Qed.

  Lemma mapM_length {A B} (f : AM B) l k :
    lmapM f klength l = length k.
  Proof. revert l; induction k; esolve_elem_of. Qed.

  Lemma elem_of_mapM_fmap {A B} (f : AB) (g : BM A) l k :
    Forallx, ∀ y, yg xf y = x) l
    kmapM g lfmap f k = l.
  Proof.
    intros Hl. revert k.
    induction Hl; simpl; intros;
      decompose_elem_of; simpl; f_equal; auto.
  Qed.


  Lemma elem_of_mapM_Forall {A B} (f : AM B) (P : BProp) l k :
    lmapM f k
    Forallx, ∀ y, yf xP y) k
    Forall P l.
  Proof. rewrite elem_of_mapM. apply Forall2_Forall_l. Qed.
  Lemma elem_of_mapM_Forall2_l {A B C} (f : AM B) (P : BCProp) l1 l2 k :
    l1mapM f k
    Forall2x y, ∀ z, zf xP z y) k l2
    Forall2 P l1 l2.
  Proof.
    rewrite elem_of_mapM. intros Hl1. revert l2.
    induction Hl1; inversion_clear 1; constructor; auto.
  Qed.

End collection_monad.