From 5a947f5d5f5fd9b83f27bfd4e43170f51d4a27a7 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 3 Sep 2018 12:00:16 +0100
Subject: 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
---
 aarch64/aarch64_extras.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'aarch64')

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.
+
-- 
cgit v1.2.3