Lvc.Infra.OptionMap

Require Import List Option Get.

Section ParametricOptionMapIndex.
  Variables X Y : Type.
  Hypothesis f : nat → X → option Y : Type.

  Fixpoint omapi_impl (n:nat) (L:list X) : option (list Y) :=
    match L with
      | x::L ⇒
        mdo v <- f n x;
          mdo vl <- omapi_impl (S n) L;
          Some (v::vl)
      | _ ⇒ Some nil
    end.

  Definition omapi := omapi_impl 0.

End ParametricOptionMapIndex.


Section ParametricOptionMap.
  Variables X Y : Type.
  Hypothesis f : X → option Y : Type.

  Fixpoint omap (L:list X) : option (list Y) :=
    match L with
      | x::L ⇒
        mdo v <- f x;
          mdo vl <- omap L;
          Some (v::vl)
      | _ ⇒ Some nil
    end.

  Lemma omap_inversion (L:list X) (L´:list Y)
  : omap L = Some L´
    → ∀ n x, get L n x → { y : Y | get L´ n y ∧ f x = Some y }.

End ParametricOptionMap.


Lemma omap_agree X Y (f g: X → option Y) L
: (∀ n x, get L n x → f x = g x)
  → omap f L = omap g L.

Lemma omap_agree_2 X X´ Y (f: X → option Y) (g: X´ → option Y) L L´
: (∀ n x y, get L n x → get L´ n y → f x = g y)
  → length L = length L´
  → omap f L = omap g L´.

Lemma omap_length X Y L´ (f: X → option Y) L
: omap f L = Some L´
  → length L = length L´.

Lemma omap_app X Y (f:X→option Y) L L´
: omap f (L ++ L´) =
  mdo v <- omap f L;
  mdo v´ <- omap f L´;
  Some (v ++ v´).