未解決問題.v

Require Import Program Arith.

(** * リストモジュールの拡張 *)
Module List.
  Require Export List.
 
  Fixpoint _index_of_loop {A:Type} (eq_dec : forall (x y:A),{x=y}+{x<>y}) a xs i :=
    match xs with
    | nil => None
    | x::xs => if eq_dec x a then Some i else _index_of_loop eq_dec a xs (S i)
    end.
  Definition index_of {A:Type} (eq_dec : forall (x y:A),{x=y}+{x<>y}) a xs :=
    _index_of_loop eq_dec a xs 0.

  Lemma index_of_nth_Some : forall (A:Type) (eq_dec : forall (x y:A),{x=y}+{x<>y}) a xs i,
    index_of eq_dec a xs = Some i -> (forall dummy, nth i xs dummy = a).
  Proof.
   (*TODO 未解決問題*)
  Admitted.
  Lemma index_of_nth_None : forall (A:Type) (eq_dec : forall (x y:A),{x=y}+{x<>y}) a xs i,
    index_of eq_dec a xs = None -> forall dummy, a<>dummy -> nth i xs dummy <> a.
  Proof.
   (*TODO 未解決問題*)
  Admitted.

  Lemma index_of_In_Some : forall (A:Type) eq_dec (a:A) xs i,
    index_of eq_dec a xs = Some i -> In a xs.
  Proof.
   (*TODO 未解決問題*)
  Admitted.
  Lemma index_of_In_None : forall (A:Type) eq_dec (a:A) xs,
    index_of eq_dec a xs = None -> ~In a xs.
  Proof.
   (*TODO 未解決問題*)
  Admitted.

  (* sumbool版リストfilter *)
  Fixpoint filter' {A:Type}{P:A -> Prop}(P_dec : forall x, {P x}+{~P x})
    (xs: list A) : list A :=
    match xs with
    | nil => nil
    | x::xs => if P_dec x then x :: filter' P_dec xs
               else filter' P_dec xs
    end.

  Lemma filter'_In : forall (A:Type) (P:A->Prop) P_dec (x:A) l,
    In x (@filter' A P P_dec l) <-> In x l /\ P x.
  Proof.
   intros A P P_dec x l. split.
   (*TODO 未解決問題*)
  Admitted.

  Lemma remove_In : forall (A:Type)(eq_dec:forall(x y:A), {x=y}+{x<>y}) x l a,
    In a (List.remove eq_dec x l) <-> In a l /\ a <> x.
  Proof.
   (*TODO 未解決問題*)
  Admitted.

  (* lからxsのすべての要素を削除する *)
  Definition remove_all {A:Type}(eq_dec:forall(x y:A), {x=y}+{x<>y}) xs l :=
    List.fold_left (fun accl x => remove eq_dec x accl) xs l.

  Lemma remove_all_In : forall (A:Type)(eq_dec:forall(x y:A), {x=y}+{x<>y}) xs l y,
    In y (remove_all eq_dec xs l) <-> In y l /\ ~In y xs.
  Proof.
   induction xs.
   - simpl. tauto.
   - intros l y. split.
     + simpl. intro H.
       destruct (IHxs (remove eq_dec a l) y) as [HH _].
       set (HH H) as H0. destruct H0 as [In_y_rem notIn_y].
       admit. (*TODO 未解決問題*)
     + admit. (*TODO 未解決問題*)
  Qed.

  Fixpoint remove_i {A:Type} i (xs:list A) :=
    match i, xs with
    | O, x::xs => xs
    | S p, x::xs => x :: remove_i p xs
    | _, nil => nil
    end.

  Lemma remove_i_le_length : forall (A:Type) i (xs:list A),
    length xs <= i -> remove_i i xs = xs.
  Proof.
    (*TODO 未解決問題*)
  Admitted.

  Fixpoint insert_i {A:Type} i (y:A) (xs:list A) :=
    match i, xs with
    | O, _ => y::xs
    | S p, x::xs => x :: insert_i p y xs
    | S p, nil => nil (* indexに到達しないときは追加しない *)
    end.

  Fixpoint replace_i {A:Type} i (y:A) xs :=
    match i, xs with
    | _, nil => nil (*置き換えない*)
    | 0, x::xs => y::xs
    | S p, x::xs => x :: replace_i p y xs
    end.

  Lemma remove_i_replace_i : forall (A:Type) dummy i (xs ys:list A),
    remove_i i xs = remove_i i ys ->
    replace_i i (nth i ys dummy) xs = ys.
  Proof.
    (*TODO 未解決問題*)
  Admitted.

  Lemma map_remove_i : forall (A B:Type) (f:A->B) i xs,
    map f (remove_i i xs) = remove_i i (map f xs).
  Proof.
    (*TODO 未解決問題*)
  Admitted.

End List.