search

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps
MIT License
41 stars 24 forks source link

New set lemmas #28

Closed jadephilipoom closed 4 years ago

jadephilipoom commented 4 years ago

Similar to #27, this PR upstreams generalizable facts about sets that I needed while developing fiat-crypto's bedrock2 backend.

Most lemmas are pretty basic; probably the more controversial elements added are a) RelationClasses and Proper instances for all the set operations and b) some lemmas that rely on decidable equality of set elements.

jadephilipoom commented 4 years ago

I did try to use set_solver_generic, but didn't meet much success, I think because most of my goals really weren't about sets. For the most part, they had sets as subterms and I needed to manipulate or rewrite them in small ways, so I didn't want to do whole-goal simplifications like destruct_products and intuition, which are included in set_solver_generic. I found it also easier to understand what was going on in my goals when I left the set definitions folded.

samuelgruetter commented 4 years ago

Makes sense, so I guess you'd have to do replace large_set_expression_1 with another_slightly_different_set_expression by set_solver_generic T, whereas your lemmas just allow you do to rewrite some_set_lemma, which is nicer.