coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of constructors

From: Jasper Hugunin <jasperh AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] injectivity of constructors
Date: Thu, 13 Dec 2018 19:07:38 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasperh AT cs.washington.edu; spf=None smtp.mailfrom=jasperh AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-ot1-f53.google.com
Ironport-phdr: 9a23:UdTqURN6t8zt4wKXIfIl6mtUPXoX/o7sNwtQ0KIMzox0LfnzrarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgIOT428mHZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYoULFeUBJv5YoJfnp1ATrxW+GAasBP7pyj9JgH/9wKo30+Y7HgHdxAwvAcgOsHTPodrpL6ceS+60w7PTzTXDbvNW3zj96JTPchAnu/2DQ69/cdfIxEQpCgjLgFKQqYn/MDOU0OQAq2mb7+x6VeKukWErsQ9xoiKpy8wxiYfJnpoYxk7Y+Sh92oo4Jt21RFRlbdK5DJdcrSGXOoVwT8g/WW9nojw6xacDuZOjfCgF1pAnxxnHZvyCaYeI4xbjWP+WITdkmX5pYby/iha8/ES6xe38Uc600FlOriVbiNXDqncN1xnL5siGTPty4Fuh1C6R2wzP7uxIO0M5mKrBJ5I/37I8ioAfvETNEyPunUX5lq6WdkEq+uiy7OTnZ63rpp2GOI9vkgHxLL4umsykDOskKQgCRWaa9v6n1L3j/E35RrpKjuExkqnfqpzVO9kUprOhDw9Pzokj8wq/Dyuh0NkAgXYHK0tFdAubgIjtJlHBO+v1Dey/glSpiDdk3erKPrznApXXL3jMiq3tfbhn6x0U9A1mxtdGoplQF7spIfTpW0a3usaLIAU+NlmWyv3/Bc819p4RRGSOBOfNMqrJqVKS5sokOK+TbZQVuTDyN/8jofPikClqyhcmYaC10M5POziDFfN8LhDBOCu+spI6CW4P+zEGYqnvgVyGXyRUYi/jDaknoC4yE4KnC4jfQYbrjbCcjn/iQs9mI1teA1XJKk/GMp2eUq5dOimJZNBoiTwFU7e9TIln2B2z5lejluhXa9HM8yhdjqrNkdh44+qJyEM3/D1wSsOBiiSDEjoykWQPSDs7mqt4pB4lxw==

`injection` seems to fit your description, see https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.injection.

- Jasper Hugunin

On Thu, Dec 13, 2018 at 4:54 PM Lily Chung <ikdc AT mit.edu> wrote:

That follows from general properties of equality, and has nothing to do with constructors. Try f_equal.

[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, Jay Kruer, 12/14/2018
  - [Coq-Club] compound coercion, richard Dapoigny, 12/16/2018