search

mit-plv / coqutil

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

hooking `word` into `lia` #56

Open JasonGross opened 2 years ago

JasonGross commented 2 years ago

Should https://github.com/mit-plv/bedrock2/blob/master/bedrock2/src/bedrock2/ZnWords.v be adapted to hook into the zify mechanism a la https://github.com/coq/coq/blob/master/theories/micromega/ZifyUint63.v and be integrated into coqutil?

samuelgruetter commented 2 years ago

Migrating ZnWords to coqutil would be ok with me.

Since ZnWords is supposed to work for every word n if n is a concrete constant, we would need parameterized zify typeclass instances, and the last time I tried to do that (not for ZnWords, but for LittleEndian), Frédéric Besson said

Don't expect zify to work with parameterized instances. Some error checking is missing but the error message should be something like "Dependent types are not allowed". This is a strong restriction of the implementation that is hardwired very deep. Sorry.

Maaaybe we could duplicate the Add Zify ... commands for each word size of interest, but what if the word instance is a section variable? Use Load? Not sure if that's worth the trouble at the moment.