correct_sb: cleanup proofs

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

src/correct_store_buffer.v

@@ -110,6 +110,7 @@ Section constrained.
   Hypothesis Hl' : List.length tpost' = List.length tpost.
   Hypothesis Htc : tc = cycle sbState t.
   Hypothesis Htc' : tc' = cycle sbState' t'.
+  Hypothesis HconstT : is_constrained e t sbState = true.
 
   (* Delve into tc, tc', cycle, cycle_elt, etc.
    * Pretty specific to these constraints, do not use it outside this section. *)
@@ -136,12 +137,11 @@ Section constrained.
 
   (* If a constrained Sp can advance, an unconstrained Sp can advance. *)
   Theorem constrained_sp_can_advance_unconstrained_too :
-    e = (opc, (Sp, 0)) ->
     (* t is constrained, t' is unconstrained *)
-    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+    e = (opc, (Sp, 0)) -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (opc, (Lsu, 0)) -> List.nth_error tc' i = Some (opc, (Lsu, 0)).
   Proof.
-    intros He HconstT HconstT'.
+    intros He HconstT'.
     rewrite He in HconstT'.
 
     constraint_delve He.
@@ -155,12 +155,11 @@ Section constrained.
   (* If a constrained Lsu can advance, an unconstrained Lsu can advance. *)
   (* Load version *)
   Theorem constrained_lsu_load_advance_unconstrained_too :
-    e = (Load, (Lsu, 0)) ->
     (* t is constrained, t' is unconstrained *)
-    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+    e = (Load, (Lsu, 0)) -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (Load, (Lu, 0)) -> List.nth_error tc' i = Some (Load, (Lu, 0)).
   Proof.
-    intros He Hconst.
+    intro He.
 
     rewrite He.
     unfold is_constrained.
@@ -181,12 +180,11 @@ Section constrained.
 
   (* Store version *)
   Theorem constrained_lsu_store_advance_unconstrained_too :
-    e = (Store, (Lsu, 0)) ->
     (* t is constrained, t' is unconstrained *)
-    is_constrained e t sbState = true -> is_constrained e t' sbState' = false ->
+    e = (Store, (Lsu, 0)) -> is_constrained e t' sbState' = false ->
     List.nth_error tc i = Some (Store, (Su, 0)) -> List.nth_error tc' i = Some (Store, (Su, 0)).
   Proof.
-    intros He HconstT HconstT'.
+    intros He HconstT'.
     rewrite He in HconstT'.
 
     constraint_delve He.