coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity on existT

From: Daniel Schepler <dschepler AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] injectivity on existT
Date: Mon, 30 May 2016 15:45:08 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dschepler AT gmail.com; spf=Pass smtp.mailfrom=dschepler AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f47.google.com
Ironport-phdr: 9a23:qFFPQhSjOaazR+l+onPbDEuyu9psv+yvbD5Q0YIujvd0So/mwa64YxWN2/xhgRfzUJnB7Loc0qyN4/GmBDBLuMzJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbviqtuOP04R3nKUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGY2zRakzTKRZATI6KCh1oZSz7ViQBTeIs1AbSy09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGGO5qFqRRugsywHOiY9/Xuf3sBrh6JWuBasvTRwxofVZMeeM/8oLfCVRs8TWWcUBpUZbCdGGI7pKtJXV+c=

On Mon, May 30, 2016 at 2:50 PM, Adam Chlipala
<adamc AT csail.mit.edu>
wrote:
> In general, it requires an axiom. If you [Require Import Eqdep], you get it
> as [inj_pair2].
>
>
> On 05/30/2016 05:48 PM, Jonathan Leivent wrote:
>>
>> Is this provable?:
>>
>> Lemma existT_inj : forall T f x a b, @existT T f x a = @existT T f x b ->
>> a = b.
>>
>> I can't prove it with injectivity, or by f_equal with projT2. If it is
>> provable, what's the secret ingredient?

And in a specific case, if you have a decision procedure for equality
to x, then existT_inj holds for that case. (Ex: if T = nat; or if T =
option A, and x = None.)
--
Daniel Schepler

[Coq-Club] injectivity on existT, Jonathan Leivent, 05/30/2016
- Re: [Coq-Club] injectivity on existT, Adam Chlipala, 05/30/2016
  - Re: [Coq-Club] injectivity on existT, Daniel Schepler, 05/31/2016
    - Re: [Coq-Club] injectivity on existT, Jonathan Leivent, 05/31/2016
      - Re: [Coq-Club] injectivity on existT, Jonathan Leivent, 05/31/2016