Coq library improvements

- add liftRS support to tactics
- define uint and sint in terms of functions without proof terms
- eq_vec correctness
- lemma that rounding up integers using reals is the obvious integer calculation
- another proof irrelevance tactic
- try lemmas in the sail hintdb both before and after goal processing

1 files changed, 10 insertions, 0 deletions

diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index 5f409e22..ef82084f 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -199,6 +199,14 @@ unfold build_trivial_exS.
 apply bindS_cong; auto.
 Qed.
 
+Lemma liftRS_cong {A R Regs E} m m' :
+  m === m' ->
+  @liftRS A R Regs E m === liftRS m'.
+intros E1.
+unfold liftRS.
+apply try_catchS_cong; auto.
+Qed.
+
 (* Monad lifting *)
 
 Lemma liftState_bind Regval Regs A B E {r : Sail2_values.register_accessors Regs Regval} {m : monad Regval A E} {f : A -> monad Regval B E} :
@@ -287,6 +295,8 @@ Ltac statecong db :=
        solve [ eapply or_boolSP_cong; intros; statecong db ]
   | |- (build_trivial_exS _) === _ =>
        solve [ eapply build_trivial_exS_cong; intros; statecong db ]
+  | |- (liftRS _) === _ =>
+       solve [ eapply liftRS_cong; intros; statecong db ]
   | |- (let '(matchvar1, matchvar2) := ?e1 in _) === _ =>
        eapply (@equiv_transitive _ _ _ _ (let '(matchvar1,matchvar2) := e1 in _) _);
        [ destruct e1; etransitivity; [ statecong db | apply equiv_reflexive ]