The Coq mailing list

[<fr.inria.coq-club AT io7m.com>]

Hi.

I have the following definition:

Require Coq.Lists.List.

Open Scope list_scope.

(** An inductive predicate that [x] is in [xs]. *)
Inductive InP {A : Type} (x : A) : list A -> Prop :=
  | InP_Here  : forall {xs : list A}, InP x (x :: xs)
  | InP_There : forall {y  : A} {xs : list A}, InP x xs -> InP x (y :: xs).

(** An inductive predicate that [x] is in [xs], in [Type]. *)
Inductive InPT {A : Type} (x : A) : list A -> Type :=
  | InPT_Here  : forall {xs : list A}, InPT x (x :: xs)
  | InPT_There : forall {y  : A} {xs : list A}, InPT x xs -> InPT x (y :: xs).

(** [InPT] implies [InP]. *)
Lemma inpt_inp : forall
  {A  : Type}
  {x  : A}
  {xs : list A},
  InPT x xs -> InP x xs.
Proof.
  induction xs as [|xh xr].
    intros H_in; inversion H_in.
    intros H_in.
    inversion H_in.
      rewrite <- H0 in H_in.
      rewrite <- H0.
      apply InP_Here.
      pose proof (IHxr X) as H_ixr.
      apply InP_There.
      assumption.
Qed.

Fixpoint position
  {A  : Type}
  {x  : A}
  {xs : list A}
  (H0 : InPT x xs)
: nat :=
  match H0 with
  | InPT_Here  _      => 0
  | InPT_There _ _ H1 => S (position H1)
  end.

Note that "position" requires "InP in Type" because it requires case
analysis of H0.

I'd like to show that InP -> InPT, but this doesn't seem to be provable
in Coq's logic directly. Is it safe to assume this as an axiom? Perhaps
it's a consequence of some other more general "safe" (read "consistent")
axiom?

M