Stream: Coq users

Topic: listsEqual tactic

view this post on Zulip 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:

Now, as I had zero idea how to write a tactic before reading the tutorial, I'm looking for feedback. Thanks!

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Alexander Gryzlov (Jan 19 2023 at 15:10):

Overloaded lemmas can also be set up to do reification, e.g.

Last updated: Oct 04 2023 at 23:01 UTC