coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of constructors

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

[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