diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-23 14:12:04 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-23 14:12:04 +0200 |
commit | b66ddea9b0304d390b56afadda80fa4d2f2184d6 (patch) | |
tree | 27a2ad0533fcd52a0d82b92ea3f582a3c02065d9 /lib/Coqlib.v | |
parent | 23f871b3faf89679414485c438ed211151bd99ce (diff) | |
download | compcert-b66ddea9b0304d390b56afadda80fa4d2f2184d6.tar.gz compcert-b66ddea9b0304d390b56afadda80fa4d2f2184d6.zip |
Replace nat_of_Z with Z.to_nat
Use Z.to_nat theorems from the standard Coq library in preference to
our theorems in lib/Coqlib.v.
Simplify lib/Coqlib.v accordingly.
Diffstat (limited to 'lib/Coqlib.v')
-rw-r--r-- | lib/Coqlib.v | 37 |
1 files changed, 7 insertions, 30 deletions
diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 3b8e5b3b..90e0b89d 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -577,43 +577,20 @@ Qed. (** Conversion from [Z] to [nat]. *) -Definition nat_of_Z: Z -> nat := Z.to_nat. - -Lemma nat_of_Z_of_nat: - forall n, nat_of_Z (Z.of_nat n) = n. -Proof. - exact Nat2Z.id. -Qed. - -Lemma nat_of_Z_max: - forall z, Z.of_nat (nat_of_Z z) = Z.max z 0. -Proof. - intros. unfold Z.max. destruct z; simpl; auto. - change (Z.of_nat (Z.to_nat (Zpos p)) = Zpos p). - apply Z2Nat.id. compute; intuition congruence. -Qed. - -Lemma nat_of_Z_eq: - forall z, z >= 0 -> Z.of_nat (nat_of_Z z) = z. -Proof. - unfold nat_of_Z; intros. apply Z2Nat.id. omega. -Qed. - -Lemma nat_of_Z_neg: - forall n, n <= 0 -> nat_of_Z n = O. +Lemma Z_to_nat_neg: + forall n, n <= 0 -> Z.to_nat n = O. Proof. destruct n; unfold Z.le; simpl; auto. congruence. Qed. -Lemma nat_of_Z_plus: - forall p q, - p >= 0 -> q >= 0 -> - nat_of_Z (p + q) = (nat_of_Z p + nat_of_Z q)%nat. +Lemma Z_to_nat_max: + forall z, Z.of_nat (Z.to_nat z) = Z.max z 0. Proof. - unfold nat_of_Z; intros. apply Z2Nat.inj_add; omega. + intros. destruct (zle 0 z). +- rewrite Z2Nat.id by auto. xomega. +- rewrite Z_to_nat_neg by omega. xomega. Qed. - (** Alignment: [align n amount] returns the smallest multiple of [amount] greater than or equal to [n]. *) |