From 326a6f8abea009d47e60737898a58d71d12f3299 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 7 Jun 2019 11:54:13 +0200
Subject: [PATCH] show that erased_steps_ntesps is an equivalence

---
 theories/program_logic/language.v | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 162ac66ba..9efd4250d 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -116,11 +116,16 @@ Section language.
 
   Definition erased_step (ρ1 ρ2 : cfg Λ) := ∃ κ, step ρ1 κ ρ2.
 
+  (** [rtc erased_step] and [nsteps] encode the same thing, just packaged
+      in a different way. *)
   Lemma erased_steps_nsteps ρ1 ρ2 :
-    rtc erased_step ρ1 ρ2 →
+    rtc erased_step ρ1 ρ2 ↔
     ∃ n κs, nsteps n ρ1 κs ρ2.
   Proof.
-    induction 1; firstorder; eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
+    split.
+    - induction 1; firstorder; eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
+    - intros (n & κs & Hsteps). induction Hsteps; first done. econstructor; last done.
+      eexists. done.
   Qed.
 
   Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
-- 
GitLab