definitions: simplify proofs

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

src/definitions.v

@@ -90,11 +90,12 @@ Proof.
   intros s o.
 
   (* Enumerate all stages *)
-  destruct s;
-    try reflexivity. (* Trivial for all cases, except Lsu *)
-  (* Lsu depends on the opcode *)
-  destruct o;
-    reflexivity.
+  destruct s eqn:Hs;
+    match goal with
+    (* Trivial for all cases, except Lsu: depends on the opcode *)
+    | [ _ : s = Lsu |- _ ] => destruct o; reflexivity
+    | _ => reflexivity
+    end.
 Qed.
 
 Variant sbStateT :=
@@ -166,9 +167,7 @@ Lemma kind_is_valid :
 Proof.
   intros t i Hl.
   assert (Hl' := Hl).
-  rewrite <- opc_length in Hl.
-  rewrite <- (nth_error_Some (get_opc t) i) in Hl.
-  exact Hl.
+  now rewrite <- opc_length, <- (nth_error_Some (get_opc t) i) in Hl.
 Qed.
 
 Lemma stage_is_valid :
@@ -176,9 +175,7 @@ Lemma stage_is_valid :
 Proof.
   intros t i Hl.
   assert (Hl' := Hl).
-  rewrite <- stg_length in Hl.
-  rewrite <- (nth_error_Some (get_stg t) i) in Hl.
-  exact Hl.
+  now rewrite <- stg_length, <- (nth_error_Some (get_stg t) i) in Hl.
 Qed.
 
 Lemma cycle_is_valid :
@@ -186,9 +183,7 @@ Lemma cycle_is_valid :
 Proof.
   intros t i Hl.
   assert (Hl' := Hl).
-  rewrite <- cyc_length in Hl.
-  rewrite <- (nth_error_Some (get_cyc t) i) in Hl.
-  exact Hl.
+  now rewrite <- cyc_length, <- (nth_error_Some (get_cyc t) i) in Hl.
 Qed.
 
 Lemma not_some_0_is_some_n :
@@ -199,8 +194,7 @@ Proof.
   intros i t Hi Hzero.
 
   assert (nth_error (get_cyc t) i <> None) as Hnone.
-  - apply cycle_is_valid.
-    exact Hi.
+  - now apply cycle_is_valid.
 
   - destruct nth_error.
     + exists n.
@@ -266,8 +260,7 @@ Section check_correctness.
     rewrite (check_latencies_is_correct_v0 _ t1 tstep).
     - rewrite (check_latencies_is_correct_v0 tstep [e] t2).
       + rewrite He.
-        destruct lat;
-          reflexivity.
+        now destruct lat.
       + exact Htstep.
     - exact Ht.
   Qed.
@@ -295,8 +288,7 @@ Section check_correctness.
     rewrite <- Htstep in Ht.
     rewrite (check_loads_and_stores_is_correct_v0 t t1 tstep).
     - rewrite (check_loads_and_stores_is_correct_v0 tstep [e] t2).
-      + rewrite He, andb_comm.
-        reflexivity.
+      + now rewrite He, andb_comm.
       + exact Htstep.
     - exact Ht.
   Qed.
@@ -309,8 +301,7 @@ Section check_correctness.
     rewrite <- Htstep in Ht.
     rewrite (check_loads_and_stores_is_correct_v0 t t1 tstep).
     - rewrite (check_loads_and_stores_is_correct_v0 tstep [e] t2).
-      + rewrite He, andb_comm.
-        reflexivity.
+      + now rewrite He, andb_comm.
       + exact Htstep.
     - exact Ht.
   Qed.