proposition: Lemma shiftl_spec_high a n m : 0<=m -> n<=m -> testbit (shiftl a n) m = testbit a (m-n).
proof: Proof. intros Hm H. destruct n as [ |n|n]. - simpl. now rewrite sub_0_r. - destruct m as [ |m|m]; try (now destruct H). assert (0 <= pos m - pos n). { red. now rewrite compare_antisym, <- compare_sub, <- compare_antisym. } assert (EQ : to_N (pos m - pos n) = (N.pos m - N.pos n)%N). { red in H. simpl in H. simpl to_N. rewrite pos_sub_spec, Pos.compare_antisym. destruct (Pos.compare_spec n m) as [H'|H'|H']; try (now destruct H). - subst. now rewrite N.sub_diag. - simpl. destruct (Pos.sub_mask_pos' m n H') as (p & -> & <-). f_equal. now rewrite Pos.add_comm, Pos.add_sub. } destruct a as [|p|p]; unfold shiftl. + replace (Pos.iter (mul 2) 0 n) with 0 by (apply Pos.iter_invariant; intros; subst; trivial). now rewrite 2 testbit_0_l. + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite 2 testbit_Zpos, EQ by easy. exact (N.shiftl_spec_high' (N.pos p) (N.pos n) (N.pos m) H). + rewrite <- (Pos.iter_swap_gen _ _ _ xO) by trivial. rewrite 2 testbit_Zneg, EQ by easy. f_equal. simpl to_N. rewrite <- N.shiftl_spec_high by easy. now apply (N.pos_pred_shiftl_high p (N.pos n)). - unfold sub. simpl. now apply (shiftr_spec_aux a (pos n) m). Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass