From a543cf7946fbcb8eb94d66ee716d46e51663b69a Mon Sep 17 00:00:00 2001
From: Alban Gruin <alban.gruin@irit.fr>
Date: Tue, 26 Jul 2022 16:14:20 +0200
Subject: [PATCH] definitions: simplify proofs
Signed-off-by: Alban Gruin <alban.gruin@irit.fr>
---
src/definitions.v | 35 +++++++++++++----------------------
1 file changed, 13 insertions(+), 22 deletions(-)
diff --git a/src/definitions.v b/src/definitions.v
index 6f1ef36..34e7527 100644
--- a/src/definitions.v
+++ b/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.
--
GitLab