# Library Coq.ZArith.Zcompare

``` ```
Binary Integers (Pierre Crégut, CNET, Lannion, France)
``` Require Export BinPos. Require Export BinInt. Require Import Lt. Require Import Gt. Require Import Plus. Require Import Mult. Open Local Scope Z_scope. ```

# Comparison on integers

``` Lemma Zcompare_refl : forall n:Z, (n ?= n) = Eq. Proof.   intro x; destruct x as [| p| p]; simpl in |- *;     [ reflexivity | apply Pcompare_refl | rewrite Pcompare_refl; reflexivity ]. Qed. Lemma Zcompare_Eq_eq : forall n m:Z, (n ?= m) = Eq -> n = m. Proof.   intros x y; destruct x as [| x'| x']; destruct y as [| y'| y']; simpl in |- *;     intro H; reflexivity || (try discriminate H);       [ rewrite (Pcompare_Eq_eq x' y' H); reflexivity         | rewrite (Pcompare_Eq_eq x' y');           [ reflexivity | destruct ((x' ?= y')%positive Eq); reflexivity || discriminate ] ]. Qed. Lemma Zcompare_Eq_iff_eq : forall n m:Z, (n ?= m) = Eq <-> n = m. Proof.   intros x y; split; intro E;     [ apply Zcompare_Eq_eq; assumption | rewrite E; apply Zcompare_refl ]. Qed. Lemma Zcompare_antisym : forall n m:Z, CompOpp (n ?= m) = (m ?= n). Proof.   intros x y; destruct x; destruct y; simpl in |- *;     reflexivity || discriminate H || rewrite Pcompare_antisym;       reflexivity. Qed. Lemma Zcompare_Gt_Lt_antisym : forall n m:Z, (n ?= m) = Gt <-> (m ?= n) = Lt. Proof.   intros x y; split; intro H;     [ change Lt with (CompOpp Gt) in |- *; rewrite <- Zcompare_antisym; rewrite H; reflexivity | change Gt with (CompOpp Lt) in |- *; rewrite <- Zcompare_antisym; rewrite H; reflexivity ]. Qed. ```

# Transitivity of comparison

``` Lemma Zcompare_Gt_trans :   forall n m p:Z, (n ?= m) = Gt -> (m ?= p) = Gt -> (n ?= p) = Gt. Proof.   intros x y z; case x; case y; case z; simpl in |- *;     try (intros; discriminate H || discriminate H0); auto with arith;       [ intros p q r H H0; apply nat_of_P_gt_Gt_compare_complement_morphism;         unfold gt in |- *; apply lt_trans with (m := nat_of_P q);           apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;             assumption         | intros p q r; do 3 rewrite <- ZC4; intros H H0;           apply nat_of_P_gt_Gt_compare_complement_morphism;             unfold gt in |- *; apply lt_trans with (m := nat_of_P q);               apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;                 assumption ]. Qed. ```

# Comparison and opposite

``` Lemma Zcompare_opp : forall n m:Z, (n ?= m) = (- m ?= - n). Proof.   intros x y; case x; case y; simpl in |- *; auto with arith; intros;     rewrite <- ZC4; trivial with arith. Qed. Hint Local Resolve Pcompare_refl. ```

# Comparison first-order specification

``` Lemma Zcompare_Gt_spec :   forall n m:Z, (n ?= m) = Gt -> exists h : positive, n + - m = Zpos h. Proof.   intros x y; case x; case y;     [ simpl in |- *; intros H; discriminate H | simpl in |- *; intros p H; discriminate H | intros p H; exists p; simpl in |- *; auto with arith | intros p H; exists p; simpl in |- *; auto with arith | intros q p H; exists (p - q)%positive; unfold Zplus, Zopp in |- *; unfold Zcompare in H; rewrite H; trivial with arith | intros q p H; exists (p + q)%positive; simpl in |- *; trivial with arith | simpl in |- *; intros p H; discriminate H | simpl in |- *; intros q p H; discriminate H | unfold Zcompare in |- *; intros q p; rewrite <- ZC4; intros H; exists (q - p)%positive; simpl in |- *; rewrite (ZC1 q p H); trivial with arith ]. Qed. ```

# Comparison and addition

``` Lemma weaken_Zcompare_Zplus_compatible :   (forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m)) ->   forall n m p:Z, (p + n ?= p + m) = (n ?= m). Proof.   intros H x y z; destruct z;     [ reflexivity | apply H | rewrite (Zcompare_opp x y); rewrite Zcompare_opp; do 2 rewrite Zopp_plus_distr; rewrite Zopp_neg; apply H ]. Qed. Hint Local Resolve ZC4. Lemma weak_Zcompare_Zplus_compatible :   forall (n m:Z) (p:positive), (Zpos p + n ?= Zpos p + m) = (n ?= m). Proof.   intros x y z; case x; case y; simpl in |- *; auto with arith;     [ intros p; apply nat_of_P_lt_Lt_compare_complement_morphism; apply ZL17       | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith;         apply nat_of_P_gt_Gt_compare_complement_morphism;           rewrite nat_of_P_minus_morphism;             [ unfold gt in |- *; apply ZL16 | assumption ]       | intros p; ElimPcompare z p; intros E; auto with arith;         apply nat_of_P_gt_Gt_compare_complement_morphism;           unfold gt in |- *; apply ZL17       | intros p q; ElimPcompare q p; intros E; rewrite E;         [ rewrite (Pcompare_Eq_eq q p E); apply Pcompare_refl           | apply nat_of_P_lt_Lt_compare_complement_morphism;             do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l;               apply nat_of_P_lt_Lt_compare_morphism with (1 := E)           | apply nat_of_P_gt_Gt_compare_complement_morphism; unfold gt in |- *;             do 2 rewrite nat_of_P_plus_morphism; apply plus_lt_compat_l;               exact (nat_of_P_gt_Gt_compare_morphism q p E) ]       | intros p q; ElimPcompare z p; intros E; rewrite E; auto with arith;         apply nat_of_P_gt_Gt_compare_complement_morphism;           rewrite nat_of_P_minus_morphism;             [ unfold gt in |- *; apply lt_trans with (m := nat_of_P z);               [ apply ZL16 | apply ZL17 ]               | assumption ]       | intros p; ElimPcompare z p; intros E; rewrite E; auto with arith;         simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;           rewrite nat_of_P_minus_morphism; [ apply ZL16 | assumption ]       | intros p q; ElimPcompare z q; intros E; rewrite E; auto with arith;         simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;           rewrite nat_of_P_minus_morphism;             [ apply lt_trans with (m := nat_of_P z); [ apply ZL16 | apply ZL17 ]               | assumption ]       | intros p q; ElimPcompare z q; intros E0; rewrite E0; ElimPcompare z p;         intros E1; rewrite E1; ElimPcompare q p; intros E2;           rewrite E2; auto with arith;             [ absurd ((q ?= p)%positive Eq = Lt);               [ rewrite <- (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z); discriminate | assumption ]               | absurd ((q ?= p)%positive Eq = Gt);                 [ rewrite <- (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq z p E1); rewrite (Pcompare_refl z); discriminate | assumption ]               | absurd ((z ?= p)%positive Eq = Lt);                 [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2); rewrite (Pcompare_refl q); discriminate | assumption ]               | absurd ((z ?= p)%positive Eq = Lt);                 [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate | assumption ]               | absurd ((z ?= p)%positive Eq = Gt);                 [ rewrite (Pcompare_Eq_eq z q E0); rewrite <- (Pcompare_Eq_eq q p E2); rewrite (Pcompare_refl q); discriminate | assumption ]               | absurd ((z ?= p)%positive Eq = Gt);                 [ rewrite (Pcompare_Eq_eq z q E0); rewrite E2; discriminate | assumption ]               | absurd ((z ?= q)%positive Eq = Lt);                 [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2); rewrite (Pcompare_refl p); discriminate | assumption ]               | absurd ((p ?= q)%positive Eq = Gt);                 [ rewrite <- (Pcompare_Eq_eq z p E1); rewrite E0; discriminate | apply ZC2; assumption ]               | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2);                 rewrite (Pcompare_refl (p - z)); auto with arith               | simpl in |- *; rewrite <- ZC4;                 apply nat_of_P_gt_Gt_compare_complement_morphism;                   rewrite nat_of_P_minus_morphism;                     [ rewrite nat_of_P_minus_morphism;                       [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z);                         rewrite le_plus_minus_r;                           [ rewrite le_plus_minus_r;                             [ apply nat_of_P_lt_Lt_compare_morphism; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; assumption ]                             | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;                               assumption ]                         | apply ZC2; assumption ]                       | apply ZC2; assumption ]               | simpl in |- *; rewrite <- ZC4;                 apply nat_of_P_lt_Lt_compare_complement_morphism;                   rewrite nat_of_P_minus_morphism;                     [ rewrite nat_of_P_minus_morphism;                       [ apply plus_lt_reg_l with (p := nat_of_P z);                         rewrite le_plus_minus_r;                           [ rewrite le_plus_minus_r;                             [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; assumption ]                             | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;                               assumption ]                         | apply ZC2; assumption ]                       | apply ZC2; assumption ]               | absurd ((z ?= q)%positive Eq = Lt);                 [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate | assumption ]               | absurd ((q ?= p)%positive Eq = Lt);                 [ cut ((q ?= p)%positive Eq = Gt);                   [ intros E; rewrite E; discriminate                     | apply nat_of_P_gt_Gt_compare_complement_morphism;                       unfold gt in |- *; apply lt_trans with (m := nat_of_P z);                         [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ]                   | assumption ]               | absurd ((z ?= q)%positive Eq = Gt);                 [ rewrite (Pcompare_Eq_eq z p E1); rewrite (Pcompare_Eq_eq q p E2); rewrite (Pcompare_refl p); discriminate | assumption ]               | absurd ((z ?= q)%positive Eq = Gt);                 [ rewrite (Pcompare_Eq_eq z p E1); rewrite ZC1;                   [ discriminate | assumption ]                   | assumption ]               | absurd ((z ?= q)%positive Eq = Gt);                 [ rewrite (Pcompare_Eq_eq q p E2); rewrite E1; discriminate | assumption ]               | absurd ((q ?= p)%positive Eq = Gt);                 [ rewrite ZC1;                   [ discriminate                     | apply nat_of_P_gt_Gt_compare_complement_morphism;                       unfold gt in |- *; apply lt_trans with (m := nat_of_P z);                         [ apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption | apply nat_of_P_lt_Lt_compare_morphism; assumption ] ]                   | assumption ]               | simpl in |- *; rewrite (Pcompare_Eq_eq q p E2); apply Pcompare_refl               | simpl in |- *; apply nat_of_P_gt_Gt_compare_complement_morphism;                 unfold gt in |- *; rewrite nat_of_P_minus_morphism;                   [ rewrite nat_of_P_minus_morphism;                     [ apply plus_lt_reg_l with (p := nat_of_P p);                       rewrite le_plus_minus_r;                         [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P q);                           rewrite plus_assoc; rewrite le_plus_minus_r;                             [ rewrite (plus_comm (nat_of_P q)); apply plus_lt_compat_l; apply nat_of_P_lt_Lt_compare_morphism; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption ]                           | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;                             apply ZC1; assumption ]                       | assumption ]                     | assumption ]               | simpl in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism;                 rewrite nat_of_P_minus_morphism;                   [ rewrite nat_of_P_minus_morphism;                     [ apply plus_lt_reg_l with (p := nat_of_P q);                       rewrite le_plus_minus_r;                         [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);                           rewrite plus_assoc; rewrite le_plus_minus_r;                             [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption ]                           | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;                             apply ZC1; assumption ]                       | assumption ]                     | assumption ] ] ]. Qed. Lemma Zcompare_plus_compat : forall n m p:Z, (p + n ?= p + m) = (n ?= m). Proof.   exact (weaken_Zcompare_Zplus_compatible weak_Zcompare_Zplus_compatible). Qed. Lemma Zplus_compare_compat :   forall (r:comparison) (n m p q:Z),     (n ?= m) = r -> (p ?= q) = r -> (n + p ?= m + q) = r. Proof.   intros r x y z t; case r;     [ intros H1 H2; elim (Zcompare_Eq_iff_eq x y); elim (Zcompare_Eq_iff_eq z t);       intros H3 H4 H5 H6; rewrite H3;         [ rewrite H5;           [ elim (Zcompare_Eq_iff_eq (y + t) (y + t)); auto with arith | auto with arith ]           | auto with arith ]       | intros H1 H2; elim (Zcompare_Gt_Lt_antisym (y + t) (x + z)); intros H3 H4;         apply H3; apply Zcompare_Gt_trans with (m := y + z);           [ rewrite Zcompare_plus_compat; elim (Zcompare_Gt_Lt_antisym t z); auto with arith | do 2 rewrite <- (Zplus_comm z); rewrite Zcompare_plus_compat; elim (Zcompare_Gt_Lt_antisym y x); auto with arith ]       | intros H1 H2; apply Zcompare_Gt_trans with (m := x + t);         [ rewrite Zcompare_plus_compat; assumption | do 2 rewrite <- (Zplus_comm t); rewrite Zcompare_plus_compat; assumption ] ]. Qed. Lemma Zcompare_succ_Gt : forall n:Z, (Zsucc n ?= n) = Gt. Proof.   intro x; unfold Zsucc in |- *; pattern x at 2 in |- *;     rewrite <- (Zplus_0_r x); rewrite Zcompare_plus_compat;       reflexivity. Qed. Lemma Zcompare_Gt_not_Lt : forall n m:Z, (n ?= m) = Gt <-> (n ?= m + 1) <> Lt. Proof.   intros x y; split;     [ intro H; elim_compare x (y + 1);       [ intro H1; rewrite H1; discriminate         | intros H1; elim Zcompare_Gt_spec with (1 := H); intros h H2;           absurd ((nat_of_P h > 0)%nat /\ (nat_of_P h < 1)%nat);             [ unfold not in |- *; intros H3; elim H3; intros H4 H5;               absurd (nat_of_P h > 0)%nat;                 [ unfold gt in |- *; apply le_not_lt; apply le_S_n; exact H5 | assumption ]               | split;                 [ elim (ZL4 h); intros i H3; rewrite H3; apply gt_Sn_O                   | change (nat_of_P h < nat_of_P 1)%nat in |- *;                     apply nat_of_P_lt_Lt_compare_morphism;                       change ((Zpos h ?= 1) = Lt) in |- *; rewrite <- H2;                         rewrite <- (fun m n:Z => Zcompare_plus_compat m n y);                           rewrite (Zplus_comm x); rewrite Zplus_assoc;                             rewrite Zplus_opp_r; simpl in |- *; exact H1 ] ]         | intros H1; rewrite H1; discriminate ]       | intros H; elim_compare x (y + 1);         [ intros H1; elim (Zcompare_Eq_iff_eq x (y + 1)); intros H2 H3;           rewrite (H2 H1); exact (Zcompare_succ_Gt y)           | intros H1; absurd ((x ?= y + 1) = Lt); assumption           | intros H1; apply Zcompare_Gt_trans with (m := Zsucc y);             [ exact H1 | exact (Zcompare_succ_Gt y) ] ] ]. Qed. ```

# Successor and comparison

``` Lemma Zcompare_succ_compat : forall n m:Z, (Zsucc n ?= Zsucc m) = (n ?= m). Proof.   intros n m; unfold Zsucc in |- *; do 2 rewrite (fun t:Z => Zplus_comm t 1);     rewrite Zcompare_plus_compat; auto with arith. Qed. ```

# Multiplication and comparison

``` Lemma Zcompare_mult_compat :   forall (p:positive) (n m:Z), (Zpos p * n ?= Zpos p * m) = (n ?= m). Proof.   intros x; induction x as [p H| p H| ];     [ intros y z; cut (Zpos (xI p) = Zpos p + Zpos p + 1);       [ intros E; rewrite E; do 4 rewrite Zmult_plus_distr_l;         do 2 rewrite Zmult_1_l; apply Zplus_compare_compat;           [ apply Zplus_compare_compat; apply H | trivial with arith ]         | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ]       | intros y z; cut (Zpos (xO p) = Zpos p + Zpos p);         [ intros E; rewrite E; do 2 rewrite Zmult_plus_distr_l; apply Zplus_compare_compat; apply H | simpl in |- *; rewrite (Pplus_diag p); trivial with arith ]       | intros y z; do 2 rewrite Zmult_1_l; trivial with arith ]. Qed. ```

# Reverting `x ?= y` to trichotomy

``` Lemma rename :   forall (A:Type) (P:A -> Prop) (x:A), (forall y:A, x = y -> P y) -> P x. Proof.   auto with arith. Qed. Lemma Zcompare_elim :   forall (c1 c2 c3:Prop) (n m:Z),     (n = m -> c1) ->     (n < m -> c2) ->     (n > m -> c3) -> match n ?= m with                        | Eq => c1                        | Lt => c2                        | Gt => c3                      end. Proof.   intros c1 c2 c3 x y; intros.   apply rename with (x := x ?= y); intro r; elim r;     [ intro; apply H; apply (Zcompare_Eq_eq x y); assumption | unfold Zlt in H0; assumption | unfold Zgt in H1; assumption ]. Qed. Lemma Zcompare_eq_case :   forall (c1 c2 c3:Prop) (n m:Z),     c1 -> n = m -> match n ?= m with                      | Eq => c1                      | Lt => c2                      | Gt => c3                    end. Proof.   intros c1 c2 c3 x y; intros.   rewrite H0; rewrite Zcompare_refl.   assumption. Qed. ```

# Decompose an egality between two `?=` relations into 3 implications

``` Lemma Zcompare_egal_dec :   forall n m p q:Z,     (n < m -> p < q) ->     ((n ?= m) = Eq -> (p ?= q) = Eq) ->     (n > m -> p > q) -> (n ?= m) = (p ?= q). Proof.   intros x1 y1 x2 y2.   unfold Zgt in |- *; unfold Zlt in |- *; case (x1 ?= y1); case (x2 ?= y2);     auto with arith; symmetry in |- *; auto with arith. Qed. ```

# Relating `x ?= y` to `Zle`, `Zlt`, `Zge` or `Zgt`

``` Lemma Zle_compare :   forall n m:Z,     n <= m -> match n ?= m with                 | Eq => True                 | Lt => True                 | Gt => False               end. Proof.   intros x y; unfold Zle in |- *; elim (x ?= y); auto with arith. Qed. Lemma Zlt_compare :   forall n m:Z,    n < m -> match n ?= m with               | Eq => False               | Lt => True               | Gt => False             end. Proof.   intros x y; unfold Zlt in |- *; elim (x ?= y); intros;     discriminate || trivial with arith. Qed. Lemma Zge_compare :   forall n m:Z,     n >= m -> match n ?= m with                 | Eq => True                 | Lt => False                 | Gt => True               end. Proof.   intros x y; unfold Zge in |- *; elim (x ?= y); auto with arith. Qed. Lemma Zgt_compare :   forall n m:Z,     n > m -> match n ?= m with                | Eq => False                | Lt => False                | Gt => True              end. Proof.   intros x y; unfold Zgt in |- *; elim (x ?= y); intros;     discriminate || trivial with arith. Qed. ```

# Other properties

``` Lemma Zmult_compare_compat_l :   forall n m p:Z, p > 0 -> (n ?= m) = (p * n ?= p * m). Proof.   intros x y z H; destruct z.   discriminate H.   rewrite Zcompare_mult_compat; reflexivity.   discriminate H. Qed. Lemma Zmult_compare_compat_r :   forall n m p:Z, p > 0 -> (n ?= m) = (n * p ?= m * p). Proof.   intros x y z H; rewrite (Zmult_comm x z); rewrite (Zmult_comm y z);     apply Zmult_compare_compat_l; assumption. Qed. ```