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, 9 insertions, 1 deletions

diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v
index 94851ef5..67d165cd 100644
--- a/aarch64/aarch64_extras.v
+++ b/aarch64/aarch64_extras.v
@@ -133,4 +133,12 @@ Definition read_ram {rv e} addrsize size `{ArithFact (size >= 0)} (hexRAM : mwor
 (*val elf_entry : unit -> integer*)
 Definition elf_entry (_:unit) := 0.
 (*declare ocaml target_rep function elf_entry = `Elf_loader.elf_entry`
-*)
\ No newline at end of file
+*)
+
+Lemma mul_quot_8_helper : forall x, 8 * x = 8 * (Z.quot (8 * x) 8).
+intro.
+rewrite Z.mul_comm.
+rewrite Z.quot_mul; auto with zarith.
+Qed.
+Hint Resolve mul_quot_8_helper : sail.
+