From 92f1e32b677d3b80eb509ddadb323714de2b3092 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 18 Jul 2018 11:35:04 +0100
Subject: Coq: constraint solving improvements Use eauto so that user-added
 hints are more flexible, example with Replicate in aarch64, dropped zbool to
 prevent slow proof searches (and preprocessing deals with boolean comparisons
 now). Report failed constraints after preprocessing; Separate preprocessing
 tactic out.

---
 aarch64/aarch64_extras.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'aarch64')

diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v
index 7d5020ec..94851ef5 100644
--- a/aarch64/aarch64_extras.v
+++ b/aarch64/aarch64_extras.v
@@ -10,6 +10,31 @@ Axiom set_slice : forall (n : Z) (m : Z), mword n -> Z -> mword m -> mword n.
 Definition length {n} (x : mword n) := length_mword x.
 Hint Unfold length : sail.
 
+
+Lemma Replicate_lemma1 {N M O x} :
+  O * M = N ->
+  O = Z.quot N M ->
+  x = Z.quot N M -> M * x = N.
+intros. rewrite H1.
+rewrite H0 in H.
+rewrite Z.mul_comm.
+assumption.
+Qed.
+Hint Resolve Replicate_lemma1 : sail.
+
+Lemma Replicate_lemma2 {N M x} :
+ M >= 0 /\ N >= 0 ->
+ x = Z.quot N M ->
+ x >= 0.
+intros; subst.
+destruct M; destruct N; intros; try easy.
+unfold Z.quot, Z.quotrem.
+destruct (N.pos_div_eucl p0 (N.pos p)) as [x y].
+case x; easy.
+Qed.
+Hint Resolve Replicate_lemma2 : sail.
+
+
 (*
 let hexchar_to_bool_list c =
   if c = #'0' then      Just ([false;false;false;false])
-- 
cgit v1.2.3