Coq: rework generation of dependent pairs so that they are only

constructed when a function call, cast, or binder demands them, removing
some ambiguous corner cases.

Also
- Don't simplify nexps before printing (note that we usually end up
  needing a (8 * x) / 8 lemma as a result)
- More extraction of properties in the goal
- Splitting of conditionals/matches in goals (which can occur more often
  because of the new positions of build_ex in definitions)
- Try simple solving first to improve speed / reduce proof sizes / help
  fill in metavariables (because manipulating the goal can interfere with
  instantiating them)
- Update RISC-V patch

1 files changed, 6 insertions, 0 deletions

diff --git a/mips/mips_extras.v b/mips/mips_extras.v
index 51856d9e..83f39079 100644
--- a/mips/mips_extras.v
+++ b/mips/mips_extras.v
@@ -161,6 +161,12 @@ Definition putchar {T} (_:T) : unit := tt.
 Require DecimalString.
 Definition string_of_int z := DecimalString.NilZero.string_of_int (Z.to_int z).
 
+Lemma __MIPS_read_lemma : forall width, 8 * width = 8 * (8 * width ÷ 8).
+intros.
+rewrite Z.mul_comm.
+rewrite Z.quot_mul; auto with zarith.
+Qed.
+Hint Resolve __MIPS_read_lemma : sail.
 
 Lemma MEMr_wrapper_lemma : forall size : Z, 8 * size = 8 * (8 * (8 * size ÷ 8) ÷ 8).
 intros.