The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Dear Guillaume,
thanks for your response.

Am 26.04.2016 um 14:34 schrieb Guillaume Melquiond:
> 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.

That makes sense. I used booleans before but found the automatization 
for rewriting was not so good. Is there a tactic that normalizes boolean 
expressions (by normalize I mean here to turn into a unique DNF or such)?

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

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.

Thanks again and best wishes,
Jonas