numbers.v 7.66 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
Coercion Z.of_nat : nat >-> Z.

11 12 13 14 15
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).

16
Infix "≤" := le : nat_scope.
17 18 19 20 21 22 23 24 25 26
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
27
Instance nat_eq_dec:  x y : nat, Decision (x = y) := eq_nat_dec.
28 29
Instance nat_le_dec:  x y : nat, Decision (x  y) := le_dec.
Instance nat_lt_dec:  x y : nat, Decision (x < y) := lt_dec.
30
Instance nat_inhabited: Inhabited nat := populate 0%nat.
31 32 33 34 35 36

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
37 38 39 40 41 42 43 44
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
45
Instance positive_eq_dec:  x y : positive, Decision (x = y) := Pos.eq_dec.
46 47
Instance positive_inhabited: Inhabited positive := populate 1%positive.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54 55
Instance: Injective (=) (=) xO.
Proof. by injection 1. Qed.
Instance: Injective (=) (=) xI.
Proof. by injection 1. Qed.

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

64 65 66
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
67 68 69
Instance: Injective (=) (=) Npos.
Proof. by injection 1. Qed.

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

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

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

101
(** * Conversions *)
102 103
(** The function [Z_to_option_N] converts an integer [x] into a natural number
by giving [None] in case [x] is negative. *)
104
Definition Z_to_option_N (x : Z) : option N :=
Robbert Krebbers's avatar
Robbert Krebbers committed
105 106 107 108 109
  match x with
  | Z0 => Some N0
  | Zpos p => Some (Npos p)
  | Zneg _ => None
  end.
110 111 112 113 114 115
Definition Z_to_option_nat (x : Z) : option nat :=
  match x with
  | Z0 => Some 0
  | Zpos p => Some (Pos.to_nat p)
  | Zneg _ => None
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 153
Lemma Z_to_option_N_Some x y :
  Z_to_option_N x = Some y  (0  x)%Z  y = Z.to_N x.
Proof.
  split.
  * intros. by destruct x; simpl in *; simplify_equality;
      auto using Zle_0_pos.
  * intros [??]. subst. destruct x; simpl; auto; lia.
Qed.
Lemma Z_to_option_N_Some_alt x y :
  Z_to_option_N x = Some y  (0  x)%Z  x = Z.of_N y.
Proof.
  rewrite Z_to_option_N_Some.
  split; intros [??]; subst; auto using N2Z.id, Z2N.id, eq_sym.
Qed.

Lemma Z_to_option_nat_Some x y :
  Z_to_option_nat x = Some y  (0  x)%Z  y = Z.to_nat x.
Proof.
  split.
  * intros. by destruct x; simpl in *; simplify_equality;
      auto using Zle_0_pos.
  * intros [??]. subst. destruct x; simpl; auto; lia.
Qed.
Lemma Z_to_option_nat_Some_alt x y :
  Z_to_option_nat x = Some y  (0  x)%Z  x = Z.of_nat y.
Proof.
  rewrite Z_to_option_nat_Some.
  split; intros [??]; subst; auto using Nat2Z.id, Z2Nat.id, eq_sym.
Qed.
Lemma Z_to_option_of_nat x :
  Z_to_option_nat (Z.of_nat x) = Some x.
Proof. apply Z_to_option_nat_Some_alt. auto using Nat2Z.is_nonneg. Qed.

(** The function [Z_of_sumbool] converts a sumbool [P] into an integer
by yielding one if [P] and zero if [Q]. *)
Definition Z_of_sumbool {P Q : Prop} (p : {P} + {Q}) : Z :=
  (if p then 1 else 0)%Z.
154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211

(** 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.