The Coq mailing list

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

On 26/04/2016 14:19, Jonas Oberhauser wrote:
> I have a set M and two subsets of M,  N,N'.
> I have functions in dependent products over N,N', that agree on the
> codomain,
> f : forall n : N, X n
> f' : forall n : N', X n
> Where X : M -> Type
> 
> When the two subsets are disjoint, I want to merge these functions:
> 
> merge f f'  :  forall n : N union N', X n
> 
> In set theory, merge is simply the union, but one might do extra work
> and define
> merge f f' n = if n : N then f n else f' n
> 
> What would be the best way to formalize this whole thing in Coq?
> I have thought about using predicates in the domain, (f : forall n : M,
> P n -> X n) but this has problems (P needs to be decidable because of
> the elim restriction, and one has to work with PI).

Note that if you express P has a boolean predicate (since it is
decidable, it might has well be boolean), you do not have to bother with
proof irrelevance, it comes for free.

> I have also thought
> about putting the partiality into the codomain (f : forall n : M, X n *
> P n + ~ P n), but that again assumes decidability of P and I need to
> deal with the second case all the time. If I have a decider for P, I
> might as well descruct it in the return type (if dec P n then X n else
> unit).
> 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').

Best regards,

Guillaume