diff options
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Sail2_values.v | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index d1f1a768..9cff3f83 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1948,3 +1948,20 @@ Definition min_nat (x : Z) `{ArithFact (x >= 0)} (y : Z) `{ArithFact (y >= 0)} : 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_8 (x y : Z) `{HE:ArithFact (x = 8)} `{HR:ArithFact (0 <= y <= 3)}: {z : Z & ArithFact (In z [8;16;32;64])}. +refine (existT _ (shl_int x y) _). +destruct HE as [HE]. +destruct HR as [HR]. +assert (H : y = 0 \/ y = 1 \/ y = 2 \/ y = 3) by omega. +constructor. +intuition (subst; compute; auto). +Defined. + +Definition shl_int_32 (x y : Z) `{HE:ArithFact (x = 32)} `{HR:ArithFact (In y [0;1])}: {z : Z & ArithFact (In z [32;64])}. +refine (existT _ (shl_int x y) _). +destruct HE as [HE]. +destruct HR as [[HR1 | [HR2 | []]]]; +subst; compute; +auto using Build_ArithFact. +Defined. |