From e77bc88aad03bd28dfdea49ce7ed1318f693a9ad Mon Sep 17 00:00:00 2001
From: adelaett <90894311+adelaett@users.noreply.github.com>
Date: Mon, 8 Apr 2024 11:18:54 +0200
Subject: [PATCH] proof simplification

---
 theories/trans.v | 27 ++++-----------------------
 1 file changed, 4 insertions(+), 23 deletions(-)

diff --git a/theories/trans.v b/theories/trans.v
index f482990..5f29a5c 100644
--- a/theories/trans.v
+++ b/theories/trans.v
@@ -415,25 +415,17 @@ Theorem correction_continuations:
       (trans_state s2) target.
 Proof.
 
-  Local Ltac step' := (
+  Local Ltac step' := ( idtac
     (* This tatic try to advance the computation on the right or on the left of the diagram. *)
-    try (eapply step_left; [solve
-      (* generic case *)
-      [ econstructor; simpl; eauto using List.map_nth_error
-      (* for contextual error cases *)
-      | econstructor; repeat intro; tryfalse
-    ]|])
-    ; try (eapply step_right; [solve
-      [ econstructor; simpl; eauto using List.map_nth_error
-      | econstructor; repeat intro; tryfalse
-    ]|])
+    ; try (eapply step_left; [solve [ econstructor; simpl; eauto using List.map_nth_error, trans_value_op_correct]|])
+    ; try (eapply step_right; [solve [ econstructor; simpl; eauto using List.map_nth_error, trans_value_op_correct]|])
   ).
 
   intros s1 s2 Hsred.
   induction Hsred;
     try induction phi;
     try induction o;
-    intros; unpack.
+    intros; unpack; tryfalse.
 
   all:
     try solve [
@@ -441,15 +433,4 @@ Proof.
       try eapply diagram_finish;
       eauto
     ].
-  
-  (* Only two cases are left. *)
-  { tryfalse. }
-  { (* requires operator translation correction *)
-    eexists; split; asimpl; [|eapply star_refl].
-    eapply star_step.
-    { econstructor.
-      eapply trans_value_op_correct; eauto.
-    }
-    eapply star_refl.
-  }
 Qed.