Library com.io7m.entomos.Alignment


Require Import Stdlib.Arith.PeanoNat.

Alignment

Return size scaled such that it is a multiple of q.
Definition asMultipleOf (size q : nat) (Hnz : 0 ≠ q) : nat :=
  let r := size / q in
    match Nat.ltb_spec0 r q with
    | ReflectT _ _ ⇒ (r + 1) × q
    | ReflectF _ _ ⇒ r × q
    end.

#[local]
Lemma p0not4 : 0 ≠ 4.
Proof. discriminate. Qed.

#[local]
Lemma p0not16 : 0 ≠ 16.
Proof. discriminate. Qed.

Return size scaled such that it is a multiple of 4.
Definition asMultipleOf4 (size : nat) : nat :=
  asMultipleOf size 4 p0not4.

Return size scaled such that it is a multiple of 6.
Definition asMultipleOf16 (size : nat) : nat :=
  asMultipleOf size 16 p0not16.

If n is a multiple of m, then n mod m = 0.
Lemma asMultipleOfMod : ∀ s q (Hneq : 0 ≠ q), (asMultipleOf s q Hneq) mod q = 0.
Proof.
  intros s q Hneq.
  unfold asMultipleOf.
  destruct (Nat.ltb_spec0 (s / q) q) as [Hlt|H1].
  - apply (Nat.Div0.mod_mul (s / q + 1) q).
  - apply (Nat.Div0.mod_mul (s / q) q).
Qed.