A few associativity and absorption lemmas for `word.and`, `word.or`, and `word.xor`

mit-plv / coqutil

Coq library for tactics, basic definitions, sets, maps

MIT License

42 stars 24 forks source link

A few associativity and absorption lemmas for `word.and`, `word.or`, and `word.xor` #118

Closed vfukala closed 3 months ago

vfukala commented 3 months ago

word.or_assoc, word.or_0_l, and word.or_0_r are used in the crit-bit tree study in LiveVerif. I also added word.and_assoc and word.xor_assoc for completeness.