(* ZCompat.v — Minimal ZArith compatibility shim for Rocq 9.0.
   Rocq 9.0's BinNums.IntDef defines Z operations but provides
   zero proof lemmas and no infix notations.
   This file supplies the subset needed by SilverSight's Q16_16
   and AVMIsa formalizations.
   NOTE: Use fully-qualified Z.* identifiers; infix +,-,*,<=,<,>=
   are NOT registered in Rocq 9.0's minimal IntDef.
*)
From Corelib Require Import BinNums PosDef NatDef IntDef.
Require Import SilverSight.coq.ProveAxioms.
Local Open Scope Z_scope.

(* ── Positive comparison lemmas ─────────────────────────────── *)

Lemma Pos_compare_self (p : positive) : Pos.compare p p = Eq.
Proof.
  unfold Pos.compare.
  induction p as [p IHp | p IHp | ]; simpl.
  - rewrite IHp; reflexivity.
  - rewrite IHp; reflexivity.
  - reflexivity.
Qed.

(* ── Z comparison lemmas ────────────────────────────────────── *)

Lemma Zcompare_self (x : Z) : Z.compare x x = Eq.
Proof. destruct x; simpl.
  - reflexivity.
  - apply Pos_compare_self.
  - unfold CompOpp; rewrite Pos_compare_self; reflexivity.
Qed.

Lemma Zcompare_antisym_lt (x y : Z) (h : Z.compare x y = Lt) : Z.compare y x = Gt.
Proof.
  destruct x, y; unfold Z.compare in *; simpl in *.
  - inversion h.
  - clear h; reflexivity.
  - inversion h.
  - inversion h.
  - apply Pos_compare_antisym_lt; exact h.
  - inversion h.
  - clear h; reflexivity.
  - clear h; reflexivity.
  - unfold CompOpp in h; destruct (Pos.compare p p0) eqn:hc; simpl in h.
    + inversion h.
    + inversion h.
    + clear h; unfold CompOpp; rewrite (Pos_compare_antisym_gt _ _ hc); reflexivity.
Qed.

Lemma Zcompare_antisym_gt (x y : Z) (h : Z.compare x y = Gt) : Z.compare y x = Lt.
Proof.
  destruct x, y; unfold Z.compare in *; simpl in *.
  - inversion h.
  - inversion h.
  - clear h; reflexivity.
  - clear h; reflexivity.
  - apply Pos_compare_antisym_gt; exact h.
  - clear h; reflexivity.
  - inversion h.
  - inversion h.
  - unfold CompOpp in h; destruct (Pos.compare p p0) eqn:hc; simpl in h.
    + inversion h.
    + clear h; unfold CompOpp; rewrite (Pos_compare_antisym_lt _ _ hc); reflexivity.
    + inversion h.
Qed.

Lemma Zcompare_eq (x y : Z) (h : Z.compare x y = Eq) : x = y.
Proof.
  destruct x, y; unfold Z.compare in *; simpl in *.
  - reflexivity.
  - inversion h.
  - inversion h.
  - inversion h.
  - f_equal; apply Pos_compare_eq_eq; exact h.
  - inversion h.
  - inversion h.
  - inversion h.
  - unfold CompOpp in h; destruct (Pos.compare p p0) eqn:hc; simpl in h.
    + f_equal; apply Pos_compare_eq_eq; exact hc.
    + inversion h.
    + inversion h.
Qed.

(* ── Z ordering lemmas ─────────────────────────────────────── *)

Lemma Zle_refl (x : Z) : Z.le x x.
Proof. unfold Z.le; rewrite Zcompare_self; discriminate. Qed.

Lemma Zlt_not_le (x y : Z) (h : Z.lt x y) : ~(Z.le y x).
Proof.
  unfold Z.lt, Z.le. intro hle.
  assert (h' : Z.compare y x = Gt) by exact (Zcompare_antisym_lt x y h).
  rewrite h' in hle; exact (hle eq_refl).
Qed.

Lemma Znlt_ge (x y : Z) (h : ~(Z.lt x y)) : Z.le y x.
Proof.
  unfold Z.lt, Z.le.
  refine (match (Z.compare x y) as c return (c = Z.compare x y -> Z.compare y x <> Gt) with
  | Eq => fun hc => _
  | Lt => fun hc => False_rect _ (h (eq_sym hc))
  | Gt => fun hc => _
  end (eq_refl (Z.compare x y))).
  - rewrite (Zcompare_eq x y (eq_sym hc)); rewrite Zcompare_self; discriminate.
  - rewrite (Zcompare_antisym_gt x y (eq_sym hc)); discriminate.
Qed.

(* ── Decidable equality / ordering ──────────────────────────── *)

Definition Z_lt_dec (x y : Z) : {Z.lt x y} + {Z.ge x y}.
Proof.
  unfold Z.lt, Z.ge.
  refine (match (Z.compare x y) as c return (c = Z.compare x y -> {Z.compare x y = Lt} + {Z.compare x y <> Lt}) with
  | Eq => fun hc => right (_ : Z.compare x y <> Lt)
  | Lt => fun hc => left (_ : Z.compare x y = Lt)
  | Gt => fun hc => right (_ : Z.compare x y <> Lt)
  end (eq_refl (Z.compare x y))).
  - rewrite (eq_sym hc); discriminate.
  - exact (eq_sym hc).
  - rewrite (eq_sym hc); discriminate.
Defined.

Definition Z_eq_dec (x y : Z) : {x = y} + {x <> y}.
Proof.
  refine (match (Z.compare x y) as c return (c = Z.compare x y -> {x = y} + {x <> y}) with
  | Eq => fun hc => left (Zcompare_eq x y (eq_sym hc))
  | Lt => fun hc => right (fun hx => _)
  | Gt => fun hc => right (fun hx => _)
  end (eq_refl (Z.compare x y))).
  - subst x; rewrite Zcompare_self in hc; inversion hc.
  - subst x; rewrite Zcompare_self in hc; inversion hc.
Defined.

(* ── Ring lemmas (using fully qualified Z.*, not infix notation) *)

Lemma Zadd_comm (x y : Z) : Z.add x y = Z.add y x.
Proof.
  unfold Z.add; destruct x, y; simpl; auto; f_equal; apply Pos_add_comm.
Qed.

Lemma pos_sub_diag (p : positive) : Z.pos_sub p p = Z0.
Proof.
  induction p as [p IH | p IH | ].
  - simpl. rewrite IH. simpl. reflexivity.
  - simpl. rewrite IH. simpl. reflexivity.
  - reflexivity.
Qed.

Lemma Zsub_diag (x : Z) : Z.sub x x = Z0.
Proof.
  unfold Z.sub, Z.opp; destruct x; simpl; auto.
  - apply pos_sub_diag.
  - apply pos_sub_diag.
Qed.

Lemma Zmul_comm (x y : Z) : Z.mul x y = Z.mul y x.
Proof.
  unfold Z.mul; destruct x, y; simpl; auto; f_equal; apply Pos_mul_comm.
Qed.