The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Mon, Jun 10, 2013 at 8:38 AM,  
<fr.inria.coq-club AT io7m.com>
 wrote:
> 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).
>
[snip]
> 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?

It's provable if you have decidable equality on the base type:

Require Import Program.

Program Fixpoint eqdec_inp_inpt
  {A : Type} {Aeq : forall x y : A, { x = y } + { x <> y }}
  {x : A} {xs : list A} (H : InP x xs) : InPT x xs :=
match xs with
| [] => !
| x0 :: xs' =>
    if Aeq x x0 then
      InPT_Here x (xs := xs')
    else
      InPT_There x (eqdec_inp_inpt (Aeq := Aeq) (x := x) (xs := xs') _)
end.
Next Obligation.
inversion H.
Defined.
Next Obligation.
inversion H; subst.
contradict H0; reflexivity.
trivial.
Defined.

Therefore, since classic_dec : forall P:Prop, { P } + { ~P } is
consistent, so is InP -> InPT.

On the other hand, here's my argument that InP -> InPT is not provable
axiom-free: take the model where Type is the category of sheaves of
types on R, and Prop is the subobject classifier.  Take A to be
{0,1,2} modulo the equivalence relation generated by 0 == 2 on (-∞,1)
and 1 == 2 on (0,∞); and then x := 2, xs := [0; 1].  Then InP x xs has
a global section taking by gluing InP_Here on (-∞,1) and InP_There
InP_Here on (0,∞).  On the other hand, there's no global section of
nat which would be a valid value for position of a global section of
InPT x xs (as such a global section would have to be a constant member
of nat).  Thus, there can be no global section of the sheaf InP x xs
-> InPT x xs; which implies InP -> InPT cannot be proved axiom-free in
Coq, or that would result on interpretation in such a global section.
In fact, it can't even be proved assuming proof irrelevance and the
"constructive definite description" operator (exists! x, P x) -> {x |
P x}.
-- 
Daniel Schepler