coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewriting in an equality without eq_ind_r / transport

From: Samuel Gruetter <gruetter AT mit.edu>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] rewriting in an equality without eq_ind_r / transport
Date: Wed, 13 Nov 2019 18:33:55 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gruetter AT mit.edu; spf=Pass smtp.mailfrom=gruetter AT mit.edu; spf=None smtp.helo=postmaster AT outgoing-exchange-7.mit.edu
Ironport-phdr: 9a23:5MCvnxaMm3EsozPs56vGH8P/LSx+4OfEezUN459isYplN5qZr8y9bnLW6fgltlLVR4KTs6sC17ON9fm7ACdZuMjJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/MusQYnIduJbs9xgbIr3BVZ+lY2GRkKE6JkR3h/Mmw5plj8ypRu/Il6cFNVLjxcro7Q7JFEjkoKng568L3uxbNSwuP/WYcXX4NkhVUGQjF7Qr1UYn3vyDnq+dywiiaPcnxTbApRTSv6rpgRRH0hCsbMTMy7WfagdFygq1GuhKsvxxxzZDJboGJOvRwfa3dctEbRWVdUclcTDZODp+mYoYVE+YNIeRVoo/grFUOtxu+AgysCfvyxDBSg3/2wLM10+A8Gg/HxgwgAswBsGjIrNrrLqcZTOe4zKbSzTXecfxWxSv955bSch06pPGMXK5wfdDPxkYyCgPIl1OdopHrMTOS0+QCqWmb7+x4WOKgim4ntwFxoiW0ycs2lobJgYcVx1bZ/it62IY4PcC0RU1hbdOgCpdcqSKXO5F2T84hW21kpTg2x74ctZO1YCQG0okrywLFZ/CabYSF4wrvWPuSLDtigH9pYr2yiwyv/US9xeDxUNS/3kxQoSpfiNbMs2gA1xzN5ciDTftw5kCh2SuT1wDc7eFEIEY0laXCJ5E/zb8/ipoTvl7FHi/5hkr6la2bel8h+uip9+TreKvpqYKBN4NsiwH+NLohmtCnDOglMQUCRWyW9f6i2LDg50H0QLZHguUzkqbDsZDaIcobprS+Aw9Qyosj5Ay/Dyq439QEgXkIMkhFdQmCj4joJ1HCOu73Auqig1i0ijdk2+jGPqH9ApXKNnXMjLDhfa9k50FAzAoz0MtQ6olPCrABJfLzQlX+uMbZDh8/KQy0wvzoBM9z1oMECiqzBfrTO6TL9FSM++gHIu+WZYZTtiy3Y6wu4Oerhnskk3cce7Oo1N0ZcibrMO5hJhCiaH/xj9NJPn0XsxYiQfai3FKYTDNPe3uod6c9+nc2BJ/wXtSLfZyknLHUhHTzJZZRfG0TUgndQ0etTJ2NXrI3UAzXJ8ZgljIeUr3wGYogyVejuBKokuM7fNqRwTURsNfY7PYw//faxEM39CAyAsiAgTnUEjNE21gQTjpz55hR5ExwzlDZgPp/nuBXEt1V6LZEQgw6PJjTwqklTdXzRkTMcsrbEFs=

… but in general, I'd stay away from evar-based strategies.

Right, I tried unify after sending my last message, and it doesn't work

well.  For example, the term 4 * (m + (3 * n) *does* unify against

?x + ?y, since it expands to a sum.  But I don't want to rewrite

something that isn't explicitly written as a sum.  So unify is out.

I'd also try to not use evars if possible, but in case you do need to address the above problem, you'd have to do a "syntactic unify". I don't think Coq provides this feature out-of-the box, but we implemented (a restricted form of) it in Ltac here: https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Tactics/syntactic_unify.v

Re: [Coq-Club] rewriting in an equality without eq_ind_r / transport, (continued)