From 4598e77a9406d8040357c943a05dd1ab939932db Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Thu, 27 Jun 2024 01:56:05 +0200
Subject: Tidy up project

* Write README.md
* Add LICENSE
* Clean up some theorems and proofs
---
 relations.v | 19 ++++++++++++-------
 1 file changed, 12 insertions(+), 7 deletions(-)

(limited to 'relations.v')

diff --git a/relations.v b/relations.v
index 9bfb7e6..7523c96 100644
--- a/relations.v
+++ b/relations.v
@@ -1,10 +1,14 @@
+(** This files contains definitions for determinism, strong confluence,
+ * semi-confluence, the Church-Rosser property and proofs about relationships
+ * of these properties. We use definitions and proofs from 'Term Rewriting and
+ * All That' by Franz Baader and Tobias Nipkow (1998). *)
 From stdpp Require Import relations.
 
 Definition deterministic {A} (R : relation A) :=
   ∀ x y1 y2, R x y1 → R x y2 → y1 = y2.
 
-(* As in Baader and Nipkow (1998): *)
-(* y is a normal form of x if x -->* y and y is in normal form. *)
+(** Baader and Nipkow (1998), p. 9:
+ *   y is a normal form of x if x -->* y and y is in normal form. *)
 Definition is_nf_of `(R : relation A) x y := (rtc R x y) ∧ nf R y.
 
 (** The reflexive closure. *)
@@ -14,15 +18,15 @@ Inductive rc {A} (R : relation A) : relation A :=
 
 Hint Constructors rc : core.
 
-(* Baader and Nipkow, Definition 2.7.3. *)
+(** Baader and Nipkow, Definition 2.7.3. *)
 Definition strongly_confluent {A} (R : relation A) :=
   ∀ x y1 y2, R x y1 → R x y2 → ∃ z, rtc R y1 z ∧ rc R y2 z.
 
-(* Baader and Nipkow, Definition 2.1.4. *)
+(** Baader and Nipkow, Definition 2.1.4. *)
 Definition semi_confluent {A} (R : relation A) :=
   ∀ x y1 y2, R x y1 → rtc R x y2 → ∃ z, rtc R y1 z ∧ rtc R y2 z.
 
-(* Lemma 2.7.4 from Baader and Nipkow *)
+(** Lemma 2.7.4 from Baader and Nipkow *)
 Lemma strong__semi_confluence {A} (R : relation A) :
   strongly_confluent R → semi_confluent R.
 Proof.
@@ -47,11 +51,12 @@ Proof.
       by apply rtc_transitive with (y := y2).
 Qed.
 
-(* Copied from stdpp, originates from Baader and Nipkow (1998) *)
+(** Baader and Nipkow, Definition 2.1.3. 
+ * Copied from stdpp v1.10.0 (confluent_alt). *)
 Definition cr {A} (R : relation A) :=
   ∀ x y, rtsc R x y → ∃ z, rtc R x z ∧ rtc R y z.
 
-(* Part of Lemma 2.1.5 from Baader and Nipkow (1998) *)
+(** Part of Lemma 2.1.5 from Baader and Nipkow (1998) *)
 Lemma semi_confluence__cr {A} (R : relation A) :
   semi_confluent R → cr R.
 Proof.
-- 
cgit v1.2.3