numbers.v 6.09 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 10 11 12 13
Reserved Notation "x ≤ y ≤ z" (at level 70, y at next level).
Reserved Notation "x ≤ y < z" (at level 70, y at next level).
Reserved Notation "x < y < z" (at level 70, y at next level).
Reserved Notation "x < y ≤ z" (at level 70, y at next level).

14
Infix "≤" := le : nat_scope.
15 16 17 18 19 20 21 22 23 24
Notation "x ≤ y ≤ z" := (x  y  y  z)%nat : nat_scope.
Notation "x ≤ y < z" := (x  y  y < z)%nat : nat_scope.
Notation "x < y < z" := (x < y  y < z)%nat : nat_scope.
Notation "x < y ≤ z" := (x < y  y  z)%nat : nat_scope.
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.

Infix "`div`" := NPeano.div (at level 35) : nat_scope.
Infix "`mod`" := NPeano.modulo (at level 35) : nat_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Instance nat_eq_dec:  x y : nat, Decision (x = y) := eq_nat_dec.
26 27
Instance nat_le_dec:  x y : nat, Decision (x  y) := le_dec.
Instance nat_lt_dec:  x y : nat, Decision (x < y) := lt_dec.
28 29 30 31 32 33

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
34 35 36 37 38
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.
39 40 41 42
Notation "x ≤ y ≤ z" := (x  y  y  z)%N : N_scope.
Notation "x ≤ y < z" := (x  y  y < z)%N : N_scope.
Notation "x < y < z" := (x < y  y < z)%N : N_scope.
Notation "x < y ≤ z" := (x < y  y  z)%N : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
Notation "(≤)" := N.le (only parsing) : N_scope.
44
Notation "(<)" := N.lt (only parsing) : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
45

46 47 48
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
49 50 51 52 53 54 55
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.
56 57 58 59 60 61
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
62 63

Infix "≤" := Z.le : Z_scope.
64 65 66 67
Notation "x ≤ y ≤ z" := (x  y  y  z)%Z : Z_scope.
Notation "x ≤ y < z" := (x  y  y < z)%Z : Z_scope.
Notation "x < y < z" := (x < y  y < z)%Z : Z_scope.
Notation "x < y ≤ z" := (x < y  y  z)%Z : Z_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Notation "(≤)" := Z.le (only parsing) : Z_scope.
69
Notation "(<)" := Z.lt (only parsing) : Z_scope.
70

Robbert Krebbers's avatar
Robbert Krebbers committed
71 72
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.
73
Instance Z_lt_dec:  x y : Z, Decision (x < y)%Z := Z_lt_dec.
Robbert Krebbers's avatar
Robbert Krebbers committed
74

75
(** * Conversions *)
76 77
(** The function [Z_to_option_N] converts an integer [x] into a natural number
by giving [None] in case [x] is negative. *)
78
Definition Z_to_option_N (x : Z) : option N :=
Robbert Krebbers's avatar
Robbert Krebbers committed
79 80 81 82 83 84
  match x with
  | Z0 => Some N0
  | Zpos p => Some (Npos p)
  | Zneg _ => None
  end.

85 86 87 88 89
(** 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.

90 91
(** 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]. *)
92 93 94
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.
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152

(** Some correspondence lemmas between [nat] and [N] that are not part of the
standard library. We declare a hint database [natify] to rewrite a goal
involving [N] into a corresponding variant involving [nat]. *)
Lemma N_to_nat_lt x y : N.to_nat x < N.to_nat y  (x < y)%N.
Proof. by rewrite <-N.compare_lt_iff, nat_compare_lt, N2Nat.inj_compare. Qed.
Lemma N_to_nat_le x y : N.to_nat x  N.to_nat y  (x  y)%N.
Proof. by rewrite <-N.compare_le_iff, nat_compare_le, N2Nat.inj_compare. Qed.
Lemma N_to_nat_0 : N.to_nat 0 = 0.
Proof. done. Qed.
Lemma N_to_nat_1 : N.to_nat 1 = 1.
Proof. done. Qed.
Lemma N_to_nat_div x y : N.to_nat (x `div` y) = N.to_nat x `div` N.to_nat y.
Proof.
  destruct (decide (y = 0%N)).
  { subst. by destruct x. }
  apply NPeano.Nat.div_unique with (N.to_nat (x `mod` y)).
  { by apply N_to_nat_lt, N.mod_lt. }
  rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
  by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
Qed.
(* We have [x `mod` 0 = 0] on [nat], and [x `mod` 0 = x] on [N]. *)
Lemma N_to_nat_mod x y :
  y  0%N 
  N.to_nat (x `mod` y) = N.to_nat x `mod` N.to_nat y.
Proof.
  intros.
  apply NPeano.Nat.mod_unique with (N.to_nat (x `div` y)).
  { by apply N_to_nat_lt, N.mod_lt. }
  rewrite (N.div_unique_exact (x * y) y x), N.div_mul by lia.
  by rewrite <-N2Nat.inj_mul, <-N2Nat.inj_add, <-N.div_mod.
Qed.

Hint Rewrite <-N2Nat.inj_iff : natify.
Hint Rewrite <-N_to_nat_lt : natify.
Hint Rewrite <-N_to_nat_le : natify.
Hint Rewrite Nat2N.id : natify.
Hint Rewrite N2Nat.inj_add : natify.
Hint Rewrite N2Nat.inj_mul : natify.
Hint Rewrite N2Nat.inj_sub : natify.
Hint Rewrite N2Nat.inj_succ : natify.
Hint Rewrite N2Nat.inj_pred : natify.
Hint Rewrite N_to_nat_div : natify.
Hint Rewrite N_to_nat_0 : natify.
Hint Rewrite N_to_nat_1 : natify.
Ltac natify := repeat autorewrite with natify in *.

Hint Extern 100 (Nlt _ _) => natify : natify.
Hint Extern 100 (Nle _ _) => natify : natify.
Hint Extern 100 (@eq N _ _) => natify : natify.
Hint Extern 100 (lt _ _) => natify : natify.
Hint Extern 100 (le _ _) => natify : natify.
Hint Extern 100 (@eq nat _ _) => natify : natify.

Instance:  x, PropHolds (0 < x)%N  PropHolds (0 < N.to_nat x).
Proof. unfold PropHolds. intros. by natify. Qed.
Instance:  x, PropHolds (0  x)%N  PropHolds (0  N.to_nat x).
Proof. unfold PropHolds. intros. by natify. Qed.