correct_store_buffer: rename lemmas for clarity

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

src/correct_store_buffer.v

@@ -235,7 +235,7 @@ Section monotonicity.
     - auto.
   Qed.
 
-  Lemma unmoved_can_advance :
+  Lemma unmoved_is_monotonic :
     forall n, e = (opc, (st, n)) -> e = e' ->
          compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
   Proof.
@@ -263,7 +263,7 @@ Section monotonicity.
 
   Variable st' : stage.
 
-  Lemma moved_no_lat_is_lower :
+  Lemma moved_no_lat_is_monotonic :
     e = (opc, (st, 0)) -> e' = (opc, (st', 0)) -> e <> e' ->
     state_leb (st, 0) (st', 0) = true ->
     compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
@@ -311,7 +311,7 @@ Section monotonicity.
   Hypothesis HvalidStLat : forall (e : instr_kind) st n, e = (Store, (st, n)) -> n = 0.
   Hypothesis HvalidLdLat : forall (e : instr_kind) st n dlat, e = (Load dlat, (st, n)) -> 0 <> n -> st = Lu /\ n <= dlat.
 
-  Lemma moved_lat_is_lower :
+  Lemma moved_lat_is_monotonic :
     forall n n', e = (opc, (st, n)) -> e' = (opc, (st', n')) -> e <> e' ->
                  state_leb (st, n) (st', n') = true ->
                  compare_two (List.nth_error tc i) (List.nth_error tc' i) = true.
@@ -324,7 +324,7 @@ Section monotonicity.
 
     destruct n, n'; [
         (* n and n' are = 0.  We have a lemma for that. *)
-        now apply moved_no_lat_is_lower |
+        now apply moved_no_lat_is_monotonic |
         (* Other cases: rewrite the goal to make cycle appear. *)
         rewrite Htc, Htc', Ht, Ht';
           unfold cycle;
@@ -374,8 +374,11 @@ Section monotonicity.
     intros n n' He He' Hsl.
     pose proof (instr_kind_is_comparable e e') as Heqd.
 
+    (* e = e' or e <> e'. *)
     destruct Heqd as [Heq | Hdiff].
-    - now apply (unmoved_can_advance n).
-    - now apply (moved_lat_is_lower n n').
+    - (* If e = e', we have a lemma for this. *)
+      now apply (unmoved_is_monotonic n).
+    - (* If e <> e', we have a lemma for this. *)
+      now apply (moved_lat_is_monotonic n n').
   Qed.
 End monotonicity.