Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] injectivity of constructors

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of constructors


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

https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.f-equal

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



Archive powered by MHonArc 2.6.18.

Top of Page