Lvc.Constr.MapAgreeSet

Require Export Setoid Coq.Classes.Morphisms.
Require Import EqDec Computable Util AutoIndTac.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapLookup MapAgreement.

Set Implicit Arguments.

Section MapAgreeSet.
  Variable X : Type.
  Context `{OrderedType X}.
  Variable Y : Type.
  Context `{OrderedType Y}.

  Definition agree_set (lv:set X) (m m´:X → Y) : set X
    := filter (fun x ⇒ if [m x === m´ x] then true else false) lv.

  Lemma agree_set_spec (lv:set X) (m m´: X → Y) x
        `{Proper _ (respectful _eq _eq) m} `{Proper _ (respectful _eq _eq) m´}
  : x ∈ agree_set lv m m´ ↔ x ∈ lv ∧ m x === m´ x.

  Lemma agree_on_agree_set_eq
        (lv:set X) (D D´:X → Y)
        `{Proper _ (respectful _eq _eq) D} `{Proper _ (respectful _eq _eq) D´}
  : agree_on _eq lv D D´ → agree_set lv D D´ [=] lv.

  Lemma agree_set_agree_on Z `{OrderedType Z}
        (lv:set X) (D D´:X → Y) (E E´: X → Z)
        `{Proper _ (respectful _eq _eq) D} `{Proper _ (respectful _eq _eq) D´}
  : agree_on _eq lv D D´ → agree_on _eq (agree_set lv D D´) E E´
    → agree_on _eq lv E E´.

  Lemma agree_on_agree_set (lv:set X) (D D´ D´´: X → Y)
        `{Proper _ (respectful _eq _eq) D}
        `{Proper _ (respectful _eq _eq) D´}
        `{Proper _ (respectful _eq _eq) D´´}
  : agree_on _eq lv D D´ → agree_set lv D D´´ ⊆ agree_set lv D´ D´´.

  Lemma agree_set_incl (lv:set X) (D D´: X → Y)
        `{Proper _ (respectful _eq _eq) D}
        `{Proper _ (respectful _eq _eq) D´}
  : (agree_set lv D D´) ⊆ lv.

  Lemma agree_set_incl_both (lv´ lv:set X) (D D´:X→Y)
        `{Proper _ (respectful _eq _eq) D}
        `{Proper _ (respectful _eq _eq) D´}
  : lv´ ⊆ lv → agree_set lv´ D D´ ⊆ agree_set lv D D´.

End MapAgreeSet.


Global Instance eq_cset_agree_set_morphism X `{OrderedType X} Y `{OrderedType Y}
  : Proper (SetInterface.Equal ==> (@fpeq X Y _eq H H0) ==> (@fpeq X Y _eq _ _) ==> SetInterface.Equal) (@agree_set X _ Y _ ).

Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y} : (@lookup_set X _ Y _)
  with signature (@fpeq X Y _eq _ _) ==> SetInterface.Equal ==> SetInterface.Equal
    as eq_cset_lookup_set_morphism.

Add Parametric Morphism {X} `{OrderedType X} {Y} `{OrderedType Y}
  : (@lookup_set X _ Y _)
  with signature (@fpeq X Y _eq _ _) ==> Subset ==> Subset
    as incl_lookup_set_morphism.

Lemma agree_set_minus X `{OrderedType X} Y `{OrderedType Y} lv lv´ (D D´: X → Y)
      `{Proper _ (_eq ==> _eq) D} `{Proper _ (_eq ==> _eq) D´}
: agree_set lv D D´ \ lv´ [=] agree_set (lv \ lv´) D D´.