Lvc.Constr.MapAgreement

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

Set Implicit Arguments.

Section MapAgreement.
  Open Scope fmap_scope.

  Variable X : Type.
  Context `{OrderedType X}.

  Variable Y : Type.

  Definition agree_on (R:relation Y) (D:set X) (E E´:X → Y) :=
    ∀ x, x ∈ D → R (E x) (E´ x).

  Global Instance agree_on_refl `{Reflexive Y} L
    : Reflexive (agree_on R L).

  Global Instance agree_on_sym `{Symmetric Y} L
    : Symmetric (agree_on R L).

  Lemma agree_on_trans `{Transitive Y} L
    : Transitive (agree_on R L).

  Global Instance agree_on_equivalence `{Equivalence Y} {s:set X}
  : Equivalence (agree_on R s).

  Lemma agree_on_update (R:relation Y) L (E E´:X→Y) (x:X) (v v´:Y)
    : R v v´ → agree_on R L E E´ → agree_on R L (E[x<-v]) (E´[x<-v´]).

  Lemma agree_on_incl R (bv lv:set X) (E E´: X → Y)
    : agree_on R lv E E´
    → bv ⊆ lv
    → agree_on R bv E E´.

  Lemma agree_on_update_same (R:relation Y) (lv:set X) (E E´:X → Y) x v v´
  : R v v´
    → agree_on R (lv\{{x}}) E E´
    → agree_on R lv (E [x <- v]) (E´ [x <- v´]).

  Lemma agree_on_update_any_same (R:relation Y) (lv:set X) (E E´:X → Y) x v v´
  : R v v´
    → agree_on R lv E E´
    → agree_on R (lv ∪ {{x}}) (E [x <- v]) (E´ [x <- v´]).

  Lemma agree_on_update_dead R (lv:set X) (E E´:X → Y) x v
    : ¬x ∈ lv
    → agree_on R lv E E´
    → agree_on R lv (E [x <- v]) E´.

  Lemma agree_on_update_inv R (lv:set X) (E E´:X → Y) x v
  : agree_on R lv (E [x <- v]) E´
    → agree_on R (lv \ {{ x }}) E E´.

  Lemma agree_on_update_dead_both R (lv:set X) (E E´:X → Y) x v v´
    : ¬x ∈ lv
    → agree_on R lv E E´
    → agree_on R lv (E [x <- v]) (E´[x <- v´]).

End MapAgreement.

Lemma lookup_set_agree X `{OrderedType X} Y `{OrderedType Y} s (m m´:X → Y)
`{Proper _ (respectful _eq _eq) m} `{Proper _ (respectful _eq _eq) m´}
: @agree_on _ _ _ _eq s m m´ → lookup_set m s [=] lookup_set m´ s.

Definition eagree_on X `{OrderedType X} Y R `{Equivalence Y R} D E E´
           := @agree_on X _ Y R D E E´.


Global Instance eq_cset_agree_on_morphism X `{OrderedType X} Y R `{Transitive Y R} `{Symmetric Y R}
: Proper (SetInterface.Equal ==> (@feq X Y R) ==> (@feq X Y R) ==> iff) (agree_on R).

Global Instance incl_agree_on_morphism X `{OrderedType X} Y R `{Transitive Y R} `{Symmetric Y R}
: Proper (SetInterface.Equal ==> (@feq X Y R) ==> (@feq X Y R) ==> flip impl) (agree_on R).

Global Instance incl_agree_on_morphism_eq X `{OrderedType X} Y R `{Transitive Y R} `{Symmetric Y R}
: Proper (SetInterface.Equal ==> eq ==> eq ==> flip impl) (agree_on R).

Lemma eagree_on_union {X} `{OrderedType X} {Y} (f:X→Y) g D D´
  : eagree_on D f g
  → eagree_on D´ f g
  → eagree_on (D ∪ D´) f g.

Lemma agree_on_union {X} `{OrderedType X} {Y} (f:X→Y) R g D D´
  : agree_on R D f g
  → agree_on R D´ f g
  → agree_on R (D ∪ D´) f g.

Global Instance agree_on_computable {X} `{OrderedType X} {Y} `{OrderedType Y}
 (f g:X→Y) D `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> _eq) g}
  : Computable (eagree_on D f g).

Lemma map_agree X `{OrderedType X} Y `{OrderedType Y}
      lv (f:X→Y) `{Proper _ (_eq ==> _eq) f} (g:X→Y) `{Proper _ (_eq ==> _eq) g}
: agree_on _eq lv f g
  → map f lv [=] map g lv.

Hint Extern 10 (agree_on _ _?a ?a) ⇒ reflexivity.

Extraction Inline agree_on_computable.

Global Instance incl_agree_on_morphism_flip_impl X `{OrderedType X} Y R `{Transitive Y R} `{Symmetric Y R}
: Proper (SetInterface.Subset ==> eq ==> eq ==> flip impl) (agree_on R).

Hint Resolve agree_on_incl : cset.