numbers.v 6.77 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
8
9
10
11
12
Require Export base decidable.

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).
Robbert Krebbers's avatar
Robbert Krebbers committed
13

14
Infix "≤" := le : nat_scope.
15
16
17
18
19
20
21
22
23
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.
24

Robbert Krebbers's avatar
Robbert Krebbers committed
25
Instance nat_eq_dec:  x y : nat, Decision (x = y) := eq_nat_dec.
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
Instance nat_le_dec:  x y : nat, Decision (x  y) := le_dec.
Instance nat_lt_dec:  x y : nat, Decision (x < y) := lt_dec.
Instance nat_inhabited: Inhabited nat := populate 0%nat.

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.

Definition sum_list_with {A} (f : A  nat) : list A  nat :=
  fix go l :=
  match l with
  | [] => 0
  | x :: l => f x + go l
  end.
Notation sum_list := (sum_list_with id).

Robbert Krebbers's avatar
Robbert Krebbers committed
43
Instance positive_eq_dec:  x y : positive, Decision (x = y) := Pos.eq_dec.
44
45
Instance positive_inhabited: Inhabited positive := populate 1%positive.

Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.

49
50
51
52
53
Instance: Injective (=) (=) xO.
Proof. by injection 1. Qed.
Instance: Injective (=) (=) xI.
Proof. by injection 1. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
54
Infix "≤" := N.le : N_scope.
55
56
57
58
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
59
Notation "(≤)" := N.le (only parsing) : N_scope.
60
61
62
63
64
65
66
Notation "(<)" := N.lt (only parsing) : N_scope.

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

Instance: Injective (=) (=) Npos.
Proof. by injection 1. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
67
68
69
70
71
72
73
74

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.
75
76
77
78
79
80
81
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.
Instance N_inhabited: Inhabited N := populate 1%N.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83

Infix "≤" := Z.le : Z_scope.
84
85
86
87
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
88
Notation "(≤)" := Z.le (only parsing) : Z_scope.
89
90
91
92
93
Notation "(<)" := Z.lt (only parsing) : Z_scope.

Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
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.
96
97
Instance Z_lt_dec:  x y : Z, Decision (x < y)%Z := Z_lt_dec.
Instance Z_inhabited: Inhabited Z := populate 1%Z.
Robbert Krebbers's avatar
Robbert Krebbers committed
98

99
(** * Conversions *)
100
101
(** The function [Z_to_option_N] converts an integer [x] into a natural number
by giving [None] in case [x] is negative. *)
102
Definition Z_to_option_N (x : Z) : option N :=
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
106
107
108
  match x with
  | Z0 => Some N0
  | Zpos p => Some (Npos p)
  | Zneg _ => None
  end.

109
110
111
112
113
(** 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.

114
115
(** 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]. *)
116
117
118
119
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.

120
121
122
123
124
125
126
127
128
129
130
131
(** 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof.
133
134
135
136
137
138
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
Qed.
140
141
142
143
(* 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.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
Proof.
145
146
147
148
149
  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.
Robbert Krebbers's avatar
Robbert Krebbers committed
150
151
Qed.

152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
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.