correct_store_buffer: simplify proofs

Signed-off-by: Alban Gruin <alban.gruin@irit.fr>

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.