proposition: Theorem mask_spec: forall k m n, is_mask m n -> (forall p, (p < n)%nat -> testbit (mask k m) p = testbit k p) /\ (forall p, (p >= n)%nat -> testbit (mask k m) p = false).
proof: Proof. intros k m n P. unfold mask; simpl. split. - intros. rewrite land_spec. assert (testbit (interp m) p = true). + eapply interp_spec. exact P. exact H. + unfold testbit in *. rewrite H0. destruct (K.testbit k p); auto. - intros. rewrite land_spec. assert (testbit (interp m) p = false). + case_eq (testbit (interp m) p); intros; auto. eapply interp_spec in H0; simpl in H0; eauto; try lia. + unfold testbit in *. rewrite H0. destruct (K.testbit k p); auto. Qed.
imports: Lia Cdcl.Coqlib