coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] injectivity of constructors

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] injectivity of constructors
Date: Fri, 14 Dec 2018 00:29:55 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:v/FjRBFevvSyDSTGpAYhmp1GYnF86YWxBRYc798ds5kLTJ7zociwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoByjqBx+34Hab46aOeFifqPEZ94WWXZNUtpRWiFHH4iyb5EPD+0EPetAq4fyuUEOogW7BQisGejhxCVHh3Ht3a091eQqDAbL0gg+ENIUrnvUqdX0OL0cX++vwqjI1jLDb/VN1Djn7ojIbwotru+RUrJta8be01QvGhrDg16NqoLlJyuY2+sRv2SB8uZsSeCih3Q6pwx/ozWj3MMhh43Rio8azl3I7zh1zYI1KNGiRkN2YsSoHIVIuyGUKYR7Qd8uTmRttSs5yrALvYC0cS0Xx5kp3BHSavmKfoyH7x/tWuucJDN1iXJkdb2lgRu57FKuxffmVsau1VZHtipFncfItnAKzxHe9saIROZh8ku8wDqB0A/d5vxdLUAzjqXUNYQtwrktlpoPqkvDGTL2mEPrg6OMbkUk4O+o6/j5bbr6up+cNoh0igfkPqQph8y/HeA4Mg8JX2iY4+izyLrj/UjhTLVLiP05jLXZvYjVKMgHvKK1HhNZ34Q55xqiATqr0c4UkH0DIV5dfRKIlYnpO1XAIPDiCve/hkyhnjN1yPDcILLhB5XMImLNnrj7c7d98ElcyAwowN9F4ZJUF6sNL+zuVU/srtDXFAI5PxSuw+n7ENV9yp8eWWWXD6CFN6PSqEaE6f4rI+mRf4AYoy39Kvgg5/72l3A1g14dfa+z3ZsWcn+0BPpmI1/KKUbr150KFn5PtQ4jRsTrjkeDWHhdfTz6C6k7/3QwDJ+sJYbFXIGkxrKbinSVBJpTM0JLEF2JAD/EfpqfXPFEPACfOMJkg3ooXKe6TIkJ3Bez8gL21vxuM7yHqWUjqZv/2Y0ttKXonhYo+GksVpXP4yS2V2hx21gwaXoz1aF7r1Z6zw7Zg6F+nrpVGcEV7u4bC15mZ66Z9PRzDpXJYiyEZs2AEQz0S9O7Rzw9U5Q43o1WOhsvK5CZlhnGmhGSLfoVmriMWMNm25/nhyG0AuskjnHM2e8mkkUsRdZJOSu+nKlj+gPPBonP1UKEi6Ktcqda1ynIpj6O
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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