coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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, 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
- Re: [Coq-Club] injectivity of constructors, Jay Kruer, 12/14/2018
- [Coq-Club] compound coercion, richard Dapoigny, 12/16/2018
Archive powered by MHonArc 2.6.18.