coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
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
Archive powered by MHonArc 2.6.18.