The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 27/04/2016 19:28, Jonas Oberhauser wrote:

>>> Are there better solutions, in particular ones that do not need
>>> decidability of P?
>> Certainly not without the decidability of P. Think about the following
>> type:
>>
>> Inductive X : M -> Type :=
>>    | X0 : forall n, P n -> X n
>>    | X1 : forall n, not (P n) -> X n.
>>
>> By taking f and f' as identity functions, you get a way to decide P if
>> you have a way to define (merge f f').
> 
> I'm not sure I follow.  What are the types of f and f'? By identities,
> do you mean (fun n => n)? I can not merge these since they have the same
> domain (domains have to be disjoint) or different codomains.
> If I would merge X0 and X1 I would expect to obtain a function forall n,
> P n \/ not (P n) -> X n, which should not give me a decider for P unless
> I already work classically.

You are mixing two kinds of decidability here. (I don't know if there is
a better way to name them.) One is the excluded-middle property and the
other is the existence of an algorithm. Here is a Coq script to make it
clearer:

Parameter M : Type.
Definition merge {X} {P P' : M -> Prop} (f : forall n, P n -> X n)
  (f' : forall n, P' n -> X n) : forall n, P n \/ P' n -> X n.
Admitted.

Parameter P : M -> Prop.
Inductive X : M -> Type :=
   | X0 : forall n, P n -> X n
   | X1 : forall n, not (P n) -> X n.

Lemma foo : forall n, P n \/ not (P n) -> {P n} + {not (P n)}.
Proof.
intros n H.
apply (merge X0 X1 n) in H.
now destruct H as [H|H] ; [left|right].
Qed.

Best regards,

Guillaume