gistfile1.v

Definition prop_dec T : Type :=
  { P : T -> Prop & forall x, {P x} + {~ P x}}
.

Definition make_prop_dec
  T
  (P : T -> Prop)
  (decide : forall x, {P x} + {~ P x})
  : prop_dec T
  :=
    existT
      (fun Q => forall x, {Q x} + {~ Q x})
      P
      decide.


Definition nat_eq_dec (a b : nat)
 : {a = b} + {a <> b}.
decide equality.
Defined.

Definition prop_dec_eq_1 : prop_dec nat :=
  make_prop_dec
    nat
    (fun x => x = 1)
    (fun x => nat_eq_dec x 1)
.


Require Import List.

(* can't use prop_dec here, because "list_forall"
   is defined in other module in my real case. *)
Inductive list_forall A P : list A -> Prop :=
  | lf_nil : list_forall A P nil
  | lf_cons : forall h t,
      P h ->
      list_forall A P t ->
      list_forall A P (h :: t)
.
Hint Constructors list_forall.


Print List.filter.

Print sigT.
Print exist.

Definition prop_of_pd
  {T : Type} (PD : prop_dec T) :=
  match PD with
  | existT P D => P
  end
.

Definition my_list_filter
  {A : Type}
  (PD : prop_dec A)
  (lst : list A)
  :
  { r : list A | list_forall A (prop_of_pd PD) r }
.
destruct PD as [P D].
unfold prop_of_pd.
refine (
  let pred x :=
    match D x with
    | left _ => true
    | right _ => false
    end
  in
  let r := List.filter pred lst
  in
  exist _ r _
).
induction lst as [ | h t].
(* lst nil *)
  apply lf_nil.
(* lst cons *)
  simpl in *.
  unfold pred in *.
  destruct (D h) as [ Ph | NotPh ].
  (* P h *)
    apply (lf_cons A P h _ Ph).
    exact IHt.
  (* ~ P h *)
    auto.
Defined.

Eval compute in
  (my_list_filter
     prop_dec_eq_1
     (0 :: 1 :: 2 :: 1 :: nil)
  )
.