diff options
Diffstat (limited to 'src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v')
-rw-r--r-- | src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v | 42 |
1 files changed, 0 insertions, 42 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v deleted file mode 100644 index 7210d80d5..000000000 --- a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v +++ /dev/null @@ -1,42 +0,0 @@ -Require Import Coq.ZArith.ZArith. -Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.LegacyArithmetic.Double.Core. -Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Definitions. - -Local Open Scope Z_scope. - -Local Opaque tuple_decoder. -Local Arguments Z.pow !_ !_. -Local Arguments Z.mul !_ !_. - -Section shrd. - Context (n : Z) {W} - {ldi : load_immediate W} - {shrd : shift_right_doubleword_immediate W} - {decode : decoder n W} - {isdecode : is_decode decode} - {isldi : is_load_immediate ldi} - {isshrd : is_shift_right_doubleword_immediate shrd}. - - Local Ltac zutil_arith ::= solve [ auto with nocore omega ]. - - Global Instance is_shift_right_doubleword_immediate_double : is_shift_right_doubleword_immediate (shrd_double n). - Proof using isdecode isshrd. - intros high low count Hcount; hnf in Hcount. - unfold shrd_double, shift_right_doubleword_immediate_double; simpl. - generalize (decode_range low). - generalize (decode_range high). - generalize (decode_range (fst low)). - generalize (decode_range (snd low)). - generalize (decode_range (fst high)). - generalize (decode_range (snd high)). - assert (forall x, 0 <= Z.pow2_mod x n < 2^n) by auto with zarith. - assert (forall n' x, 2^n <= 2^n' -> 0 <= x < 2^n -> 0 <= x < 2^n') by auto with zarith. - assert (forall n' x, n <= n' -> 0 <= x < 2^n -> 0 <= x < 2^n') by auto with zarith omega. - autorewrite with simpl_tuple_decoder; push_decode. - shift_left_right_t. - Qed. -End shrd. |