Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Injectivity of existT

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Injectivity of existT


Chronological Thread 
  • 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





Archive powered by MHonArc 2.6.18.

Top of Page