coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Injectivity of existT

From: Adam Chlipala <adamc AT csail.mit.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Injectivity of existT
Date: Fri, 14 Feb 2020 15:01:33 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
Ironport-phdr: 9a23:akPC0R/pSp504v9uRHKM819IXTAuvvDOBiVQ1KB30ekcTK2v8tzYMVDF4r011RmVBNmdtKoP0rGM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCeybL9oLhi6sQrdutQYjId8N6081gbHrnxUdutZwm9lOUidlAvm6Meq+55j/SVQu/Y/+MNFTK73Yac2Q6FGATo/K2w669HluhfFTQuU+3sTSX4WnQZSAwjE9x71QJH8uTbnu+Vn2SmaOcr2Ta0oWTmn8qxmRgPkhDsBOjUk927Zl9FwjLlDoB2/uxN/34DaYIaQNPVkf6Pde84RSW5OU8tVUiBMBJ63YYkSAOobJetWspfzp1UOoxW9CwejCuzgxT1UiXLtx6I2z/4sHBva0AEuHd8DtmnfotXvNKcVVOC41LXFwijZYPNTxDzw9ojIchQgofGUR71wddDewlQoGgzfk1qfs4nlMC+O2+sRqGiU9etgVea1h24iqgFxviKjydkxhYnUn48YzE3P+yt+wIYwP9K4SUh7bMarEJtRqyGaN5Z2Tdg4T2FpvyY3zKANt52jfCUS1Zgr2R3SZ+aJfoSU+B7vSvydLSlliH55YL6zmQq+/Ei6xuHiSsW4zUxGojdBn9XWuH0ByRre4dWdRPRn5EeuwzOP2hjT6u5aJUA0krLWK5k8wr4smZoTtkXDHin5mEnvl6+Wal8r+vSy5Oj9frrmvYWTN45wig3kN6Qum9C/Df4mPQcTQmiX4eW81Lv98k3lWLhGk+M6n6rDvJ3UOcgXvLC1DxVL3oo+9xqzFzKm384ZnXkDIlJFYhWHj43xNl7UPf/3F/K/jEi3nTh33PDJJLzhApHXInjGkbfhYaxx5FBBxwou1dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zFQaZOyi2YYdQHG+BPVvZUuDMlT2hdJUOGsDu0IVTOjrkFSGWHYHbnq7WqkU7SoyCYbgCIbfAI2hnerSj2+AApRKazUeWRi3GnDyetDYCq5QOhLXGddol3k/bZbkU5UojEz8vxTzyr4hK+vIvCAUqMC7jYUn16jojRg3sAdMIYGd3mWKFDkmmX4USDg32q86ulB01l7F2rNxgvgeEN1Pof5FT1VibM+O/6lBE9n3Hzn5UJKMQVeiTM+hBGhsHNkqyt4KJUN8B5Ovgg2Rhic=

No, that is actually one of the top axioms assumed in Coq developments, and proofs on paper have shown it is truly independent of the underlying theory! For more, see Eqdep, where your property appears as inj_pairT2 (derived from a slightly more basic axiom).

On 2/14/20 2:56 PM, John Li wrote:

Hi,

I have a proof of the following statement which assumes injectivity of dependent equality:

forall (A : Type) P x y, existT P A x = existT P A y -> x = y.

Is it possible to prove this without using any extra assumptions?

Thanks,
John

[Coq-Club] Injectivity of existT, John Li, 02/14/2020
- Re: [Coq-Club] Injectivity of existT, Adam Chlipala, 02/14/2020
- Re: [Coq-Club] Injectivity of existT, Chris Dams, 02/14/2020
  - Re: [Coq-Club] Injectivity of existT, Cao Qinxiang, 02/15/2020