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

5 files changed, 138 insertions, 2 deletions

diff --git a/lib/coq/Hoare.v b/lib/coq/Hoare.v
index 44a81971..af0e8321 100644
--- a/lib/coq/Hoare.v
+++ b/lib/coq/Hoare.v
@@ -1152,6 +1152,8 @@ Ltac PrePostE_step :=
   | |- PrePostE _ (undefined_bitvectorS _) ?ppeQ ?ppeE =>
          apply PrePostE_undefined_bitvectorS_any with (Q := ppeQ) (E := ppeE)
   | |- PrePostE _ (build_trivial_exS _) _ _ => eapply PrePostE_build_trivial_exS; intros
+  | |- PrePostE _ (liftRS _) ?ppeQ ?ppeE =>
+         apply PrePostE_liftRS with (Q := ppeQ) (E := ppeE); intros
   | |- PrePostE _ (let '(_,_) := ?x in _) _ _ =>
          is_var x;
          let PAIR := fresh "PAIR" in
diff --git a/lib/coq/Sail2_operators_mwords.v b/lib/coq/Sail2_operators_mwords.v
index 9f40e0df..9970dcd5 100644
--- a/lib/coq/Sail2_operators_mwords.v
+++ b/lib/coq/Sail2_operators_mwords.v
@@ -288,8 +288,11 @@ induction n.
   reflexivity.
 Qed.
 
+Definition uint_plain {a} (x : mword a) : Z :=
+  Z.of_N (Word.wordToN (get_word x)).
+
 Program Definition uint {a} (x : mword a) : {z : Z & ArithFact (0 <=? z <=? 2 ^ a - 1)} :=
- existT _ (Z.of_N (Word.wordToN (get_word x))) _.
+ existT _ (uint_plain x) _.
 Next Obligation.
 constructor.
 apply Bool.andb_true_iff.
@@ -323,9 +326,13 @@ induction n.
   rewrite Z.pow_succ_r; auto with zarith.
 Qed.
 
+Definition sint_plain {a} (x : mword a) : Z :=
+  Word.wordToZ (get_word x).
+
 Program Definition sint {a} `{ArithFact (a >? 0)} (x : mword a) : {z : Z & ArithFact (-(2^(a-1)) <=? z <=? 2 ^ (a-1) - 1)} :=
-  existT _ (Word.wordToZ (get_word x)) _.
+  existT _ (sint_plain x) _.
 Next Obligation.
+unfold sint_plain.
 destruct H.
 unbool_comparisons.
 destruct a; try inversion fact.
@@ -513,6 +520,28 @@ Definition ugteq_vec := ugteq_bv.
 Definition sgteq_vec := sgteq_bv.
 
 *)
+Lemma eq_vec_true_iff {n} (v w : mword n) :
+  eq_vec v w = true <-> v = w.
+unfold eq_vec.
+destruct n.
+* simpl in v,w. shatter_word v. shatter_word w.
+  compute. intuition.
+* simpl in *. destruct (weq v w).
+  + subst. rewrite weqb_eq; tauto.
+  + rewrite weqb_ne; auto. intuition.
+* destruct v.
+Qed.
+
+Lemma eq_vec_false_iff {n} (v w : mword n) :
+  eq_vec v w = false <-> v <> w.
+specialize (eq_vec_true_iff v w).
+destruct (eq_vec v w).
+intuition.
+intros [H1 H2].
+split.
+* intros _ EQ. intuition.
+* auto.
+Qed.
 
 Definition eq_vec_dec {n} : forall (x y : mword n), {x = y} + {x <> y}.
 refine (match n with
diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v
index 494e36d4..4800f18b 100644
--- a/lib/coq/Sail2_real.v
+++ b/lib/coq/Sail2_real.v
@@ -34,3 +34,74 @@ Definition pow_real := powerRZ.
 
 Definition print_real (_ : string) (_ : R) : unit := tt.
 Definition prerr_real (_ : string) (_ : R) : unit := tt.
+
+
+
+
+Lemma IZRdiv m n :
+  0 < m -> 0 < n ->
+  (IZR (m / n) <= IZR m / IZR n)%R.
+intros.
+apply Rmult_le_reg_l with (r := IZR n).
+auto using IZR_lt.
+unfold Rdiv.
+rewrite <- Rmult_assoc.
+rewrite Rinv_r_simpl_m.
+rewrite <- mult_IZR.
+apply IZR_le.
+apply Z.mul_div_le.
+assumption.
+discrR.
+omega.
+Qed.
+
+(* One annoying use of reals in the ARM spec I've been looking at. *)
+Lemma round_up_div m n :
+  0 < m -> 0 < n ->
+  round_up (div_real (to_real m) (to_real n)) = (m + n - 1) / n.
+intros.
+unfold round_up, round_down, div_real, to_real.
+apply Z.eq_opp_l.
+apply Z.sub_move_r.
+symmetry.
+apply up_tech.
+
+rewrite Ropp_Ropp_IZR.
+apply Ropp_le_contravar.
+apply Rmult_le_reg_l with (r := IZR n).
+auto using IZR_lt.
+unfold Rdiv.
+rewrite <- Rmult_assoc.
+rewrite Rinv_r_simpl_m.
+rewrite <- mult_IZR.
+apply IZR_le.
+assert (diveq : n*((m+n-1)/n) = (m+n-1) - (m+n-1) mod n).
+apply Zplus_minus_eq.
+rewrite (Z.add_comm ((m+n-1) mod n)).
+apply Z.div_mod.
+omega.
+rewrite diveq.
+assert (modmax : (m+n-1) mod n < n).
+specialize (Z.mod_pos_bound (m+n-1) n). intuition.
+omega.
+
+discrR; omega.
+
+rewrite <- Z.opp_sub_distr.
+rewrite Ropp_Ropp_IZR.
+apply Ropp_lt_contravar.
+apply Rmult_lt_reg_l with (r := IZR n).
+auto using IZR_lt.
+unfold Rdiv.
+rewrite <- Rmult_assoc.
+rewrite Rinv_r_simpl_m.
+2: { discrR. omega. }
+rewrite <- mult_IZR.
+apply IZR_lt.
+rewrite Z.mul_sub_distr_l.
+apply Z.le_lt_trans with (m := m+n-1-n*1).
+apply Z.sub_le_mono_r.
+apply Z.mul_div_le.
+assumption.
+omega.
+Qed.
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 ]
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index f8315ecc..48920a59 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -65,6 +65,21 @@ Ltac replace_ArithFact_proof :=
     end
   end.
 
+Ltac generalize_ArithFact_proof_in H :=
+  match type of H with context f [?x] =>
+    match type of x with ArithFactP (?P = true) =>
+      let pf := fresh "pf" in
+      cut (forall (pf : ArithFact P), ltac:(let t := context f[pf] in exact t));
+      [ clear H; intro H
+      | intro pf; rewrite <- (ArithFact_irrelevant P x pf); apply H ]
+    | ArithFact ?P =>
+      let pf := fresh "pf" in
+      cut (forall (pf : ArithFact P), ltac:(let t := context f[pf] in exact t));
+      [ clear H; intro H
+      | intro pf; rewrite <- (ArithFact_irrelevant P x pf); apply H ]
+    end
+  end.
+
 (* Allow setoid rewriting through ArithFact *)
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
@@ -2134,8 +2149,16 @@ Ltac clear_fixpoints :=
     match goal with
     | H:_ -> ?res |- _ => is_fixpoint res; clear H
     end.
+Ltac clear_proof_bodies :=
+  repeat match goal with
+  | H := _ : ?ty |- _ =>
+    match type of ty with
+    | Prop => clearbody H
+    end
+  end.
 
 Ltac solve_arithfact :=
+  clear_proof_bodies;
   try solve [squashed_andor_solver]; (* Do this first so that it can name the intros *)
   intros; (* To solve implications for derive_m *)
   clear_fixpoints; (* Avoid using recursive calls *)
@@ -2144,6 +2167,7 @@ Ltac solve_arithfact :=
     [ solve_unknown
     | assumption
     | match goal with |- ArithFact ((?x <=? ?x <=? ?x)) => exact trivial_range end
+    | eauto 2 with sail (* the low search bound might not be necessary *)
     | fill_in_evar_eq
     | match goal with |- context [projT1 ?X] => apply (ArithFact_self_proof X) end
     | match goal with |- context [projT1 ?X] => apply (ArithFactP_self_proof X) end