Lvc.Constr.MapLookupList

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

Set Implicit Arguments.

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

  Open Scope fmap_scope.

  Fixpoint lookup_list (m:X → Y) (L:list X) : list Y :=
    match L with
      | nil ⇒ nil
      | x::L ⇒ m x::lookup_list m L
    end.

  Lemma update_with_list_app (A A´ : list X) (B B´ : list Y) E
    : length A = length B
    → update_with_list (A++A´) (B++B´) E = update_with_list A B (update_with_list A´ B´ E).

  Lemma lookup_list_length (m:X → Y) (L:list X)
    : length (lookup_list m L) = length L.

  Lemma lookup_list_agree (m m´:X → Y) (L:list X)
    : agree_on eq (of_list L) m m´
    → lookup_list m L = lookup_list m´ L.

  Lemma of_list_lookup_list `{OrderedType Y} (m:X → Y) L
    : Proper (_eq ==> _eq) m
      → of_list (lookup_list m L) [=] lookup_set m (of_list L).

End MapLookupList.

Lemma lookup_id X (l:list X)
: lookup_list (@id X) l = l.

Global Instance update_with_list_inst X `{OrderedType X} Y `{OrderedType Y} :
  Proper (eq ==> eq ==> (@feq X Y _eq ) ==> (@feq _ _ _eq)) (@update_with_list X _ Y).

Global Instance lookup_list_inst X `{OrderedType X} Y:
  Proper ((@feq X Y eq) ==> eq ==> eq) (@lookup_list X Y).

Lemma update_with_list_lookup_list X `{OrderedType X} Y `{OrderedType Y} (E:X → Y)
     `{Proper _ (_eq ==> _eq) E} (Z : list X)
: @feq _ _ _eq (update_with_list Z (lookup_list E Z) E) E.

Lemma lookup_list_app X Y (A A´:list X) (E:X → Y)
: lookup_list E (A ++ A´) = List.app (lookup_list E A) (lookup_list E A´).

Lemma lookup_list_unique X `{OrderedType X} Y (Z:list X) (Z´:list Y) f
: length Z = length Z´
  → unique Z
  → lookup_list (f [Z <-- Z´]) Z = Z´.

Hint Resolve lookup_list_agree : cset.