diff options
| author | Brian Campbell | 2020-06-17 21:14:09 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-06-17 21:14:09 +0100 |
| commit | 2e8928231f46e5f0cfb454849dd41731a3201867 (patch) | |
| tree | b675b11deb9cfc7a8fb35d01632d898e9c8fc71c | |
| parent | 4ea47e5a20f6cdf201774e8bd2ddfb977ee4dc43 (diff) | |
Coq: implement shl_int_1
| -rw-r--r-- | lib/arith.sail | 2 | ||||
| -rw-r--r-- | lib/coq/Values.v | 10 |
2 files changed, 11 insertions, 1 deletions
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]. |