vafeiadis / hahn

Hahn: A Coq library
MIT License
29 stars 15 forks source link

Lemmas about symmetric closure and symmetry of relations #18

Closed eupp closed 4 years ago

eupp commented 4 years ago
  1. Definitions of symmetric clos_sym and reflexive-symmetric clos_refl_sym closures.
  2. Notation for them.
    • "a ^⋈" notation for symmetric closure
    • "a ^⋈?" notation for reflexive-symmetric closure
  3. Some useful lemmas about (reflexive-)symmetric closure.
  4. Some useful lemmas about symmetry of relations.

    It seems that there is no standard notation for symmetric closure in the literature. Thus the choice of notation is debatable. A few alternatives considered by me.

    "a ^=" notation for reflexive-symmetric closure from WeakestMO original paper. The "a ^=" notation is also often used for reflexive closure and thus it is undesirable (might lead to confusion).

    "a ^s" and "a ^s?" notation. It seems that this notation was used previously in some literature (link). However, I personally like \bowtie ^⋈ notation more.