Require Import List.
Import ListNotations.
Require Import StructTact.StructTactics.
Require Import StructTact.ListTactics.

Set Implicit Arguments.

Fixpoint filterMap {A B} (f : A -> option B) (l : list A) : list B :=
  match l with
    | [] => []
    | x :: xs => match f x with
                   | None => filterMap f xs
                   | Some y => y :: filterMap f xs
                 end
  end.

Section filter_map.
  Variables A B C : Type.

  Lemma map_of_filterMap :
    forall (f : A -> option B) (g : B -> C) l,
      map g (filterMap f l) = filterMap (fun x => match f x with
                                                 | Some y => Some (g y)
                                                 | None => None
                                                 end) l.
  Proof using.
(* Goal: forall (f g : forall _ : A, option B) (l : list A) (_ : forall x : A, @eq (option B) (f x) (g x)), @eq (list B) (@filterMap A B f l) (@filterMap A B g l) *)
    induction l; intros; simpl in *.
    - auto.
    - repeat break_match; simpl; auto using f_equal.
  Qed.

  Lemma filterMap_ext :
    forall (f g : A -> option B) l,
      (forall x, f x = g x) ->
      filterMap f l = filterMap g l.
  Proof using.
(* Goal: forall (f g : forall _ : A, option B) (l : list A) (_ : forall x : A, @eq (option B) (f x) (g x)), @eq (list B) (@filterMap A B f l) (@filterMap A B g l) *)
    induction l; intros; simpl in *.
    - auto.
    - repeat find_higher_order_rewrite; auto.
  Qed.

  Lemma filterMap_defn :
    forall (f : A -> option B) x xs,
      filterMap f (x :: xs) = match f x with
                             | Some y => y :: filterMap f xs
                             | None => filterMap f xs
                             end.
  Proof using.
(* Goal: forall (f : forall _ : A, option B) (x : A) (xs : list A), @eq (list B) match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end *)
    simpl. auto.
  Qed.

  Lemma In_filterMap :
    forall (f : A -> option B) b xs,
      In b (filterMap f xs) ->
      exists a,
        In a xs /\ f a = Some b.
  Proof using.
(* Goal: forall (f : forall _ : A, option B) (b : B) (xs : list A) (_ : @In B b (@filterMap A B f xs)), @ex A (fun a : A => and (@In A a xs) (@eq (option B) (f a) (@Some B b))) *)
    intros.
(* Goal: @ex A (fun a : A => and (@In A a xs) (@eq (option B) (f a) (@Some B b))) *)
    induction xs; simpl in *; intuition.
(* Goal: @ex A (fun a0 : A => and (or (@eq A a a0) (@In A a0 xs)) (@eq (option B) (f a0) (@Some B b))) *)
    break_match.
    - simpl in *. intuition; subst; eauto.
(* Goal: @ex A (fun a0 : A => and (or (@eq A a a0) (@In A a0 xs)) (@eq (option B) (f a0) (@Some B b))) *)
      break_exists_exists; intuition.
    - concludes. break_exists_exists; intuition.
  Qed.

  Lemma filterMap_app :
    forall (f : A -> option B) xs ys,
      filterMap f (xs ++ ys) = filterMap f xs ++ filterMap f ys.
  Proof using.
(* Goal: forall (f : forall _ : A, option B) (xs ys : list A), @eq (list B) (@filterMap A B f (@app A xs ys)) (@app B (@filterMap A B f xs) (@filterMap A B f ys)) *)
    induction xs; intros; simpl in *; repeat break_match; simpl in *; intuition auto using f_equal.
  Qed.

  Lemma filterMap_In :
    forall A B (f : A -> option B) a b xs,
      f a = Some b ->
      In a xs ->
      In b (filterMap f xs).
  Proof using.
(* Goal: forall (A B : Type) (f : forall _ : A, option B) (a : A) (b : B) (xs : list A) (_ : @eq (option B) (f a) (@Some B b)) (_ : @In A a xs), @In B b (@filterMap A B f xs) *)
    induction xs; simpl; repeat break_match; simpl; intuition (auto; try congruence).
  Qed.

  Lemma filterMap_of_filterMap :
    forall (f : B -> option C) (g : A -> option B) xs,
      filterMap f (filterMap g xs) =
      filterMap (fun a => match g a with
                         | Some b => f b
                         | None => None
                         end) xs.
  Proof using.
(* Goal: forall (f : forall _ : B, option C) (g : forall _ : A, option B) (xs : list A), @eq (list C) (@filterMap B C f (@filterMap A B g xs)) (@filterMap A C (fun a : A => match g a with | Some b => f b | None => @None C end) xs) *)
    induction xs; simpl; intuition.
(* Goal: forall (f : forall _ : A, option B) (x : A) (xs : list A), @eq (list B) match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end *)
    repeat break_match; simpl; repeat find_rewrite; auto.
  Qed.

  Lemma filterMap_all_None :
    forall (f : A -> option B) xs,
      (forall x, In x xs -> f x = None) ->
      filterMap f xs = [].
  Proof using.
(* Goal: forall (f : forall _ : A, option B) (xs : list A) (_ : forall (x : A) (_ : @In A x xs), @eq (option B) (f x) (@None B)), @eq (list B) (@filterMap A B f xs) (@nil B) *)
    induction xs; intros; simpl in *; intuition.
(* Goal: forall (f : forall _ : A, option B) (x : A) (xs : list A), @eq (list B) match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end *)
    rewrite H; auto.
  Qed.

  Lemma filterMap_NoDup_inj :
    forall (f : A -> option B) l,
      (forall x1 x2 y,
          f x1 = Some y ->
          f x2 = Some y ->
          x1 = x2) ->
      NoDup l ->
      NoDup (filterMap f l).
  Proof using.
(* Goal: forall (f : forall _ : A, option B) (b : B) (xs : list A) (_ : @In B b (@filterMap A B f xs)), @ex A (fun a : A => and (@In A a xs) (@eq (option B) (f a) (@Some B b))) *)
    induction l; intros.
    - constructor.
    - simpl. invc_NoDup.
(* Goal: forall (f : forall _ : A, option B) (x : A) (xs : list A), @eq (list B) match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end *)
      break_match; auto.
(* Goal: forall (f : forall _ : A, option B) (x : A) (xs : list A), @eq (list B) match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end *)
      constructor; auto.
(* Goal: not (@In B b (@filterMap A B f l)) *)
      intro.
(* Goal: False *)
      find_apply_lem_hyp In_filterMap. break_exists. break_and.
(* Goal: forall (f : forall _ : A, option B) (x : A) (xs : list A), @eq (list B) match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end match f x with | Some y => @cons B y (@filterMap A B f xs) | None => @filterMap A B f xs end *)
      assert (a = x) by eauto.
(* Goal: False *)
      subst. contradiction.
  Qed.
End filter_map.
