coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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'.Note that if you express P has a boolean predicate (since it is
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).
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 thoughtCertainly not without the decidability of P. Think about the following type:
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?
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
- [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/26/2016
- Re: [Coq-Club] merging functions over disjoint domains, Guillaume Melquiond, 04/26/2016
- Re: [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/27/2016
- Re: [Coq-Club] merging functions over disjoint domains, Guillaume Melquiond, 04/27/2016
- Re: [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/27/2016
- Re: [Coq-Club] merging functions over disjoint domains, Abhishek Anand, 04/27/2016
- Re: [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/27/2016
- Re: [Coq-Club] merging functions over disjoint domains, Guillaume Melquiond, 04/27/2016
- Re: [Coq-Club] merging functions over disjoint domains, Jonas Oberhauser, 04/27/2016
- Re: [Coq-Club] merging functions over disjoint domains, Guillaume Melquiond, 04/26/2016
Archive powered by MHonArc 2.6.18.