Skip to content

GitLab

Prove more equivalences for closure operators on relations.

Merged Robbert Krebbers requested to merge robbert/relations_alt into master

Add and extend equivalences between closure operators:

  • Add ↔ lemmas that relate rtc, tc, nsteps, and bsteps.
  • Rename → lemmas rtc_nsteps → rtc_nsteps_1, nsteps_rtc → rtc_nsteps_2, rtc_bsteps → rtc_bsteps_1, and bsteps_rtc → rtc_bsteps_2.
  • Add lemmas that relate rtc, tc, nsteps, and bsteps to path representations as lists.

The _list lemmas were proposed by @jules and he provided an initial proof specific to rtc.

Edited by Robbert Krebbers