Qcert.Basic.Util.RLift

Section RLift.


  Definition lift {A B:Type} (f:A→B) : (option A → option B)
    := fun a ⇒
         match a with
           | None ⇒ None
           | Some a' ⇒ Some (f a')
         end.

  Definition olift {A B} (f:A → option B) (x:option A) : option B :=
    match x with
      | None ⇒ None
      | Some x' ⇒ f x'
    end.

  Definition bind {A B:Type} a b := (@olift A B b a).

  Definition olift_some {A B} (f:A → option B) (x:A) :
    olift f (Some x) = f x.

  Definition olift2 {A B C} (f:A → B → option C) (x1:option A) (x2:option B) : option C :=
    match x1,x2 with
      | Some d1, Some d2 ⇒ f d1 d2
      | _,_ ⇒ None
    end.

  Lemma olift2_none_r {A B C} (f:A → B → option C) (x1:option A) :
    olift2 f x1 None = None.

  Lemma olift2_somes {A B C} (f:A → B → option C) (x1:A) (x2:B) :
    olift2 f (Some x1) (Some x2) = f x1 x2.

  Lemma lift_some_simpl {A B:Type} (f:A→B) x : lift f (Some x) = Some (f x).

  Lemma lift_some_simpl_eq {A B:Type} (f:A→B) x y :
    f x = f y ↔
    lift f (Some x) = Some (f y).

  Lemma lift_none_simpl {A B:Type} (f:A→B) : lift f None = None.

  Lemma lift_none {A B:Type} {f:A→B} {x} :
    x = None →
    lift f x = None.

  Lemma lift_some {A B:Type} {f:A→B} {x y} z :
    x = Some z →
    f z = y →
    lift f x = Some y.

  Lemma none_lift {A B:Type} {f:A→B} {x} :
    lift f x = None →
    x = None.

  Lemma some_lift {A B:Type} {f:A→B} {x y} :
    lift f x = Some y →
    {z | x = Some z & y = f z}.

  Lemma lift_injective {A B:Type} (f:A→B) :
    (∀ x y, f x = f y → x = y) →
    (∀ x y, lift f x = lift f y → x = y).

  Fixpoint lift_map {A B:Type} (f:A → option B) (l:list A) : option (list B) :=
    match l with
      | nil ⇒ Some nil
      | x::l' ⇒
        match (f x) with
          | None ⇒ None
          | Some x' ⇒
            match lift_map f l' with
              | None ⇒ None
              | Some l'' ⇒ Some (x'::l'')
            end
        end
    end.

  Fixpoint lift_filter {A:Type} (f:A → option bool) (l:list A) : option (list A) :=
    match l with
      | nil ⇒ Some nil
      | x::l' ⇒
        match (f x) with
          | None ⇒ None
          | Some b ⇒
            match lift_filter f l' with
              | None ⇒ None
              | Some l'' ⇒
                if b then Some (x::l'') else Some l''
            end
        end
    end.

  Definition lift_app {A:Type} (l1 l2:option (list A)) : option (list A) :=
    match l1,l2 with
      | Some l1',Some l2' ⇒ Some (l1'++l2')
      | _,_ ⇒ None
    end.

  Definition lift2 {A B C:Type} (f:A → B → C) (x:option A) (y:option B) : option C :=
    match x,y with
      | Some x', Some y' ⇒ Some (f x' y')
      | _,_ ⇒ None
    end.

  Lemma lift_filter_eq {A} (f g:A → option bool) l :
    (∀ a, In a l → f a = g a) →
    lift_filter f l = lift_filter g l.

  Lemma lift_app_filter {A:Type} (p:A → option bool) (l1 l2:list A):
    lift_filter p (app l1 l2) = lift2 (@app A) (lift_filter p l1) (lift_filter p l2).

  Lemma lift_id {A} (x:option A) :
    lift (fun l'' ⇒ l'') x = x.

  Lemma match_lift_id {A} (x:option A) :
    match x with
      | None ⇒ None
      | Some l'' ⇒ Some l''
    end = x.

End RLift.