From 410a14dee7f6d123706127ba42c7f5bc5efbcaa0 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 15 Jan 2021 15:55:41 +0100
Subject: [PATCH] Simplify some proofs.

---
 theories/prelude/lang_facts.v | 32 +++++++++++---------------------
 1 file changed, 11 insertions(+), 21 deletions(-)

diff --git a/theories/prelude/lang_facts.v b/theories/prelude/lang_facts.v
index 7322a84..4c4bbd6 100644
--- a/theories/prelude/lang_facts.v
+++ b/theories/prelude/lang_facts.v
@@ -70,16 +70,17 @@ Section facts.
   Qed.
 
   Lemma nice_ctx_lemma' K tp1 tp2 e ρ1 ρ2 v `{!LanguageCtx K} :
-    rtc erased_step ρ1 ρ2 →
     ρ1.1 = (K e) :: tp1 →
     ρ2.1 = of_val v :: tp2 →
+    rtc erased_step ρ1 ρ2 →
     ∃ tp2' tp3' σ' σ'' w,
       rtc erased_step (e :: tp1, ρ1.2) (of_val w :: tp2', σ') ∧
       rtc erased_step (K (of_val w) :: tp2', σ') (of_val v :: tp3', σ'').
   Proof.
-    intros Hsteps.
-    revert tp1 e.
-    induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH]; intros tp1 e Hρ1 Hρ2.
+    intros Heq1 Heq2 Hsteps.
+    revert tp1 e Heq1 Heq2.
+    induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH];
+      intros tp1 e Hρ1 Hρ2.
     { destruct (to_val e) as [w|] eqn:He.
       - apply of_to_val in He as <-.
         destruct ρ as [ρ1 ρ2]. simplify_eq/=.
@@ -118,12 +119,7 @@ Section facts.
     ∃ tp2' tp3' σ' σ'' w,
       rtc erased_step (e :: tp1, σ1) (of_val w :: tp2', σ') ∧
       rtc erased_step (K (of_val w) :: tp2', σ') (of_val v :: tp3', σ'').
-  Proof.
-    pose (ρ1:=((K e) :: tp1, σ1)).
-    pose (ρ2:=(of_val v :: tp2, σ2)).
-    fold ρ1 ρ2. intros Hρ.
-    change σ1 with ρ1.2. eapply nice_ctx_lemma'; eauto.
-  Qed.
+  Proof. by eapply nice_ctx_lemma'. Qed.
 
   Lemma nice_ctx_lemma_1 K tp1 tp2 e σ1 σ2 v `{!LanguageCtx K} :
     rtc erased_step (K e :: tp1, σ1) (of_val v :: tp2, σ2) →
@@ -145,14 +141,15 @@ Section facts.
     end.
 
   Lemma pure_exec_inversion_lemma' tp1 tp2 e1 e2 ρ1 ρ2 v ϕ :
+    ρ1.1 = e1 :: tp1 →
+    ρ2.1 = of_val v :: tp2 →
     PureExec ϕ 1 e1 e2 →
     ϕ →
     rtc erased_step ρ1 ρ2 →
-    ρ1.1 = e1 :: tp1 →
-    ρ2.1 = of_val v :: tp2 →
     rtc erased_step (e2 :: tp1, ρ1.2) ρ2.
   Proof.
-    intros Hpure HÏ• Hsteps. revert tp1. specialize (Hpure HÏ•).
+    intros Heq1 Heq2 Hpure HÏ• Hsteps.
+    revert tp1 Heq1 Heq2. specialize (Hpure HÏ•).
     apply nsteps_once_inv in Hpure.
     revert e1 Hpure.
     induction Hsteps as [ρ|ρ1 ρ2 ρ3 Hstep Hsteps IH]; intros e1 Hpure tp1 Hρ1 Hρ2.
@@ -181,13 +178,7 @@ Section facts.
     ϕ →
     rtc erased_step (e1 :: tp1, σ1) (of_val v :: tp2, σ2) →
     rtc erased_step (e2 :: tp1, σ1) (of_val v :: tp2, σ2).
-  Proof.
-    intros ? ? ?.
-    pose (ρ1 := (e1 :: tp1, σ1)).
-    pose (ρ2 := (of_val v :: tp2, σ2)).
-    fold ρ1 ρ2. change σ1 with ρ1.2.
-    eapply pure_exec_inversion_lemma'; eauto.
-  Qed.
+  Proof. by eapply pure_exec_inversion_lemma'. Qed.
 
   Lemma pure_exec_erased_step tp e1 e2 σ ϕ :
     PureExec ϕ 1 e1 e2 →
@@ -203,5 +194,4 @@ Section facts.
     naive_solver.
   Qed.
 
-
 End facts.
-- 
GitLab