The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

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). 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?

Best wishes and a lot of fun,

jonas