Lvc.Constr.MapInjectivity

Require Import EqDec Computable Util AutoIndTac LengthEq.
Require Export CSet Containers.SetDecide.
Require Export MapBasics MapUpdate MapLookup OrderedTypeEx.

Set Implicit Arguments.

Section MapInjectivity.
  Open Scope fmap_scope.
  Variable X : Type.
  Context `{OrderedType X}.
  Variable Y : Type.
  Context `{OrderedType Y}.

  Definition injective_on D (f:X→Y) :=
    ∀ x y, x ∈ D → y ∈ D → f x === f y → x === y.

  Lemma injective_on_incl (D D´:set X) (f:X → Y)
    : injective_on D f → D´ ⊆ D → injective_on D´ f.

  Lemma injective_on_dead lv (f:X → Y) x v `{Proper _ (respectful _eq _eq) f}
  : injective_on (lv\{{x}}) f
    → injective_on (lv\{{x}}) (f[x<-v]).

  Lemma injective_on_fresh lv (f:X → Y) x xr `{Proper _ (_eq ==> _eq) f}
    : injective_on (lv\{{x}}) f
      → ¬xr ∈ lookup_set f (lv\{{x}})
      → injective_on ({{x}} ∪ lv) (f[x <- xr]).

  Lemma injective_on_forget s (f:X → Y) y `{Proper _ (_eq ==> _eq) f}
  : injective_on s f
    → injective_on (s\{{y}}) f.

  Lemma lookup_set_minus_incl_inj s t (m:X → Y) `{Proper _ (_eq ==> _eq) m}
  : injective_on (s ∪ t) m
    → lookup_set m (s \ t) ⊆ lookup_set m s \ (lookup_set m t).

End MapInjectivity.

Global Instance injective_on_morphism {X} `{OrderedType X} {Y} {HY:OrderedType Y}
  : Proper (Equal ==> (@feq X Y (@_eq Y HY)) ==> iff) (@injective_on X H Y HY).

Lemma injective_on_update_not_in {X} `{OrderedType X} {Y} `{OrderedType Y}
  D x (f:X → Y) `{Proper _ (_eq ==> _eq) f}
: injective_on (D \ {{x}}) f
  → f x ∉ lookup_set f (D \ {{x}})
  → injective_on D f.

Lemma injective_on_update_fresh {X} `{OrderedType X} {Y} `{OrderedType Y}
  D x y f `{Proper _ (_eq ==> _eq) f}
: injective_on (D \ {{x}}) f
  → y ∉ lookup_set f (D \ {{x}})
  → injective_on D (update f x y).

Lemma injective_on_not_in_lookup_set {X} `{OrderedType X} {Y} `{OrderedType Y} f D D´ x
    `{Proper _ (_eq ==> _eq) f}
    : injective_on D f
      → D´ ⊆ D\{{x}} → x ∈ D
      → f x ∉ lookup_set f D´.

Lemma lookup_set_not_in {X} `{OrderedType X} {Y} `{OrderedType Y} f D x
    `{Proper _ (_eq ==> _eq) f}
  : f x ∉ lookup_set f D
    → lookup_set f D \ {{f x}} [=] lookup_set f (D\{{x}}).

Definition injective_on_step {X} {Y} `{OrderedType Y}
f (x : X) (p : set Y × bool) :=
      ({f x; fst p}, if snd p then
        negb (sumbool_bool (@decision_procedure (f x ∈ fst p) _))
       else false).

Lemma injective_on_step_transpose {X} {Y} `{OrderedType Y}
f
  : transpose _eq (@injective_on_step X Y _ f).

Lemma injective_on_step_spec {X} `{OrderedType X} {Y} `{OrderedType Y}
f (x : X) (p : set Y × bool) (s:set Y) b
: snd (injective_on_step f x (s,b))
   → {f x; s} [=] fst (injective_on_step f x (s,b)).

Global Instance injective_on_step_proper
  {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
  `{Proper _ (_eq ==> _eq) f}
 : Proper (_eq ==> _eq ==> _eq) (injective_on_step f).

Global Instance injective_on_step_proper´
  {X} `{OrderedType X} {Y} `{OrderedType Y} (f:X→Y)
  `{Proper _ (_eq ==> eq) f}
 : Proper (_eq ==> eq ==> eq) (injective_on_step f).

Definition injective_on_compute {X} `{OrderedType X} {Y} `{OrderedType Y}
  (D:set X) (f: X→ Y) `{Proper _ (_eq ==> _eq) f} : bool
  := snd (fold (injective_on_step f) D (∅, true)).

Lemma injective_on_compute_lookup_set {X} `{OrderedType X} {Y} `{OrderedType Y}
   (f: X→ Y) `{Proper _ (_eq ==> _eq) f}
:
  ∀ D LD´,
    lookup_set f D ∪ LD´ [=] fst (fold (injective_on_step f) D (LD´, true)).

Definition injective_on_iff {X} `{OrderedType X} {Y} `{OrderedType Y}
   (f: X→ Y) `{Proper _ (_eq ==> _eq) f} D
: ∀ D´ LD´,
    D´ ∩ D [=] ∅
    → lookup_set f D´ [=] LD´
    → injective_on D´ f
    → (snd (fold (injective_on_step f) D (LD´, true)) ↔ (injective_on (D ∪ D´) f)).

Global Instance injective_on_computable {X} `{OrderedType X} {Y} `{OrderedType Y}
  (D:set X) (f: X→ Y) `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> eq) f}
: Computable (injective_on D f).

Lemma lookup_set_minus_eq X `{OrderedType X} Y `{OrderedType Y} s t (m:X → Y) `{Proper _ (_eq ==> _eq) m}
: injective_on (s ∪ t) m
  → lookup_set m (s \ t) [=] lookup_set m s \ (lookup_set m t).

Lemma injective_on_agree X `{OrderedType X} Y `{OrderedType Y} D (ϱ ϱ´: X → Y)
: injective_on D ϱ
  → agree_on _eq D ϱ ϱ´
  → injective_on D ϱ´.

Lemma injective_on_fresh_list X `{OrderedType X} Y `{OrderedType Y} XL YL (ϱ: X → Y) `{Proper _ (_eq ==> _eq) ϱ} lv
: injective_on lv ϱ
  → length XL = length YL
  → (of_list YL) ∩ (lookup_set ϱ lv) [=] ∅
  → unique XL
  → unique YL
  → injective_on (lv ∪ of_list XL) (ϱ [XL <-- YL]).