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
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
Instance nat_inhabited: Inhabited nat := populate 0%nat.
29 30 31 32 33 34

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
35 36 37 38 39 40 41 42
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.

Robbert Krebbers's avatar
Robbert Krebbers committed
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
Notation "(<)" := N.lt (only parsing) : N_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
61

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

Robbert Krebbers's avatar
Robbert Krebbers committed
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
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.
81
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
Notation "(<)" := Z.lt (only parsing) : Z_scope.
90

Robbert Krebbers's avatar
Robbert Krebbers committed
91 92 93
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
Instance Z_lt_dec:  x y : Z, Decision (x < y)%Z := Z_lt_dec.
97
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
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.
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 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176

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