Module RLift

Section RLift.

  Require Import List.

  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) :
    (forall x y, f x = f y -> x = y) ->
    (forall 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 :
    (forall 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.

Hint Rewrite @olift_some : alg.
Hint Rewrite @olift2_none_r : alg.
Hint Rewrite @olift2_somes : alg.

Ltac case_option
  := match goal with
         [|- context [match ?x with
                        | Some _ => _
                        | None => _
                      end]] => case_eq x
     end.

Ltac case_lift
  := match goal with
         [|- context [lift _ ?x]] => case_eq x
     end.

Ltac case_option_in H
  := match type of H with
         context [match ?x with
                    | Some _ => _
                    | None => _
                  end] => let HH:=(fresh "eqs") in case_eq x; [intros ? HH|intros HH]; try rewrite HH in H
     end.

Ltac case_lift_in H
  := match type of H with
         context [lift _ ?x] => let HH:=(fresh "eqs") in case_eq x; [intros ? HH|intros HH]; try rewrite HH in H
     end.