(* Coq Formalization of Q16_16 Fixed-Point Arithmetic *)
Require Import ZArith Lia.

Lemma le_neg2147483648_2147483647 : (-2147483648 <= 2147483647)%Z.
Proof. lia. Qed.
Lemma le_0_2147483647 : (0 <= 2147483647)%Z.
Proof. lia. Qed.
Lemma le_neg2147483648_0 : (-2147483648 <= 0)%Z.
Proof. lia. Qed.

Lemma le_2147483647_2147483647 : (2147483647 <= 2147483647)%Z.
Proof. lia. Qed.

Module Q16_16.
  Open Scope Z_scope.

  Definition q16_min_raw : Z := -2147483648.
  Definition q16_max_raw : Z := 2147483647.
  Definition q16_scale  : Z := 65536.

  Definition in_range (x : Z) : Prop :=
    q16_min_raw <= x /\ x <= q16_max_raw.

  Definition clamp_raw (i : Z) : Z :=
    if Z_lt_dec q16_max_raw i then q16_max_raw
    else if Z_lt_dec i q16_min_raw then q16_min_raw
    else i.

  Theorem clamp_bounded (x : Z) : in_range (clamp_raw x).
  Proof.
    unfold clamp_raw, in_range.
    case (Z_lt_dec q16_max_raw x); intros H1.
    - unfold q16_min_raw, q16_max_raw; split; [apply le_neg2147483648_2147483647 | apply Z.le_refl].
    - case (Z_lt_dec x q16_min_raw); intros H2.
      + unfold q16_min_raw, q16_max_raw; split; [apply Z.le_refl | apply le_neg2147483648_2147483647].
      + split; apply Z.nlt_ge; assumption.
  Qed.

  Theorem clamp_idempotent (x : Z) (h : in_range x) : clamp_raw x = x.
  Proof.
    destruct h as [Hlo Hhi].
    unfold clamp_raw.
    case (Z_lt_dec q16_max_raw x); intros Hgt; [exfalso; exact (Zlt_not_le _ _ Hgt Hhi) |].
    case (Z_lt_dec x q16_min_raw); intros Hlt; [exfalso; exact (Zlt_not_le _ _ Hlt Hlo) |].
    reflexivity.
  Qed.

  Definition zero : Z := 0.
  Definition one : Z := 65536.
  Definition epsilon : Z := 1.
  Definition half : Z := 32768.
  Definition pct1   : Z := 655.
  Definition pct70  : Z := 45875.
  Definition pct30  : Z := 19661.
  Definition one50  : Z := 98304.

  Definition add (a b : Z) : Z := clamp_raw (a + b).
  Definition sub (a b : Z) : Z := clamp_raw (a - b).
  Definition neg (a : Z) : Z := clamp_raw (-a).
  Definition mul (a b : Z) : Z := clamp_raw (Z.div (a * b) q16_scale).
  Definition div (a b : Z) : Z :=
    if Z.eq_dec b 0 then zero else clamp_raw (Z.div (a * q16_scale) b).

  Theorem add_comm (a b : Z) : add a b = add b a.
  Proof. unfold add; rewrite Z.add_comm; reflexivity. Qed.

  Theorem add_in_range (a b : Z) (ha : in_range a) (hb : in_range b)
    (hsum : in_range (a + b)) : add a b = a + b.
  Proof.
    unfold add; rewrite clamp_idempotent; trivial.
  Qed.

  Theorem sub_self (a : Z) (ha : in_range a) : sub a a = zero.
  Proof.
    unfold sub, zero; rewrite Z.sub_diag.
    apply clamp_idempotent; unfold in_range; unfold q16_min_raw, q16_max_raw.
    split; [apply le_neg2147483648_0 | apply le_0_2147483647].
  Qed.

  Theorem mul_comm (a b : Z) : mul a b = mul b a.
  Proof. unfold mul; rewrite Z.mul_comm; reflexivity. Qed.

  Theorem in_range_zero : in_range 0.
  Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.

  Theorem in_range_one : in_range 1.
  Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.

End Q16_16.