From 41ad5dec719bf51124ff72057f8b26f7e96c33d5 Mon Sep 17 00:00:00 2001
From: Johannes Hostert <jhostert@ethz.ch>
Date: Thu, 14 Nov 2024 23:20:56 +0100
Subject: [PATCH] implement MR feedback

---
 theories/tree_borrows/read_read_reorder/equivalence_def.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/tree_borrows/read_read_reorder/equivalence_def.v b/theories/tree_borrows/read_read_reorder/equivalence_def.v
index d0e6c122..8a3b266d 100644
--- a/theories/tree_borrows/read_read_reorder/equivalence_def.v
+++ b/theories/tree_borrows/read_read_reorder/equivalence_def.v
@@ -10,7 +10,8 @@ Fixpoint nsteps P (e : expr) σ e'' σ'' n : Prop := match n with
   0 => e = e'' ∧ σ = σ''
 | S n => ∃ e' σ', prim_step P e σ e' σ' nil ∧ nsteps P e' σ' e'' σ'' n end.
 
-(* This says that after n steps, any state reachable in from e_1 in σ must be reachable from e_2 in σ *)
+(* This says that after n steps, any state reachable in from e_1 in σ must be reachable from e_2 in σ.
+   This is just a helper definition used for [eventually_equal]; on its own it is not very meaningful. *)
 Definition identical_states_after P e1 e2 σ n := 
   ∀ e' σ', nsteps P e1 σ e' σ' n → nsteps P e2 σ e' σ' n.
 
@@ -23,9 +24,8 @@ Inductive no_termination_within P : expr → state → nat → Prop :=
     (∀ e' σ', prim_step P e σ e' σ' nil → no_termination_within P e' σ' n) →
     no_termination_within P e σ (S n).
 
-(* So, two programs are eventually equal if they are equal after n steps, for some n.
-   This only holds as long as they don't terminate within these n steps.
-   If either program has UB within these n steps, the other program must do so as well. *)
+(* Two programs are eventually equal if they both do not terminate with n steps,
+  and after n steps, they are equal. *)
 Definition eventually_equal P e1 e2 :=
   ∃ n, ∀ σ, state_wf σ →
     no_termination_within P e1 σ n ∧
-- 
GitLab