Coq: solve some constraint/type errors with AArch64

- hints for dotp
- handle exists separately when trying eauto to keep search depth low
- more uniform existential handling (i.e., we now handle all existentials
  in the way we used to only handle existentials around atoms)

1 files changed, 29 insertions, 0 deletions

diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v
index 45c5e3ce..00ca8601 100644
--- a/aarch64/aarch64_extras.v
+++ b/aarch64/aarch64_extras.v
@@ -142,3 +142,32 @@ rewrite Z.quot_mul; auto with zarith.
 Qed.
 Hint Resolve mul_quot_8_helper : sail.
 
+(* For aarch64_vector_arithmetic_binary_uniform_mul_int_dotp *)
+Lemma quot4_ge {esize x} : 4 <= esize -> x = Z.quot esize 4 -> x >= 0.
+intros.
+apply Z.le_ge.
+subst.
+apply Z.quot_pos; omega.
+Qed.
+(* except that only proving the hard bit leads to an anomaly...
+Hint Resolve quot4_ge : sail.*)
+Lemma dotp_lemma {datasize esize x} :
+ 8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False ->
+ 4 <= esize -> x = Z.quot esize 4 -> datasize >= 0 /\ x >= 0.
+intros.
+split.
+* omega.
+* eauto using quot4_ge.
+Qed.
+Hint Resolve dotp_lemma : sail.
+
+
+Lemma quot4_gt {esize x} : 4 <= esize -> x = Z.quot esize 4 -> x > 0.
+intros.
+apply Z.lt_gt.
+subst.
+apply Z.quot_str_pos.
+omega.
+Qed.
+Hint Resolve quot4_gt : sail.
+