diff options
| author | Brian Campbell | 2018-07-16 15:59:23 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-16 18:29:45 +0100 |
| commit | a48dad8232a7db82c74a72157249a27ce25d326e (patch) | |
| tree | 58dc296c5046a6716dfbbc645d60d433eebc8973 /lib | |
| parent | 7bdcdcc7abdde74993020d1f2c33ea00d6784fc4 (diff) | |
Coq: add support for more complex atom types
As a result, add proof to pow2.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index ab557ff4..335ebf26 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -73,7 +73,13 @@ Definition nn := nat. (*val pow : Z -> Z -> Z*) Definition pow m n := m ^ n. -Definition pow2 n := pow 2 n. +Program Definition pow2 n : {z : Z & ArithFact (2 ^ n <= z <= 2 ^ n)} := existT _ (pow 2 n) _. +Next Obligation. +constructor. +unfold pow. +auto using Z.le_refl. +Qed. + (* Definition inline lt := (<) Definition inline gt := (>) |