From 5abb67e05e7e70f8846794c74f55a8966e9d02cd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Jun 2019 12:09:20 +0200
Subject: [PATCH] More automated proof of `erased_steps_nsteps`.

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

diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 9efd4250d..e6f6e0f33 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -119,13 +119,12 @@ Section language.
   (** [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 ↔
-    ∃ n κs, nsteps n ρ1 κs ρ2.
+    rtc erased_step ρ1 ρ2 ↔ ∃ n κs, nsteps n ρ1 κs ρ2.
   Proof.
     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.
+    - induction 1; firstorder eauto. (* FIXME: [naive_solver eauto] should be able to handle this *)
+    - intros (n & κs & Hsteps). unfold erased_step.
+      induction Hsteps; eauto using rtc_refl, rtc_l.
   Qed.
 
   Lemma of_to_val_flip v e : of_val v = e → to_val e = Some v.
-- 
GitLab