coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] injectivity of constructors
- Date: Fri, 14 Dec 2018 01:50:30 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f42.google.com
- Ironport-phdr: 9a23:SrFodRG/vG7h2xuS+/DBVZ1GYnF86YWxBRYc798ds5kLTJ78oc2wAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAfAAPelGtYn9vUUBpgagCAmrGePv0CNIhn7o0q0nzu8sFhnG3A0+ENIUqnTbss/5O7sVUeCo1qnI0TTDYO1L2Trm54jIdwouofCIXb5qbcXRzkwvGhrDg16Np4LlODaV2f4Ms2id9+dgVOSvi3Qmqw5ruDSvyN0sh4/UjYwW0lDJ7Tt1zJoxKNGiS0N2YcSoHIVNuy2GLYd7Td0uTmd1sygg0LIGo4S0fC0SxZQn2RHfb/uHfpCN4h35VeaRJS50hHV5eL6inhqy/0etxvPmWsm711ZKqSVFkt3SuXwXyxPT7c2HRuN8/kenxzmPyxje5v9YLU0wj6bWKJ4szqQumpYOrUjPBCD7lFvugK+TbEok++yo6+r9YrXho5+RL5d0igDgPaQ0gMywH/40PRQJX2iG4+S8yLzj8lPkQLhRgf02l7PWsJHeJcgBuqG5BApV3p456xmjFzemzMgYnX4fIV1ZfxKHlpHlNE3KIPDlFviymE+skTdux/DeJLLtGJTNLn7ZkLfgZ7lx8UBcyBBghexYsplTE/QKJO/5ck73rt3RSBEjYCKuxOOyMNRwzJkTEUmIH7WFMa7P+QuQ5+81OeTKb4gIoir8JuUN6PvnjHt/klgYK/r6laALYWy1S6w1a36SZmDh149YQDU6+zEmRemvs2WsFDtaZnK8RaU5v2hpB4evDIOFTYeo0uXYgHWLW6ZOb2UDMWiiVG/yftzdCfgJYSOWZMRml25cDOXze8oazRir8TTC5f9nI+7ToHBKsJvi0J1y+7SWm01oszNzCMuZ3ieGSGQmxm4=
f_equal is the tactic you are looking for.
Bests
Pierre
Le ven. 14 déc. 2018 à 01:30, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> a écrit :
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
- [Coq-Club] injectivity of constructors, Jeremy Dawson, 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, 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
Archive powered by MHonArc 2.6.18.