Huỳnh Trần Khanh (Jan 19 2023 at 10:41): Huỳnh Trần Khanh (Jan 19 2023 at 10:41):I find that I have to solve many goals involving two lists being equal. These proofs are simple yet so infuriating. So today I followed the tutorial in Certified Programming with Dependent Types to make a new tactic for this. Here's the code: https://github.com/huynhtrankhanh/coqcp/blob/fe27e9a412867984d058c18e683cff5c9486a372/theories/ListsEqual.v
Now, as I had zero idea how to write a tactic before reading the tutorial, I'm looking for feedback. Thanks!
Anton Golov (they/them) (Jan 19 2023 at 13:34):Cool approach with translating an expression into a value describing it! I think another approach that could do the job here would be to register some lemmas with autorewrite and then hit it with that.
Paolo Giarrusso (Jan 19 2023 at 14:25):autorewrite is simpler to setup and more extensible, but can be slower because of repeated traversals.
But typeclass-based reification / normalization is more extensible and can be more performant; set_solver in stdpp is a nice "production" example.
Karl Palmskog (Jan 19 2023 at 14:32):if we remember Jason Gross' PhD thesis, my understanding of the gist is that only carefully tuned reflective automation has a chance to perform at large scale. I think that would rule out the TC stuff a lot of the time?
Karl Palmskog (Jan 19 2023 at 14:44):but if we are doing stuff at the non-large-scale with lists and reasoning mostly about equality, AAC Tactics might be one way to do it minimal boilerplate.
Alexander Gryzlov (Jan 19 2023 at 15:10):Overloaded lemmas can also be set up to do reification, e.g. https://github.com/imdea-software/fcsl-pcm/blob/master/pcm/autopcm.v
Last updated: Oct 04 2023 at 23:01 UTC