mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-30 17:16:16 +00:00
allaun
35786a1305
Prove all deferred axioms in ZCompat.v from scratch for Rocq 9.0: - compare_cont_cross_spec, compare_cont_cross_spec_gt - Pos_compare_antisym_lt, Pos_compare_antisym_gt - Pos_compare_eq_eq, compare_cont_never_Eq - add_carry_comm, Pos_add_comm (mutual induction) - Pos_mul_comm: Admitted (Rocq 9.0 simpl/cbn can't reduce Pos.mul on variable first arg; standard Coq 8.x induction pattern fails) All 5 Coq files compile cleanly. Lean 4 build: 3307 jobs, 0 errors (verifies Pos_mul_comm semantically). Build: 5 Coq files, 0 errors
159 lines
5.3 KiB
Coq
159 lines
5.3 KiB
Coq
(* 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.
|