proposition: Theorem spec_shiftl_pow2 : forall x n, [shiftl x n] = [x] * 2 ^ [n].
proof: Proof. intros x n; unfold shiftl, shiftl_aux_body. rewrite spec_compare; case Z.compare_spec; intros H. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite <- (spec_double_size x). rewrite spec_compare; case Z.compare_spec; intros H1. apply spec_unsafe_shiftl; auto with zarith. apply spec_unsafe_shiftl; auto with zarith. rewrite <- (spec_double_size (double_size x)). apply spec_shiftl_aux with 1%positive. apply Z.le_trans with (2 := spec_double_size_head0 (double_size x)). replace (2 ^ 1) with (2 * 1). apply Z.mul_le_mono_nonneg_l; auto with zarith. generalize (spec_double_size_head0_pos x); auto with zarith. rewrite Z.pow_1_r; ring. intros x1 H2; apply spec_unsafe_shiftl. apply Z.le_trans with (2 := H2). apply Z.le_trans with (2 ^ Zpos (digits n)); auto with zarith. case (spec_digits n); auto with zarith. apply Z.pow_le_mono_r; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen