proposition: Lemma are_bits : forall (f:t->bool), Proper (eq==>Logic.eq) f -> ((exists n, forall m, 0<=m -> f m = n.[m]) <-> (exists k, forall m, k<=m -> f m = f k)).
proof: Proof. intros f Hf. split. - intros (a,H). destruct (le_gt_cases 0 a). + exists (S (log2 a)). intros m Hm. apply le_succ_l in Hm. rewrite 2 H, 2 bits_above_log2; trivial using lt_succ_diag_r. { order_pos. } apply le_trans with (log2 a); order_pos. + exists (S (log2 (P (-a)))). intros m Hm. apply le_succ_l in Hm. rewrite 2 H, 2 bits_above_log2_neg; trivial using lt_succ_diag_r. { order_pos. } apply le_trans with (log2 (P (-a))); order_pos. - intros (k,Hk). destruct (lt_ge_cases k 0) as [LT|LE]. + case_eq (f 0); intros H0. * exists (-1). intros m Hm. rewrite bits_m1, Hk by order. symmetry; rewrite <- H0. apply Hk; order. * exists 0. intros m Hm. rewrite bits_0, Hk by order. symmetry; rewrite <- H0. apply Hk; order. + revert f Hf Hk. apply le_ind with (4:=LE). * apply proper_sym_impl_iff. { exact eq_sym. } clear k LE. intros k k' Hk IH f Hf H. apply IH; trivial. now setoid_rewrite Hk. * { intros f Hf H0. destruct (f 0). - exists (-1). intros m Hm. now rewrite bits_m1, H0. - exists 0. intros m Hm. now rewrite bits_0, H0. } * { clear k LE. intros k LE IH f Hf Hk. destruct (IH (fun m => f (S m))) as (n, Hn). - solve_proper. - intros m Hm. apply Hk. now rewrite <- succ_le_mono. - exists (f 0 + 2*n). intros m Hm. le_elim Hm. + rewrite <- (succ_pred m), Hn, <- div2_bits. * rewrite mul_comm, div_add, b2z_div2, add_0_l; trivial. order'. * now rewrite <- lt_succ_r, succ_pred. * now rewrite <- lt_succ_r, succ_pred. + rewrite <- Hm. symmetry. apply add_b2z_double_bit0. } Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog