Lvc.Constr.MapComposition

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

Set Implicit Arguments.

Definition comp {X Y Z:Type} (f:X → Y) (g:Y→Z) : X→Z := fun x ⇒ g (f x).
Notation "f ´∘´ g" := (comp f g) (at level 40, left associativity) : fmap_scope.

Open Scope fmap_scope.

Lemma comp_lookup_list X Y Z (f:X → Y) (g:Y → Z) L
    : lookup_list (f∘g) L = lookup_list g (lookup_list f L).

Lemma lookup_set_agree_on_comp {X} `{OrderedType X} {Y} `{OrderedType Y} Z (f:X → Y) (g:Y → Z)
      `{Proper _ (_eq ==> _eq) f}
      x y z D
: y ∉ lookup_set f (D\{{x}})
  → agree_on eq D ((f[x<-y]) ∘ (g[y<-z])) ((f ∘ g) [x <- z]).

Lemma inverse_on_comp {X} `{OrderedType X} {Y} `{OrderedType Y} {Z} `{OrderedType Z}
  (f:X → Y) f´ (g:Y → Z) g´ x y z D
: inverse_on D ((f[x<-y]) ∘ (g[y<-z])) ((g´[z<-y]) ∘ (f´[y<-x]))
  → inverse_on D ((f ∘ g) [x <- z]) ((g´ ∘ f´) [z <- x]).

Lemma inverse_on_comp_agree {X} `{OrderedType X} {Y} `{OrderedType Y} {Z} `{OrderedType Z}
  (f:X → Y) f´ (g:Y → Z) g´ x y z D
: inverse_on D ((f[x<-y]) ∘ (g[y<-z])) ((g´[z<-y]) ∘ (f´[y<-x]))
  → agree_on _eq D ((f[x<-y]) ∘ (g[y<-z])) ((f ∘ g) [x <- z]).

Lemma inverse_on_comp_list {X} `{OrderedType X} {Y} `{OrderedType Y} {Z} `{OrderedType Z}
  (f:X → Y) (f´:Y → X) (g:Y → Z) (g´: Z → Y)
  `{Proper _ (_eq ==> _eq) f} `{Proper _ (_eq ==> _eq) g}
`{Proper _ (_eq ==> _eq) f´} `{Proper _ (_eq ==> _eq) g´}
XL YL ZL D :
  length XL = length YL
  → length YL = length ZL

  → inverse_on D ((update_with_list XL YL f) ∘ (update_with_list YL ZL g))
               ((update_with_list ZL YL g´) ∘ (update_with_list YL XL f´))
  → agree_on _eq D ((update_with_list XL YL f) ∘ (update_with_list YL ZL g)) (update_with_list XL ZL (f ∘ g)).