Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] merging functions over disjoint domains

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] merging functions over disjoint domains


Chronological Thread 
  • From: Jonas Oberhauser <s9joober AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] merging functions over disjoint domains
  • Date: Wed, 27 Apr 2016 19:28:51 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=s9joober AT gmail.com; spf=Pass smtp.mailfrom=s9joober AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f45.google.com
  • Ironport-phdr: 9a23:BdcbuRBu1d2IeLOP2bHZUyQJP3N1i/DPJgcQr6AfoPdwSP74r8bcNUDSrc9gkEXOFd2CrakU26yG6eu7BiQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTnkbDosMaMKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1kbVGwN2j1CDhLF5QzhU4255jCrtO160iSAFcLzRLEwHz+l6vE4G1fTlC4bOmthoynsgctqgfcDrQ==

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



Archive powered by MHonArc 2.6.18.

Top of Page