From 236fb32e006e2d5d450506c288ca342f120f7491 Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:35:20 +0200
Subject: [PATCH] correct_store_buffer: simplify proofs

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
 src/correct_store_buffer.v | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index d337d3d..921df5c 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -100,13 +100,10 @@ Section can_advance.
     destruct e1.
     unfold cycle_elt.
     destruct s, n0.
-    - destruct (ready _ _ _ && free _ _ _ _);
-        destruct s, o;
-        reflexivity.
-    - destruct s;
-        simpl;
-        rewrite Nat.leb_le;
-        lia.
+    - now destruct (ready _ _ _ && free _ _ _ _), s, o.
+    - simpl.
+      rewrite stage_beq_eq_true, Nat.leb_le.
+      lia.
   Qed.
 End can_advance.
 
@@ -162,8 +159,7 @@ Section constrained.
 
     unfold lsuFree, get_instr_in_stage.
     rewrite (not_existsb_means_cannot_find _ _ t');
-      destruct opc;
-      reflexivity || exact HconstT'.
+      now destruct opc.
   Qed.
 
   (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
@@ -187,8 +183,7 @@ Section constrained.
 
     unfold luFree, get_instr_in_stage.
     rewrite (not_existsb_means_cannot_find _ _ t').
-    - rewrite HconstT'2.
-      reflexivity.
+    - now rewrite HconstT'2.
     - exact HconstT'.
   Qed.
 
@@ -204,8 +199,6 @@ Section constrained.
     constraint_delve He.
 
     unfold suFree, get_instr_in_stage.
-    rewrite (not_existsb_means_cannot_find _ _ t').
-    - reflexivity.
-    - exact HconstT'.
+    now rewrite (not_existsb_means_cannot_find _ _ t').
   Qed.
 End constrained.
-- 
GitLab