Skip to content

Confluent relations

Robbert Krebbers requested to merge robbert/relations into master

This MR adds:

  • The symmetric and reflexive/transitive/symmetric closure of a relation
  • Different notions of confluence: diamond property, confluence, local confluence (following the naming conventions in https://www21.in.tum.de/~nipkow/TRaAT/)
  • Standard properties such as diamond ⊢ confluence ⊢ local confluence, the Church-Rosser property, Newman's lemma

As part of this MR, I removed the hint database ars. The name made no sense and it was not used anywhere to my knowledge. If it was used anywhere, it would be very unreliable as it contained hints like rtc_trans that would generally lead to loops.

Merge request reports