coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jay Kruer <kruerj AT reed.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] injectivity of constructors
- Date: Thu, 13 Dec 2018 23:29:41 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kruerj AT reed.edu; spf=Pass smtp.mailfrom=kruerj AT reed.edu; spf=None smtp.helo=postmaster AT mail-qk1-f172.google.com
- Ironport-phdr: 9a23:VxtEjB+yIOp9Bv9uRHKM819IXTAuvvDOBiVQ1KB52ukcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/0hykIODE37W/ZisJugq1ZoxyvoAdyw5LNYIGQKPZ+fr/RcNEcSGFcXshRTStBAoakYoULFeUAPftToYznp1sTsxS+HxSnCeTsyj9Sm3/5w7c60+Y6HAHcwgMvAc8BvG7Ko9roKacfSOa4x7TLwzXbd/5axyvx5YzSfh0iofyAR6x8fdTPxUU1Cg/IjEucpZT4Mz6WzOgAvXSX4/BkWO+hkWIrtgV8rz6yzck2kIbJnJgaylXc+CV53ok1Idq4RVZ+YdG+EZtQsziWN5J1Qs8/Wm1otjs2x78YtZKhcygKz5MnxxHba/OZaYSH/hXjVOOJLTd5gnJqZq6/ig6s/US8zuDwTMq53VZQoiZbjNXAqGoB2wHR58SZUvd9+12u2TeL1wDd8OFEJkU0mLLYK547374/iIATsUbYEy/shkr5krKZel869ee19uTreq/mqYOEN49olgH+NbwjldC4AeQhKwQBQ2yb+fmn27D45k34QLBKjuUsnaXDsZDaI94bpq+jDANP3IYj8UX3MzDz29MB2HIDMVhteRSdjoGvNUudDur/CKKdikXksy12yuqOar77H5jXLFDZnbrtO7tx9hgPm0II0dlD6scMWfk6K/XpVxqp7Y2KPloCKwWxht3fJpB434IaV3iIB/bBYrnfvFPO6+4ycbDVON0l/Q3lIv1g3MbAyGcjkAZFL7Ok0JdRZXylTKw/fhepJEH0i9JEKl8k+wozSOuw1g+HWD9XIm+xBucyv25hTo2hCojHS8amh7nThCo=
As others have suggested, f_equal works for this. In case you or any others
were curious, this can also be done pretty neatly with SSReflect’s congr
tactic:
Goal forall (a b c d: nat), a = c /\ b = d -> (a, b) = (c, d).
move=> a b c d Heq.
congr (_,_); apply Heq.
Qed.
Cheers,
- Jay
> On Dec 13, 2018, at 7:29 PM, Jeremy Dawson
> <Jeremy.Dawson AT anu.edu.au>
> wrote:
>
>
> Hi,
>
> Given a goal (a,b) = (c,d),
> how to I get from that to goals a=c and b=d?
>
> (also, for constructors generally).
>
> So far as I can see both discriminate and inversion are useful when the
> equality is in the hypotheses but how about when it is in the goal?
>
> Thanks
>
> Jeremy
- Re: [Coq-Club] injectivity of constructors, (continued)
- Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jeremy Dawson, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Dominique Larchey-Wendling, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Pierre Courtieu, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Elazar, 12/14/2018
- RE: [Coq-Club] injectivity of constructors, Jason -Zhong Sheng- Hu, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Pierre Courtieu, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jeremy Dawson, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jay Kruer, 12/14/2018
- [Coq-Club] compound coercion, richard Dapoigny, 12/16/2018
Archive powered by MHonArc 2.6.18.