proposition: Theorem zerobit_spec: forall k m n, is_mask m n -> zerobit k m = negb (testbit k n).
proof: Proof. intros k m n P. unfold zerobit; simpl. apply eqb_eq; intro e. - assert (testbit m n = true) by (apply P; auto). assert (testbit (land k m) n = false). { rewrite e. rewrite zero_spec; simpl; auto. } rewrite land_spec in H0. unfold testbit in *. rewrite H in H0. destruct (K.testbit k n); simpl; auto. - assert (forall p, p <> n -> testbit m p = false). + intros. case_eq (testbit m p); intros; auto. apply P in H0. elim H; auto. + assert (forall p, p <> n -> testbit (land k m) p = false). * intros; rewrite land_spec. rewrite H; auto. destruct (K.testbit k p); simpl; auto. * case_eq (testbit k n); intros. { assert (land k m = m). - apply testbit_spec; intros. rewrite land_spec. destruct (Nat.eq_dec n0 n). + subst n0. unfold testbit in *. rewrite (proj2 (P n)); auto. rewrite H1; auto. + rewrite H; auto. destruct (K.testbit k n0); simpl; auto. - simpl; auto. } { elim e. apply testbit_spec. intros; rewrite zero_spec. destruct (Nat.eq_dec n0 n). - subst n0. unfold testbit in *. rewrite land_spec; rewrite H1; simpl; auto. - rewrite H0; auto. } Qed.
imports: Lia Cdcl.Coqlib