Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import BinPos BinNat PeanoNat Pnat.

Conversions from N to nat

Module N2Nat.

N.to_nat is a bijection between N and nat, with Pos.of_nat as reciprocal. See Nat2N.id below for the dual equation.

Lemma id a : N.of_nat (N.to_nat a) = a.a:N
N.of_nat (N.to_nat a) = a
Proof.a:N
N.of_nat (N.to_nat a) = a
 destruct a as [| p]; simpl; trivial.p:positive
N.of_nat (Pos.to_nat p) = N.pos p
 destruct (Pos2Nat.is_succ p) as (n,H).p:positive
n:nat
H:Pos.to_nat p = S n
N.of_nat (Pos.to_nat p) = N.pos p rewrite H.p:positive
n:nat
H:Pos.to_nat p = S n
N.of_nat (S n) = N.pos p simpl.p:positive
n:nat
H:Pos.to_nat p = S n
N.pos (Pos.of_succ_nat n) = N.pos p f_equal.p:positive
n:nat
H:Pos.to_nat p = S n
Pos.of_succ_nat n = p
 apply Pos2Nat.inj.p:positive
n:nat
H:Pos.to_nat p = S n
Pos.to_nat (Pos.of_succ_nat n) = Pos.to_nat p rewrite H.p:positive
n:nat
H:Pos.to_nat p = S n
Pos.to_nat (Pos.of_succ_nat n) = S n apply SuccNat2Pos.id_succ.
Qed.

N.to_nat is hence injective

Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'.a, a':N
N.to_nat a = N.to_nat a' -> a = a'
Proof.a, a':N
N.to_nat a = N.to_nat a' -> a = a'
 intro H.a, a':N
H:N.to_nat a = N.to_nat a'
a = a' rewrite <- (id a), <- (id a').a, a':N
H:N.to_nat a = N.to_nat a'
N.of_nat (N.to_nat a) = N.of_nat (N.to_nat a') now f_equal.
Qed.

Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'.a, a':N
N.to_nat a = N.to_nat a' <-> a = a'
Proof.a, a':N
N.to_nat a = N.to_nat a' <-> a = a'
 split.a, a':N
N.to_nat a = N.to_nat a' -> a = a'
a, a':N
a = a' -> N.to_nat a = N.to_nat a' apply inj.a, a':N
a = a' -> N.to_nat a = N.to_nat a' intros; now subst.
Qed.

Interaction of this translation and usual operations.

Lemma inj_double a : N.to_nat (N.double a) = 2*(N.to_nat a).a:N
N.to_nat (N.double a) = 2 * N.to_nat a
Proof.a:N
N.to_nat (N.double a) = 2 * N.to_nat a
 destruct a; simpl N.to_nat; trivial.p:positive
Pos.to_nat p~0 = 2 * Pos.to_nat p apply Pos2Nat.inj_xO.
Qed.

Lemma inj_succ_double a : N.to_nat (N.succ_double a) = S (2*(N.to_nat a)).a:N
N.to_nat (N.succ_double a) = S (2 * N.to_nat a)
Proof.a:N
N.to_nat (N.succ_double a) = S (2 * N.to_nat a)
 destruct a; simpl N.to_nat; trivial.p:positive
Pos.to_nat p~1 = S (2 * Pos.to_nat p) apply Pos2Nat.inj_xI.
Qed.

Lemma inj_succ a : N.to_nat (N.succ a) = S (N.to_nat a).a:N
N.to_nat (N.succ a) = S (N.to_nat a)
Proof.a:N
N.to_nat (N.succ a) = S (N.to_nat a)
 destruct a; simpl; trivial.p:positive
Pos.to_nat (Pos.succ p) = S (Pos.to_nat p) apply Pos2Nat.inj_succ.
Qed.

Lemma inj_add a a' :
  N.to_nat (a + a') = N.to_nat a + N.to_nat a'.a, a':N
N.to_nat (a + a') = N.to_nat a + N.to_nat a'
Proof.a, a':N
N.to_nat (a + a') = N.to_nat a + N.to_nat a'
 destruct a, a'; simpl; trivial.p, p0:positive
Pos.to_nat (p + p0) = Pos.to_nat p + Pos.to_nat p0 apply Pos2Nat.inj_add.
Qed.

Lemma inj_mul a a' :
  N.to_nat (a * a') = N.to_nat a * N.to_nat a'.a, a':N
N.to_nat (a * a') = N.to_nat a * N.to_nat a'
Proof.a, a':N
N.to_nat (a * a') = N.to_nat a * N.to_nat a'
 destruct a, a'; simpl; trivial.p, p0:positive
Pos.to_nat (p * p0) = Pos.to_nat p * Pos.to_nat p0 apply Pos2Nat.inj_mul.
Qed.

Lemma inj_sub a a' :
  N.to_nat (a - a') = N.to_nat a - N.to_nat a'.a, a':N
N.to_nat (a - a') = N.to_nat a - N.to_nat a'
Proof.a, a':N
N.to_nat (a - a') = N.to_nat a - N.to_nat a'
 destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial.a, a':positive
N.to_nat
  match Pos.sub_mask a a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a - Pos.to_nat a'
 destruct (Pos.compare_spec a a').a, a':positive
H:a = a'
N.to_nat
  match Pos.sub_mask a a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a - Pos.to_nat a'
a, a':positive
H:(a < a')%positive
N.to_nat
  match Pos.sub_mask a a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a - Pos.to_nat a'
a, a':positive
H:(a' < a)%positive
N.to_nat
  match Pos.sub_mask a a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a - Pos.to_nat a'
 -a, a':positive
H:a = a'
N.to_nat
  match Pos.sub_mask a a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a - Pos.to_nat a' subst.a':positive
N.to_nat
  match Pos.sub_mask a' a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a' - Pos.to_nat a' now rewrite Pos.sub_mask_diag, Nat.sub_diag.
 -a, a':positive
H:(a < a')%positive
N.to_nat
  match Pos.sub_mask a a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a - Pos.to_nat a' rewrite Pos.sub_mask_neg; trivial.a, a':positive
H:(a < a')%positive
N.to_nat 0 = Pos.to_nat a - Pos.to_nat a' apply Pos2Nat.inj_lt in H.a, a':positive
H:Pos.to_nat a < Pos.to_nat a'
N.to_nat 0 = Pos.to_nat a - Pos.to_nat a'
   simpl; symmetry; apply Nat.sub_0_le.a, a':positive
H:Pos.to_nat a < Pos.to_nat a'
Pos.to_nat a <= Pos.to_nat a' now apply Nat.lt_le_incl.
 -a, a':positive
H:(a' < a)%positive
N.to_nat
  match Pos.sub_mask a a' with
  | Pos.IsPos p => N.pos p
  | _ => 0
  end = Pos.to_nat a - Pos.to_nat a' destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq).a, a':positive
H:(a' < a)%positive
q:positive
Hq:(a' + q)%positive = a
N.to_nat (N.pos q) = Pos.to_nat a - Pos.to_nat a'
   simpl; symmetry; apply Nat.add_sub_eq_l.a, a':positive
H:(a' < a)%positive
q:positive
Hq:(a' + q)%positive = a
Pos.to_nat a' + Pos.to_nat q = Pos.to_nat a now rewrite <- Hq, Pos2Nat.inj_add.
Qed.

Lemma inj_pred a : N.to_nat (N.pred a) = Nat.pred (N.to_nat a).a:N
N.to_nat (N.pred a) = Nat.pred (N.to_nat a)
Proof.a:N
N.to_nat (N.pred a) = Nat.pred (N.to_nat a)
 rewrite <- Nat.sub_1_r, N.pred_sub.a:N
N.to_nat (a - 1) = N.to_nat a - 1 apply inj_sub.
Qed.

Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a).a:N
N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a)
Proof.a:N
N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a)
 destruct a as [|[p|p| ]]; trivial.p:positive
N.to_nat (N.div2 (N.pos p~1)) =
Nat.div2 (N.to_nat (N.pos p~1))
p:positive
N.to_nat (N.div2 (N.pos p~0)) =
Nat.div2 (N.to_nat (N.pos p~0))
 -p:positive
N.to_nat (N.div2 (N.pos p~1)) =
Nat.div2 (N.to_nat (N.pos p~1)) unfold N.div2, N.to_nat.p:positive
Pos.to_nat p = Nat.div2 (Pos.to_nat p~1) now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double.
 -p:positive
N.to_nat (N.div2 (N.pos p~0)) =
Nat.div2 (N.to_nat (N.pos p~0)) unfold N.div2, N.to_nat.p:positive
Pos.to_nat p = Nat.div2 (Pos.to_nat p~0) now rewrite Pos2Nat.inj_xO, Nat.div2_double.
Qed.

Lemma inj_compare a a' :
 (a ?= a')%N = (N.to_nat a ?= N.to_nat a').a, a':N
(a ?= a')%N = (N.to_nat a ?= N.to_nat a')
Proof.a, a':N
(a ?= a')%N = (N.to_nat a ?= N.to_nat a')
 destruct a, a'; simpl; trivial.p:positive
Lt = match Pos.to_nat p with
     | 0 => Eq
     | S _ => Lt
     end
p:positive
Gt = (Pos.to_nat p ?= 0)
p, p0:positive
(p ?= p0)%positive = (Pos.to_nat p ?= Pos.to_nat p0)
 -p:positive
Lt = match Pos.to_nat p with
     | 0 => Eq
     | S _ => Lt
     end now destruct (Pos2Nat.is_succ p) as (n,->).
 -p:positive
Gt = (Pos.to_nat p ?= 0) now destruct (Pos2Nat.is_succ p) as (n,->).
 -p, p0:positive
(p ?= p0)%positive = (Pos.to_nat p ?= Pos.to_nat p0) apply Pos2Nat.inj_compare.
Qed.

Lemma inj_max a a' :
  N.to_nat (N.max a a') = Nat.max (N.to_nat a) (N.to_nat a').a, a':N
N.to_nat (N.max a a') =
Nat.max (N.to_nat a) (N.to_nat a')
Proof.a, a':N
N.to_nat (N.max a a') =
Nat.max (N.to_nat a) (N.to_nat a')
 unfold N.max.a, a':N
N.to_nat
  match (a ?= a')%N with
  | Gt => a
  | _ => a'
  end = Nat.max (N.to_nat a) (N.to_nat a') rewrite inj_compare; symmetry.a, a':N
Nat.max (N.to_nat a) (N.to_nat a') =
N.to_nat
  match N.to_nat a ?= N.to_nat a' with
  | Gt => a
  | _ => a'
  end
 case Nat.compare_spec; intros.a, a':N
H:N.to_nat a = N.to_nat a'
Nat.max (N.to_nat a) (N.to_nat a') = N.to_nat a'
a, a':N
H:N.to_nat a < N.to_nat a'
Nat.max (N.to_nat a) (N.to_nat a') = N.to_nat a'
a, a':N
H:N.to_nat a' < N.to_nat a
Nat.max (N.to_nat a) (N.to_nat a') = N.to_nat a
 -a, a':N
H:N.to_nat a = N.to_nat a'
Nat.max (N.to_nat a) (N.to_nat a') = N.to_nat a' now apply Nat.max_r, Nat.eq_le_incl.
 -a, a':N
H:N.to_nat a < N.to_nat a'
Nat.max (N.to_nat a) (N.to_nat a') = N.to_nat a' now apply Nat.max_r, Nat.lt_le_incl.
 -a, a':N
H:N.to_nat a' < N.to_nat a
Nat.max (N.to_nat a) (N.to_nat a') = N.to_nat a now apply Nat.max_l, Nat.lt_le_incl.
Qed.

Lemma inj_min a a' :
  N.to_nat (N.min a a') = Nat.min (N.to_nat a) (N.to_nat a').a, a':N
N.to_nat (N.min a a') =
Nat.min (N.to_nat a) (N.to_nat a')
Proof.a, a':N
N.to_nat (N.min a a') =
Nat.min (N.to_nat a) (N.to_nat a')
  unfold N.min; rewrite inj_compare.a, a':N
N.to_nat
  match N.to_nat a ?= N.to_nat a' with
  | Gt => a'
  | _ => a
  end = Nat.min (N.to_nat a) (N.to_nat a') symmetry.a, a':N
Nat.min (N.to_nat a) (N.to_nat a') =
N.to_nat
  match N.to_nat a ?= N.to_nat a' with
  | Gt => a'
  | _ => a
  end
  case Nat.compare_spec; intros.a, a':N
H:N.to_nat a = N.to_nat a'
Nat.min (N.to_nat a) (N.to_nat a') = N.to_nat a
a, a':N
H:N.to_nat a < N.to_nat a'
Nat.min (N.to_nat a) (N.to_nat a') = N.to_nat a
a, a':N
H:N.to_nat a' < N.to_nat a
Nat.min (N.to_nat a) (N.to_nat a') = N.to_nat a'
 -a, a':N
H:N.to_nat a = N.to_nat a'
Nat.min (N.to_nat a) (N.to_nat a') = N.to_nat a now apply Nat.min_l, Nat.eq_le_incl.
 -a, a':N
H:N.to_nat a < N.to_nat a'
Nat.min (N.to_nat a) (N.to_nat a') = N.to_nat a now apply Nat.min_l, Nat.lt_le_incl.
 -a, a':N
H:N.to_nat a' < N.to_nat a
Nat.min (N.to_nat a) (N.to_nat a') = N.to_nat a' now apply Nat.min_r, Nat.lt_le_incl.
Qed.

Lemma inj_iter a {A} (f:A->A) (x:A) :
  N.iter a f x = Nat.iter (N.to_nat a) f x.a:N
A:Type
f:A -> A
x:A
N.iter a f x = Nat.iter (N.to_nat a) f x
Proof.a:N
A:Type
f:A -> A
x:A
N.iter a f x = Nat.iter (N.to_nat a) f x
 destruct a as [|a].A:Type
f:A -> A
x:A
N.iter 0 f x = Nat.iter (N.to_nat 0) f x
a:positive
A:Type
f:A -> A
x:A
N.iter (N.pos a) f x =
Nat.iter (N.to_nat (N.pos a)) f x trivial.a:positive
A:Type
f:A -> A
x:A
N.iter (N.pos a) f x =
Nat.iter (N.to_nat (N.pos a)) f x apply Pos2Nat.inj_iter.
Qed.

End N2Nat.

Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
 N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub
 N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min
 N2Nat.id
 : Nnat.

Conversions from nat to N

Module Nat2N.

N.of_nat is an bijection between nat and N, with Pos.to_nat as reciprocal. See N2Nat.id above for the dual equation.

Lemma id n : N.to_nat (N.of_nat n) = n.n:nat
N.to_nat (N.of_nat n) = n
Proof.n:nat
N.to_nat (N.of_nat n) = n
 induction n; simpl; trivial.n:nat
IHn:N.to_nat (N.of_nat n) = n
Pos.to_nat (Pos.of_succ_nat n) = S n apply SuccNat2Pos.id_succ.
Qed.

Hint Rewrite id : Nnat.
Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat.

N.of_nat is hence injective

Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'.n, n':nat
N.of_nat n = N.of_nat n' -> n = n'
Proof.n, n':nat
N.of_nat n = N.of_nat n' -> n = n'
 intros H.n, n':nat
H:N.of_nat n = N.of_nat n'
n = n' rewrite <- (id n), <- (id n').n, n':nat
H:N.of_nat n = N.of_nat n'
N.to_nat (N.of_nat n) = N.to_nat (N.of_nat n') now f_equal.
Qed.

Lemma inj_iff n n' : N.of_nat n = N.of_nat n' <-> n = n'.n, n':nat
N.of_nat n = N.of_nat n' <-> n = n'
Proof.n, n':nat
N.of_nat n = N.of_nat n' <-> n = n'
 split.n, n':nat
N.of_nat n = N.of_nat n' -> n = n'
n, n':nat
n = n' -> N.of_nat n = N.of_nat n' apply inj.n, n':nat
n = n' -> N.of_nat n = N.of_nat n' intros; now subst.
Qed.

Interaction of this translation and usual operations.

Lemma inj_double n : N.of_nat (2*n) = N.double (N.of_nat n).n:nat
N.of_nat (2 * n) = N.double (N.of_nat n)
Proof.n:nat
N.of_nat (2 * n) = N.double (N.of_nat n) nat2N. Qed.

Lemma inj_succ_double n : N.of_nat (S (2*n)) = N.succ_double (N.of_nat n).n:nat
N.of_nat (S (2 * n)) = N.succ_double (N.of_nat n)
Proof.n:nat
N.of_nat (S (2 * n)) = N.succ_double (N.of_nat n) nat2N. Qed.

Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n).n:nat
N.of_nat (S n) = N.succ (N.of_nat n)
Proof.n:nat
N.of_nat (S n) = N.succ (N.of_nat n) nat2N. Qed.

Lemma inj_pred n : N.of_nat (Nat.pred n) = N.pred (N.of_nat n).n:nat
N.of_nat (Nat.pred n) = N.pred (N.of_nat n)
Proof.n:nat
N.of_nat (Nat.pred n) = N.pred (N.of_nat n) nat2N. Qed.

Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N.n, n':nat
N.of_nat (n + n') = (N.of_nat n + N.of_nat n')%N
Proof.n, n':nat
N.of_nat (n + n') = (N.of_nat n + N.of_nat n')%N nat2N. Qed.

Lemma inj_sub n n' : N.of_nat (n-n') = (N.of_nat n - N.of_nat n')%N.n, n':nat
N.of_nat (n - n') = (N.of_nat n - N.of_nat n')%N
Proof.n, n':nat
N.of_nat (n - n') = (N.of_nat n - N.of_nat n')%N nat2N. Qed.

Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N.n, n':nat
N.of_nat (n * n') = (N.of_nat n * N.of_nat n')%N
Proof.n, n':nat
N.of_nat (n * n') = (N.of_nat n * N.of_nat n')%N nat2N. Qed.

Lemma inj_div2 n : N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n).n:nat
N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n)
Proof.n:nat
N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n) nat2N. Qed.

Lemma inj_compare n n' :
  (n ?= n') = (N.of_nat n ?= N.of_nat n')%N.n, n':nat
(n ?= n') = (N.of_nat n ?= N.of_nat n')%N
Proof.n, n':nat
(n ?= n') = (N.of_nat n ?= N.of_nat n')%N now rewrite N2Nat.inj_compare, !id. Qed.

Lemma inj_min n n' :
  N.of_nat (Nat.min n n') = N.min (N.of_nat n) (N.of_nat n').n, n':nat
N.of_nat (Nat.min n n') =
N.min (N.of_nat n) (N.of_nat n')
Proof.n, n':nat
N.of_nat (Nat.min n n') =
N.min (N.of_nat n) (N.of_nat n') nat2N. Qed.

Lemma inj_max n n' :
  N.of_nat (Nat.max n n') = N.max (N.of_nat n) (N.of_nat n').n, n':nat
N.of_nat (Nat.max n n') =
N.max (N.of_nat n) (N.of_nat n')
Proof.n, n':nat
N.of_nat (Nat.max n n') =
N.max (N.of_nat n) (N.of_nat n') nat2N. Qed.

Lemma inj_iter n {A} (f:A->A) (x:A) :
  Nat.iter n f x = N.iter (N.of_nat n) f x.n:nat
A:Type
f:A -> A
x:A
Nat.iter n f x = N.iter (N.of_nat n) f x
Proof.n:nat
A:Type
f:A -> A
x:A
Nat.iter n f x = N.iter (N.of_nat n) f x now rewrite N2Nat.inj_iter, !id. Qed.

End Nat2N.

Hint Rewrite Nat2N.id : Nnat.

Compatibility notations

Notation nat_of_N_inj := N2Nat.inj (only parsing).
Notation N_of_nat_of_N := N2Nat.id (only parsing).
Notation nat_of_Ndouble := N2Nat.inj_double (only parsing).
Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing).
Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing).
Notation nat_of_Nplus := N2Nat.inj_add (only parsing).
Notation nat_of_Nmult := N2Nat.inj_mul (only parsing).
Notation nat_of_Nminus := N2Nat.inj_sub (only parsing).
Notation nat_of_Npred := N2Nat.inj_pred (only parsing).
Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing).
Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing).
Notation nat_of_Nmax := N2Nat.inj_max (only parsing).
Notation nat_of_Nmin := N2Nat.inj_min (only parsing).

Notation nat_of_N_of_nat := Nat2N.id (only parsing).
Notation N_of_nat_inj := Nat2N.inj (only parsing).
Notation N_of_double := Nat2N.inj_double (only parsing).
Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing).
Notation N_of_S := Nat2N.inj_succ (only parsing).
Notation N_of_pred := Nat2N.inj_pred (only parsing).
Notation N_of_plus := Nat2N.inj_add (only parsing).
Notation N_of_minus := Nat2N.inj_sub (only parsing).
Notation N_of_mult := Nat2N.inj_mul (only parsing).
Notation N_of_div2 := Nat2N.inj_div2 (only parsing).
Notation N_of_nat_compare := Nat2N.inj_compare (only parsing).
Notation N_of_min := Nat2N.inj_min (only parsing).
Notation N_of_max := Nat2N.inj_max (only parsing).