(* Coq Formalization of Q16_16 Fixed-Point Arithmetic (Rocq 9.0) *)
From Corelib Require Import BinNums PosDef NatDef IntDef.
Require Import SilverSight.coq.ZCompat.
Local Open Scope Z_scope.

Fixpoint pow2_positive (n : nat) : positive :=
  match n with O => xH | S m => xO (pow2_positive m) end.

Fixpoint ones_positive (n : nat) : positive :=
  match n with O => xH | S m => xI (ones_positive m) end.

Definition p65536 : positive := pow2_positive 16.
Definition p2147483647 : positive := ones_positive 31.
Definition p2147483648 : positive := pow2_positive 31.

Lemma neg_le_pos (p q : positive) : Z.le (Zneg p) (Zpos q).
Proof. unfold Z.le, Z.compare; discriminate. Qed.
Lemma neg_le_zero (p : positive) : Z.le (Zneg p) Z0.
Proof. unfold Z.le, Z.compare; discriminate. Qed.
Lemma zero_le_pos (q : positive) : Z.le Z0 (Zpos q).
Proof. unfold Z.le, Z.compare; discriminate. Qed.
Lemma pos_le_pos (q : positive) : Z.le (Zpos q) (Zpos q).
Proof. unfold Z.le, Z.compare; rewrite Pos_compare_self; discriminate. Qed.

Lemma le_neg2147483648_2147483647 : Z.le (Zneg p2147483648) (Zpos p2147483647).
Proof. apply neg_le_pos. Qed.
Lemma le_0_2147483647 : Z.le Z0 (Zpos p2147483647).
Proof. apply zero_le_pos. Qed.
Lemma le_neg2147483648_0 : Z.le (Zneg p2147483648) Z0.
Proof. apply neg_le_zero. Qed.
Lemma le_2147483647_2147483647 : Z.le (Zpos p2147483647) (Zpos p2147483647).
Proof. apply pos_le_pos. Qed.

Module Q16_16.
  Open Scope Z_scope.

  Definition q16_min_raw : Z := Zneg p2147483648.
  Definition q16_max_raw : Z := Zpos p2147483647.
  Definition q16_scale  : Z := Zpos p65536.

  Definition in_range (x : Z) : Prop :=
    Z.le q16_min_raw x /\ Z.le 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 Zle_refl].
    - case (Z_lt_dec x q16_min_raw); intros H2.
      + unfold q16_min_raw, q16_max_raw; split; [apply Zle_refl | apply le_neg2147483648_2147483647].
      + split; apply Znlt_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 := Z0.
  Definition one : Z := Zpos p65536.
  Definition epsilon : Z := Zpos xH.
  Definition half : Z := Zpos (pow2_positive 15).
  Definition pct1   : Z := Zpos (xI(xI(xI(xI(xO(xO(xO(xI(xO(xH)))))))))).
  Definition pct70  : Z := Zpos (xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xH)))))))))))))))).
  Definition pct30  : Z := Zpos (xI(xO(xI(xI(xO(xO(xI(xI(xO(xO(xI(xI(xO(xO(xH))))))))))))))).
  Definition one50  : Z := Zpos (xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xO(xI(xH))))))))))))))))).

  Definition add (a b : Z) : Z := clamp_raw (Z.add a b).
  Definition sub (a b : Z) : Z := clamp_raw (Z.sub a b).
  Definition neg (a : Z) : Z := clamp_raw (Z.opp a).
  Definition mul (a b : Z) : Z := clamp_raw (Z.div (Z.mul a b) q16_scale).
  Definition div (a b : Z) : Z :=
    if Z_eq_dec b Z0 then zero else clamp_raw (Z.div (Z.mul a q16_scale) b).

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

  Theorem add_in_range (a b : Z) (ha : in_range a) (hb : in_range b)
    (hsum : in_range (Z.add a b)) : add a b = Z.add 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 Zsub_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 Zmul_comm; reflexivity. Qed.

  Theorem in_range_zero : in_range Z0.
  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 (Zpos xH).
  Proof. unfold in_range, q16_min_raw, q16_max_raw. split; [apply le_neg2147483648_0 | apply le_0_2147483647]. Qed.

End Q16_16.