From 613153f35d6b864d5a38071cc2e53f9f22af140b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Apr 2020 23:04:16 +0200
Subject: [PATCH] Intuition for decidability of `red` in `wn_sn`.

---
 theories/relations.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/relations.v b/theories/relations.v
index 80e6af26..fdadac43 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -280,6 +280,10 @@ Section properties.
   Lemma wn_step_rtc x y : wn R y → rtc R x y → wn R x.
   Proof. induction 2; eauto using wn_step. Qed.
 
+  (** The following theorem requires that [red R] is decidable. The intuition
+  for this requirement is that [wn R] is a very "positive" statement as it
+  points out a particular trace. In contrast, [sn R] just says "this also holds
+  for all successors", there is no "data"/"trace" there. *)
   Lemma sn_wn `{!∀ y, Decision (red R y)} x : sn R x → wn R x.
   Proof.
     induction 1 as [x _ IH]. destruct (decide (red R x)) as [[x' ?]|?].
-- 
GitLab