From 2e8928231f46e5f0cfb454849dd41731a3201867 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 17 Jun 2020 21:14:09 +0100
Subject: Coq: implement shl_int_1

---
 lib/arith.sail   |  2 +-
 lib/coq/Values.v | 10 ++++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)

diff --git a/lib/arith.sail b/lib/arith.sail
index d57fd559..371a4a45 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -65,7 +65,7 @@ val _shl8 = {c: "shl_mach_int", coq: "shl_int_8", _: "shl_int"} :
 val _shl32 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} :
   forall 'n, 'n in {0, 1}. (int(32), int('n)) -> {'m, 'm in {32, 64}. int('m)}
 
-val _shl1 = {c: "shl_mach_int", coq: "shl_int_32", _: "shl_int"} :
+val _shl1 = {c: "shl_mach_int", coq: "shl_int_1", _: "shl_int"} :
   forall 'n, 0 <= 'n <= 3. (int(1), int('n)) -> {'m, 'm in {1, 2, 4, 8}. int('m)}
 
 val _shl_int = "shl_int" : (int, int) -> int
diff --git a/lib/coq/Values.v b/lib/coq/Values.v
index 1a9eb644..2cab87f8 100644
--- a/lib/coq/Values.v
+++ b/lib/coq/Values.v
@@ -2835,6 +2835,16 @@ Definition max_nat (x : Z) `{ArithFact (x >=? 0)} (y : Z) `{ArithFact (y >=? 0)}
   {z : Z & ArithFact (z >=? 0)} :=
   build_ex (Z.max x y).
 
+Definition shl_int_1 (x y : Z) `{HE:ArithFact (x =? 1)} `{HR:ArithFact (0 <=? y <=? 3)}: {z : Z & ArithFact (member_Z_list z [1;2;4;8])}.
+refine (existT _ (shl_int x y) _).
+destruct HE as [HE].
+destruct HR as [HR].
+unbool_comparisons.
+assert (y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega.
+constructor.
+intuition (subst; compute; auto).
+Defined.
+
 Definition shl_int_8 (x y : Z) `{HE:ArithFact (x =? 8)} `{HR:ArithFact (0 <=? y <=? 3)}: {z : Z & ArithFact (member_Z_list z [8;16;32;64])}.
 refine (existT _ (shl_int x y) _).
 destruct HE as [HE].
-- 
cgit v1.2.3