numbers.v 2.36 KB
Newer Older
1 2
(* Copyright (c) 2012, Robbert Krebbers. *)
(* This file is distributed under the terms of the BSD license. *)
3 4 5
(** This file collects some trivial facts on the Coq types [nat] and [N] for
natural numbers, and the type [Z] for integers. It also declares some useful
notations. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Require Export PArith NArith ZArith.
7
Require Export base decidable.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
Infix "≤" := le : nat_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Instance nat_eq_dec:  x y : nat, Decision (x = y) := eq_nat_dec.
11 12 13 14 15 16

Lemma lt_n_SS n : n < S (S n).
Proof. auto with arith. Qed.
Lemma lt_n_SSS n : n < S (S (S n)).
Proof. auto with arith. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
17 18 19 20 21 22
Instance positive_eq_dec:  x y : positive, Decision (x = y) := Pos.eq_dec.
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

Infix "≤" := N.le : N_scope.
Notation "(≤)" := N.le (only parsing) : N_scope.
23
Notation "(<)" := N.lt (only parsing) : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
24 25 26 27 28 29 30 31

Instance N_eq_dec:  x y : N, Decision (x = y) := N.eq_dec.
Program Instance N_le_dec (x y : N) : Decision (x  y)%N :=
  match Ncompare x y with
  | Gt => right _
  | _ => left _
  end.
Next Obligation. congruence. Qed.
32 33 34 35 36 37
Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
  match Ncompare x y with
  | Lt => left _
  | _ => right _
  end.
Next Obligation. congruence. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
38 39 40

Infix "≤" := Z.le : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
41
Notation "(<)" := Z.lt (only parsing) : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
Instance Z_eq_dec:  x y : Z, Decision (x = y) := Z.eq_dec.
Instance Z_le_dec:  x y : Z, Decision (x  y)%Z := Z_le_dec.
44
Instance Z_lt_dec:  x y : Z, Decision (x < y)%Z := Z_lt_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
45

46
(** * Conversions *)
47 48
(** The function [Z_to_option_N] converts an integer [x] into a natural number
by giving [None] in case [x] is negative. *)
49
Definition Z_to_option_N (x : Z) : option N :=
Robbert Krebbers's avatar
Robbert Krebbers committed
50 51 52 53 54 55
  match x with
  | Z0 => Some N0
  | Zpos p => Some (Npos p)
  | Zneg _ => None
  end.

56 57 58 59 60
(** The function [Z_decide] converts a decidable proposition [P] into an integer
by yielding one if [P] holds and zero if [P] does not. *)
Definition Z_decide (P : Prop) {dec : Decision P} : Z :=
  (if dec then 1 else 0)%Z.

61 62
(** The function [Z_decide_rel] is the more efficient variant of [Z_decide] when
used for binary relations. It yields one if [R x y] and zero if not [R x y]. *)
63 64 65
Definition Z_decide_rel {A B} (R : A  B  Prop)
    {dec :  x y, Decision (R x y)} (x : A) (y : B) : Z :=
  (if dec x y then 1 else 0)%Z.