proposition: Theorem spec_shiftl_aux: forall p q x n cont, 2 ^ (Zpos q) <= [head0 x] -> (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] -> [cont x n] = [x] * 2 ^ [n]) -> [shiftl_aux p cont x n] = [x] * 2 ^ [n].
proof: Proof. intros p; elim p; unfold shiftl_aux; fold shiftl_aux; clear p. intros p Hrec q x n cont H1 H2. apply spec_shiftl_aux_body with (q); auto. intros x1 H3; apply Hrec with (q + 1)%positive; auto. intros x2 H4; apply Hrec with (p + q + 1)%positive; auto. rewrite <- Pos.add_assoc. rewrite Pos2Z.inj_add; auto. intros x3 H5; apply H2. rewrite Pos2Z.inj_xI. replace (2 * Zpos p + 1 + Zpos q) with (Zpos p + Zpos (p + q + 1)); auto. rewrite !Pos2Z.inj_add; ring. intros p Hrec q n x cont H1 H2. apply spec_shiftl_aux_body with (q); auto. intros x1 H3; apply Hrec with (q); auto. apply Z.le_trans with (2 := H3); auto with zarith. apply Z.pow_le_mono_r; auto with zarith. intros x2 H4; apply Hrec with (p + q)%positive; auto. intros x3 H5; apply H2. rewrite (Pos2Z.inj_xO p). replace (2 * Zpos p + Zpos q) with (Zpos p + Zpos (p + q)); auto. rewrite Pos2Z.inj_add; ring. intros q n x cont H1 H2. apply spec_shiftl_aux_body with (q); auto. rewrite Z.add_comm; auto. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen