diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-06 19:07:04 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-06 21:14:21 -0500 |
| commit | 8c357c935d52a7b7d3beaad5dfd1f870c137eb24 (patch) | |
| tree | e893c444292d3345c36039ea438ae72f50abcf8a /src/Reflection/Z | |
| parent | c8ce1653b9a3489882c07629eaacb31a13444b6f (diff) | |
Move things from WordUtil to ZUtil, add word lemma
Diffstat (limited to 'src/Reflection/Z')
| -rw-r--r-- | src/Reflection/Z/InterpretationsGen.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Reflection/Z/InterpretationsGen.v b/src/Reflection/Z/InterpretationsGen.v index 6ccb23960..f11837e60 100644 --- a/src/Reflection/Z/InterpretationsGen.v +++ b/src/Reflection/Z/InterpretationsGen.v @@ -233,9 +233,9 @@ Module InterpretationsGen (Bit : BitSize). Lemma wordWToZ_shl : bounds_2statement shl Z.shiftl. Proof. wWToZ_t; wWToZ_extra_t; unfold wordWToZ, wordBin. - rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftl; reflexivity|]. + rewrite wordToN_NToWord_idempotent; [rewrite <- N2Z.inj_shiftl; reflexivity|]. apply N2Z.inj_lt. - rewrite Z_inj_shiftl. + rewrite N2Z.inj_shiftl. destruct (Z.lt_ge_cases 0 ((wordWToZ x) << (wordWToZ y)))%Z; [|eapply Z.le_lt_trans; [|apply N2Z.inj_lt, Npow2_gt0]; assumption]. rewrite Npow2_N, N2Z.inj_pow, ?nat_N_Z. @@ -245,9 +245,9 @@ Module InterpretationsGen (Bit : BitSize). Lemma wordWToZ_shr : bounds_2statement shr Z.shiftr. Proof. wWToZ_t; wWToZ_extra_t; unfold wordWToZ, wordBin. - rewrite wordToN_NToWord_idempotent; [rewrite <- Z_inj_shiftr; reflexivity|]. + rewrite wordToN_NToWord_idempotent; [rewrite <- N2Z.inj_shiftr; reflexivity|]. apply N2Z.inj_lt. - rewrite Z_inj_shiftr. + rewrite N2Z.inj_shiftr. destruct (Z.lt_ge_cases 0 ((wordWToZ x) >> (wordWToZ y)))%Z; [|eapply Z.le_lt_trans; [|apply N2Z.inj_lt, Npow2_gt0]; assumption]. rewrite Npow2_N, N2Z.inj_pow, nat_N_Z. |