Skip to content

Various improvements to `Permutation` lemmas and instances

Robbert Krebbers requested to merge robbert/Permutation into master

Various changes to Permutation lemmas:

  • Rename Permutation_nilPermutation_nil_r and and Permutation_singletonPermutation_singleton_r.
  • Add lemmas Permutation_nil_l and Permutation_singleton_l.
  • Add new instance cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k)..
  • Add lemma Permutation_cross_split.
  • Make lemma elem_of_Permutation a biimplication

Also, I made the following changes that should not affect users:

  • Name Proper and Inj instances for Permutation as operation_Permutation_{Proper,inj,inj_l,inj_r}
  • Remove Proper instances for :: and ++ that are already supplied by the std lib.
Edited by Robbert Krebbers

Merge request reports