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 Export BinNums.
Require Import BinPos RelationClasses Morphisms Setoid
 Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties.
Require BinNatDef.

(**********************************************************************)

Binary natural numbers, operations and properties

(**********************************************************************)

The type N and its constructors N0 and Npos are now defined in BinNums.v

Every definitions and properties about binary natural numbers are placed in a module N for qualification purpose.

Local Open Scope N_scope.

Every definitions and early properties about positive numbers are placed in a module N for qualification purpose.

Module N
 <: NAxiomsSig
 <: UsualOrderedTypeFull
 <: UsualDecidableTypeFull
 <: TotalOrder.

Definitions of operations, now in a separate file

Include BinNatDef.N.

When including property functors, only inline t eq zero one two

Set Inline Level 30.

Logical predicates

Definition eq := @Logic.eq N.
Definition eq_equiv := @eq_equivalence N.

Definition lt x y := (x ?= y) = Lt.
Definition gt x y := (x ?= y) = Gt.
Definition le x y := (x ?= y) <> Gt.
Definition ge x y := (x ?= y) <> Lt.

Infix "<=" := le : N_scope.
Infix "<" := lt : N_scope.
Infix ">=" := ge : N_scope.
Infix ">" := gt : N_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
Notation "x < y < z" := (x < y /\ y < z) : N_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.

Definition divide p q := exists r, q = r*p.
Notation "( p | q )" := (divide p q) (at level 0) : N_scope.

Definition Even n := exists m, n = 2*m.
Definition Odd n := exists m, n = 2*m+1.

Proofs of morphisms, obvious since eq is Leibniz

Local Obligation Tactic := simpl_relation.
Definition succ_wd : Proper (eq==>eq) succ := _.
Definition pred_wd : Proper (eq==>eq) pred := _.
Definition add_wd : Proper (eq==>eq==>eq) add := _.
Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
Definition div_wd : Proper (eq==>eq==>eq) div := _.
Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.

Decidability of equality.

Definition eq_dec : forall n m : N, { n = m } + { n <> m }.forall n m : N, {n = m} + {n <> m}
Proof.forall n m : N, {n = m} + {n <> m}
 decide equality.n, m:N
p, p0:positive
{p = p0} + {p <> p0}
 apply Pos.eq_dec.
Defined.

Discrimination principle

Definition discr n : { p:positive | n = pos p } + { n = 0 }.n:N
{p : positive | n = pos p} + {n = 0}
Proof.n:N
{p : positive | n = pos p} + {n = 0}
 destruct n; auto.p:positive
{p0 : positive | pos p = pos p0} + {pos p = 0}
 left; exists p; auto.
Defined.

Convenient induction principles

Definition binary_rect (P:N -> Type) (f0 : P 0)
  (f2 : forall n, P n -> P (double n))
  (fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n :=
 let P' p := P (pos p) in
 let f2' p := f2 (pos p) in
 let fS2' p := fS2 (pos p) in
 match n with
 | 0 => f0
 | pos p => positive_rect P' fS2' f2' (fS2 0 f0) p
 end.

Definition binary_rec (P:N -> Set) := binary_rect P.
Definition binary_ind (P:N -> Prop) := binary_rect P.

Peano induction on binary natural numbers

Definition peano_rect
  (P : N -> Type) (f0 : P 0)
    (f : forall n : N, P n -> P (succ n)) (n : N) : P n :=
let P' p := P (pos p) in
let f' p := f (pos p) in
match n with
| 0 => f0
| pos p => Pos.peano_rect P' (f 0 f0) f' p
end.

Theorem peano_rect_base P a f : peano_rect P a f 0 = a.P:N -> Type
a:P 0
f:forall n : N, P n -> P (succ n)
peano_rect P a f 0 = a
Proof.P:N -> Type
a:P 0
f:forall n : N, P n -> P (succ n)
peano_rect P a f 0 = a
reflexivity.
Qed.

Theorem peano_rect_succ P a f n :
 peano_rect P a f (succ n) = f n (peano_rect P a f n).P:N -> Type
a:P 0
f:forall n0 : N, P n0 -> P (succ n0)
n:N
peano_rect P a f (succ n) = f n (peano_rect P a f n)
Proof.P:N -> Type
a:P 0
f:forall n0 : N, P n0 -> P (succ n0)
n:N
peano_rect P a f (succ n) = f n (peano_rect P a f n)
destruct n; simpl.P:N -> Type
a:P 0
f:forall n : N, P n -> P (succ n)
f 0 a = f 0 a
P:N -> Type
a:P 0
f:forall n : N, P n -> P (succ n)
p:positive
Pos.peano_rect (fun p0 : positive => P (pos p0))
  (f 0 a) (fun p0 : positive => f (pos p0))
  (Pos.succ p) =
f (pos p)
  (Pos.peano_rect (fun p0 : positive => P (pos p0))
     (f 0 a) (fun p0 : positive => f (pos p0)) p)
trivial.P:N -> Type
a:P 0
f:forall n : N, P n -> P (succ n)
p:positive
Pos.peano_rect (fun p0 : positive => P (pos p0))
  (f 0 a) (fun p0 : positive => f (pos p0))
  (Pos.succ p) =
f (pos p)
  (Pos.peano_rect (fun p0 : positive => P (pos p0))
     (f 0 a) (fun p0 : positive => f (pos p0)) p)
now rewrite Pos.peano_rect_succ.
Qed.

Definition peano_ind (P : N -> Prop) := peano_rect P.

Definition peano_rec (P : N -> Set) := peano_rect P.

Theorem peano_rec_base P a f : peano_rec P a f 0 = a.P:N -> Set
a:P 0
f:forall n : N, P n -> P (succ n)
peano_rec P a f 0 = a
Proof.P:N -> Set
a:P 0
f:forall n : N, P n -> P (succ n)
peano_rec P a f 0 = a
apply peano_rect_base.
Qed.

Theorem peano_rec_succ P a f n :
 peano_rec P a f (succ n) = f n (peano_rec P a f n).P:N -> Set
a:P 0
f:forall n0 : N, P n0 -> P (succ n0)
n:N
peano_rec P a f (succ n) = f n (peano_rec P a f n)
Proof.P:N -> Set
a:P 0
f:forall n0 : N, P n0 -> P (succ n0)
n:N
peano_rec P a f (succ n) = f n (peano_rec P a f n)
apply peano_rect_succ.
Qed.

Generic induction / recursion

Theorem bi_induction :
  forall A : N -> Prop, Proper (Logic.eq==>iff) A ->
    A 0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n.forall A : N -> Prop,
Proper (Logic.eq ==> iff) A ->
A 0 ->
(forall n : N, A n <-> A (succ n)) ->
forall n : N, A n
Proof.forall A : N -> Prop,
Proper (Logic.eq ==> iff) A ->
A 0 ->
(forall n : N, A n <-> A (succ n)) ->
forall n : N, A n
intros A A_wd A0 AS.A:N -> Prop
A_wd:Proper (Logic.eq ==> iff) A
A0:A 0
AS:forall n : N, A n <-> A (succ n)
forall n : N, A n apply peano_rect.A:N -> Prop
A_wd:Proper (Logic.eq ==> iff) A
A0:A 0
AS:forall n : N, A n <-> A (succ n)
A 0
A:N -> Prop
A_wd:Proper (Logic.eq ==> iff) A
A0:A 0
AS:forall n : N, A n <-> A (succ n)
forall n : N, A n -> A (succ n) assumption.A:N -> Prop
A_wd:Proper (Logic.eq ==> iff) A
A0:A 0
AS:forall n : N, A n <-> A (succ n)
forall n : N, A n -> A (succ n) intros; now apply -> AS.
Qed.

Definition recursion {A} : A -> (N -> A -> A) -> N -> A :=
  peano_rect (fun _ => A).

Instance recursion_wd {A} (Aeq : relation A) :
 Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion.A:Type
Aeq:relation A
Proper
  (Aeq ==>
   (Logic.eq ==> Aeq ==> Aeq) ==> Logic.eq ==> Aeq)
  recursion
Proof.A:Type
Aeq:relation A
Proper
  (Aeq ==>
   (Logic.eq ==> Aeq ==> Aeq) ==> Logic.eq ==> Aeq)
  recursion
intros a a' Ea f f' Ef x x' Ex.A:Type
Aeq:relation A
a, a':A
Ea:Aeq a a'
f, f':N -> A -> A
Ef:(Logic.eq ==> Aeq ==> Aeq)%signature f f'
x, x':N
Ex:x = x'
Aeq (recursion a f x) (recursion a' f' x') subst x'.A:Type
Aeq:relation A
a, a':A
Ea:Aeq a a'
f, f':N -> A -> A
Ef:(Logic.eq ==> Aeq ==> Aeq)%signature f f'
x:N
Aeq (recursion a f x) (recursion a' f' x)
induction x using peano_ind.A:Type
Aeq:relation A
a, a':A
Ea:Aeq a a'
f, f':N -> A -> A
Ef:(Logic.eq ==> Aeq ==> Aeq)%signature f f'
Aeq (recursion a f 0) (recursion a' f' 0)
A:Type
Aeq:relation A
a, a':A
Ea:Aeq a a'
f, f':N -> A -> A
Ef:(Logic.eq ==> Aeq ==> Aeq)%signature f f'
x:N
IHx:Aeq (recursion a f x) (recursion a' f' x)
Aeq (recursion a f (succ x))
  (recursion a' f' (succ x))
trivial.A:Type
Aeq:relation A
a, a':A
Ea:Aeq a a'
f, f':N -> A -> A
Ef:(Logic.eq ==> Aeq ==> Aeq)%signature f f'
x:N
IHx:Aeq (recursion a f x) (recursion a' f' x)
Aeq (recursion a f (succ x))
  (recursion a' f' (succ x))
unfold recursion in *.A:Type
Aeq:relation A
a, a':A
Ea:Aeq a a'
f, f':N -> A -> A
Ef:(Logic.eq ==> Aeq ==> Aeq)%signature f f'
x:N
IHx:Aeq (peano_rect (fun _ : N => A) a f x) (peano_rect (fun _ : N => A) a' f' x)
Aeq (peano_rect (fun _ : N => A) a f (succ x))
  (peano_rect (fun _ : N => A) a' f' (succ x)) rewrite 2 peano_rect_succ.A:Type
Aeq:relation A
a, a':A
Ea:Aeq a a'
f, f':N -> A -> A
Ef:(Logic.eq ==> Aeq ==> Aeq)%signature f f'
x:N
IHx:Aeq (peano_rect (fun _ : N => A) a f x) (peano_rect (fun _ : N => A) a' f' x)
Aeq (f x (peano_rect (fun _ : N => A) a f x))
  (f' x (peano_rect (fun _ : N => A) a' f' x)) now apply Ef.
Qed.

Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a.A:Type
a:A
f:N -> A -> A
recursion a f 0 = a
Proof.A:Type
a:A
f:N -> A -> A
recursion a f 0 = a reflexivity. Qed.

Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A):
 Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f ->
  forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)).A:Type
Aeq:relation A
a:A
f:N -> A -> A
Aeq a a ->
Proper (Logic.eq ==> Aeq ==> Aeq) f ->
forall n : N,
Aeq (recursion a f (succ n)) (f n (recursion a f n))
Proof.A:Type
Aeq:relation A
a:A
f:N -> A -> A
Aeq a a ->
Proper (Logic.eq ==> Aeq ==> Aeq) f ->
forall n : N,
Aeq (recursion a f (succ n)) (f n (recursion a f n))
unfold recursion; intros a_wd f_wd n.A:Type
Aeq:relation A
a:A
f:N -> A -> A
a_wd:Aeq a a
f_wd:Proper (Logic.eq ==> Aeq ==> Aeq) f
n:N
Aeq (peano_rect (fun _ : N => A) a f (succ n))
  (f n (peano_rect (fun _ : N => A) a f n)) induction n using peano_ind.A:Type
Aeq:relation A
a:A
f:N -> A -> A
a_wd:Aeq a a
f_wd:Proper (Logic.eq ==> Aeq ==> Aeq) f
Aeq (peano_rect (fun _ : N => A) a f (succ 0))
  (f 0 (peano_rect (fun _ : N => A) a f 0))
A:Type
Aeq:relation A
a:A
f:N -> A -> A
a_wd:Aeq a a
f_wd:Proper (Logic.eq ==> Aeq ==> Aeq) f
n:N
IHn:Aeq (peano_rect (fun _ : N => A) a f (succ n))
  (f n (peano_rect (fun _ : N => A) a f n))
Aeq (peano_rect (fun _ : N => A) a f (succ (succ n)))
  (f (succ n)
     (peano_rect (fun _ : N => A) a f (succ n)))
rewrite peano_rect_succ.A:Type
Aeq:relation A
a:A
f:N -> A -> A
a_wd:Aeq a a
f_wd:Proper (Logic.eq ==> Aeq ==> Aeq) f
Aeq (f 0 (peano_rect (fun _ : N => A) a f 0))
  (f 0 (peano_rect (fun _ : N => A) a f 0))
A:Type
Aeq:relation A
a:A
f:N -> A -> A
a_wd:Aeq a a
f_wd:Proper (Logic.eq ==> Aeq ==> Aeq) f
n:N
IHn:Aeq (peano_rect (fun _ : N => A) a f (succ n))
  (f n (peano_rect (fun _ : N => A) a f n))
Aeq (peano_rect (fun _ : N => A) a f (succ (succ n)))
  (f (succ n)
     (peano_rect (fun _ : N => A) a f (succ n))) now apply f_wd.A:Type
Aeq:relation A
a:A
f:N -> A -> A
a_wd:Aeq a a
f_wd:Proper (Logic.eq ==> Aeq ==> Aeq) f
n:N
IHn:Aeq (peano_rect (fun _ : N => A) a f (succ n))
  (f n (peano_rect (fun _ : N => A) a f n))
Aeq (peano_rect (fun _ : N => A) a f (succ (succ n)))
  (f (succ n)
     (peano_rect (fun _ : N => A) a f (succ n)))
rewrite !peano_rect_succ in *.A:Type
Aeq:relation A
a:A
f:N -> A -> A
a_wd:Aeq a a
f_wd:Proper (Logic.eq ==> Aeq ==> Aeq) f
n:N
IHn:Aeq (f n (peano_rect (fun _ : N => A) a f n))
  (f n (peano_rect (fun _ : N => A) a f n))
Aeq
  (f (succ n)
     (f n (peano_rect (fun _ : N => A) a f n)))
  (f (succ n)
     (f n (peano_rect (fun _ : N => A) a f n))) now apply f_wd.
Qed.

Specification of constants

Lemma one_succ : 1 = succ 0.1 = succ 0
Proof.1 = succ 0 reflexivity. Qed.

Lemma two_succ : 2 = succ 1.2 = succ 1
Proof.2 = succ 1 reflexivity. Qed.

Definition pred_0 : pred 0 = 0.pred 0 = 0
Proof.pred 0 = 0 reflexivity. Qed.

Properties of mixed successor and predecessor.

Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p).p:positive
Pos.pred_N p = pred (pos p)
Proof.p:positive
Pos.pred_N p = pred (pos p)
 now destruct p.
Qed.

Lemma succ_pos_spec n : pos (succ_pos n) = succ n.n:N
pos (succ_pos n) = succ n
Proof.n:N
pos (succ_pos n) = succ n
 now destruct n.
Qed.

Lemma pos_pred_succ n : Pos.pred_N (succ_pos n) = n.n:N
Pos.pred_N (succ_pos n) = n
Proof.n:N
Pos.pred_N (succ_pos n) = n
 destruct n.Pos.pred_N (succ_pos 0) = 0
p:positive
Pos.pred_N (succ_pos (pos p)) = pos p trivial.p:positive
Pos.pred_N (succ_pos (pos p)) = pos p apply Pos.pred_N_succ.
Qed.

Lemma succ_pos_pred p : succ (Pos.pred_N p) = pos p.p:positive
succ (Pos.pred_N p) = pos p
Proof.p:positive
succ (Pos.pred_N p) = pos p
 destruct p; simpl; trivial.p:positive
pos (Pos.succ (Pos.pred_double p)) = pos p~0 f_equal.p:positive
Pos.succ (Pos.pred_double p) = (p~0)%positive apply Pos.succ_pred_double.
Qed.

Properties of successor and predecessor

Theorem pred_succ n : pred (succ n) = n.n:N
pred (succ n) = n
Proof.n:N
pred (succ n) = n
destruct n; trivial.p:positive
pred (succ (pos p)) = pos p simpl.p:positive
Pos.pred_N (Pos.succ p) = pos p apply Pos.pred_N_succ.
Qed.

Theorem pred_sub n : pred n = sub n 1.n:N
pred n = n - 1
Proof.n:N
pred n = n - 1
 now destruct n as [|[p|p|]].
Qed.

Theorem succ_0_discr n : succ n <> 0.n:N
succ n <> 0
Proof.n:N
succ n <> 0
now destruct n.
Qed.

Specification of addition

Theorem add_0_l n : 0 + n = n.n:N
0 + n = n
Proof.n:N
0 + n = n
reflexivity.
Qed.

Theorem add_succ_l n m : succ n + m = succ (n + m).n, m:N
succ n + m = succ (n + m)
Proof.n, m:N
succ n + m = succ (n + m)
destruct n, m; unfold succ, add; now rewrite ?Pos.add_1_l, ?Pos.add_succ_l.
Qed.

Specification of subtraction.

Theorem sub_0_r n : n - 0 = n.n:N
n - 0 = n
Proof.n:N
n - 0 = n
now destruct n.
Qed.

Theorem sub_succ_r n m : n - succ m = pred (n - m).n, m:N
n - succ m = pred (n - m)
Proof.n, m:N
n - succ m = pred (n - m)
destruct n as [|p], m as [|q]; trivial.p:positive
pos p - succ 0 = pred (pos p - 0)
p, q:positive
pos p - succ (pos q) = pred (pos p - pos q)
now destruct p.p, q:positive
pos p - succ (pos q) = pred (pos p - pos q)
simpl.p, q:positive
match Pos.sub_mask p (Pos.succ q) with
| Pos.IsPos p0 => pos p0
| _ => 0
end =
pred
  match Pos.sub_mask p q with
  | Pos.IsPos p0 => pos p0
  | _ => 0
  end rewrite Pos.sub_mask_succ_r, Pos.sub_mask_carry_spec.p, q:positive
match Pos.pred_mask (Pos.sub_mask p q) with
| Pos.IsPos p0 => pos p0
| _ => 0
end =
pred
  match Pos.sub_mask p q with
  | Pos.IsPos p0 => pos p0
  | _ => 0
  end
now destruct (Pos.sub_mask p q) as [|[r|r|]|].
Qed.

Specification of multiplication

Theorem mul_0_l n : 0 * n = 0.n:N
0 * n = 0
Proof.n:N
0 * n = 0
reflexivity.
Qed.

Theorem mul_succ_l n m : (succ n) * m = n * m + m.n, m:N
succ n * m = n * m + m
Proof.n, m:N
succ n * m = n * m + m
destruct n, m; simpl; trivial.p, p0:positive
pos (Pos.succ p * p0) = pos (p * p0 + p0) f_equal.p, p0:positive
(Pos.succ p * p0)%positive = (p * p0 + p0)%positive rewrite Pos.add_comm.p, p0:positive
(Pos.succ p * p0)%positive = (p0 + p * p0)%positive
apply Pos.mul_succ_l.
Qed.

Specification of boolean comparisons.

Lemma eqb_eq n m : eqb n m = true <-> n=m.n, m:N
(n =? m) = true <-> n = m
Proof.n, m:N
(n =? m) = true <-> n = m
destruct n as [|n], m as [|m]; simpl; try easy'.n, m:positive
(n =? m)%positive = true <-> pos n = pos m
rewrite Pos.eqb_eq.n, m:positive
n = m <-> pos n = pos m split; intro H.n, m:positive
H:n = m
pos n = pos m
n, m:positive
H:pos n = pos m
n = m now subst.n, m:positive
H:pos n = pos m
n = m now destr_eq H.
Qed.

Lemma ltb_lt n m : (n <? m) = true <-> n < m.n, m:N
(n <? m) = true <-> n < m
Proof.n, m:N
(n <? m) = true <-> n < m
  unfold ltb, lt.n, m:N
match n ?= m with
| Lt => true
| _ => false
end = true <-> (n ?= m) = Lt destruct compare; easy'.
Qed.

Lemma leb_le n m : (n <=? m) = true <-> n <= m.n, m:N
(n <=? m) = true <-> n <= m
Proof.n, m:N
(n <=? m) = true <-> n <= m
  unfold leb, le.n, m:N
match n ?= m with
| Gt => false
| _ => true
end = true <-> (n ?= m) <> Gt destruct compare; easy'.
Qed.

Basic properties of comparison

Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m.n, m:N
(n ?= m) = Eq <-> n = m
Proof.n, m:N
(n ?= m) = Eq <-> n = m
destruct n, m; simpl; rewrite ?Pos.compare_eq_iff; split; congruence.
Qed.

Theorem compare_lt_iff n m : (n ?= m) = Lt <-> n < m.n, m:N
(n ?= m) = Lt <-> n < m
Proof.n, m:N
(n ?= m) = Lt <-> n < m
reflexivity.
Qed.

Theorem compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.n, m:N
(n ?= m) <> Gt <-> n <= m
Proof.n, m:N
(n ?= m) <> Gt <-> n <= m
reflexivity.
Qed.

Theorem compare_antisym n m : (m ?= n) = CompOpp (n ?= m).n, m:N
(m ?= n) = CompOpp (n ?= m)
Proof.n, m:N
(m ?= n) = CompOpp (n ?= m)
destruct n, m; simpl; trivial.p, p0:positive
(p0 ?= p)%positive = CompOpp (p ?= p0)%positive apply Pos.compare_antisym.
Qed.

Some more advanced properties of comparison and orders, including compare_spec and lt_irrefl and lt_eq_cases.

Include BoolOrderFacts.

Specification of minimum and maximum

Theorem min_l n m : n <= m -> min n m = n.n, m:N
n <= m -> min n m = n
Proof.n, m:N
n <= m -> min n m = n
unfold min, le.n, m:N
(n ?= m) <> Gt ->
match n ?= m with
| Gt => m
| _ => n
end = n case compare; trivial.n, m:N
Gt <> Gt -> m = n now destruct 1.
Qed.

Theorem min_r n m : m <= n -> min n m = m.n, m:N
m <= n -> min n m = m
Proof.n, m:N
m <= n -> min n m = m
unfold min, le.n, m:N
(m ?= n) <> Gt ->
match n ?= m with
| Gt => m
| _ => n
end = m rewrite compare_antisym.n, m:N
CompOpp (n ?= m) <> Gt ->
match n ?= m with
| Gt => m
| _ => n
end = m
case compare_spec; trivial.n, m:N
n < m -> CompOpp Lt <> Gt -> n = m now destruct 2.
Qed.

Theorem max_l n m : m <= n -> max n m = n.n, m:N
m <= n -> max n m = n
Proof.n, m:N
m <= n -> max n m = n
unfold max, le.n, m:N
(m ?= n) <> Gt ->
match n ?= m with
| Gt => n
| _ => m
end = n rewrite compare_antisym.n, m:N
CompOpp (n ?= m) <> Gt ->
match n ?= m with
| Gt => n
| _ => m
end = n
case compare_spec; auto.n, m:N
n < m -> CompOpp Lt <> Gt -> m = n now destruct 2.
Qed.

Theorem max_r n m : n <= m -> max n m = m.n, m:N
n <= m -> max n m = m
Proof.n, m:N
n <= m -> max n m = m
unfold max, le.n, m:N
(n ?= m) <> Gt ->
match n ?= m with
| Gt => n
| _ => m
end = m case compare; trivial.n, m:N
Gt <> Gt -> n = m now destruct 1.
Qed.

Specification of lt and le.

Lemma lt_succ_r n m : n < succ m <-> n<=m.n, m:N
n < succ m <-> n <= m
Proof.n, m:N
n < succ m <-> n <= m
destruct n as [|p], m as [|q]; simpl; try easy'.p:positive
pos p < 1 <-> pos p <= 0
p, q:positive
pos p < pos (Pos.succ q) <-> pos p <= pos q
split.p:positive
pos p < 1 -> pos p <= 0
p:positive
pos p <= 0 -> pos p < 1
p, q:positive
pos p < pos (Pos.succ q) <-> pos p <= pos q now destruct p.p:positive
pos p <= 0 -> pos p < 1
p, q:positive
pos p < pos (Pos.succ q) <-> pos p <= pos q now destruct 1.p, q:positive
pos p < pos (Pos.succ q) <-> pos p <= pos q
apply Pos.lt_succ_r.
Qed.

We can now derive all properties of basic functions and orders, and use these properties for proving the specs of more advanced functions.

Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

Properties of double and succ_double

Lemma double_spec n : double n = 2 * n.n:N
double n = 2 * n
Proof.n:N
double n = 2 * n
 reflexivity.
Qed.

Lemma succ_double_spec n : succ_double n = 2 * n + 1.n:N
succ_double n = 2 * n + 1
Proof.n:N
succ_double n = 2 * n + 1
 now destruct n.
Qed.

Lemma double_add n m : double (n+m) = double n + double m.n, m:N
double (n + m) = double n + double m
Proof.n, m:N
double (n + m) = double n + double m
 now destruct n, m.
Qed.

Lemma succ_double_add n m : succ_double (n+m) = double n + succ_double m.n, m:N
succ_double (n + m) = double n + succ_double m
Proof.n, m:N
succ_double (n + m) = double n + succ_double m
 now destruct n, m.
Qed.

Lemma double_mul n m : double (n*m) = double n * m.n, m:N
double (n * m) = double n * m
Proof.n, m:N
double (n * m) = double n * m
 now destruct n, m.
Qed.

Lemma succ_double_mul n m :
 succ_double n * m = double n * m + m.n, m:N
succ_double n * m = double n * m + m
Proof.n, m:N
succ_double n * m = double n * m + m
 destruct n; simpl; destruct m; trivial.p, p0:positive
pos (p0 + (p * p0)~0) = pos (p * p0)~0 + pos p0
 now rewrite Pos.add_comm.
Qed.

Lemma div2_double n : div2 (double n) = n.n:N
div2 (double n) = n
Proof.n:N
div2 (double n) = n
now destruct n.
Qed.

Lemma div2_succ_double n : div2 (succ_double n) = n.n:N
div2 (succ_double n) = n
Proof.n:N
div2 (succ_double n) = n
now destruct n.
Qed.

Lemma double_inj n m : double n = double m -> n = m.n, m:N
double n = double m -> n = m
Proof.n, m:N
double n = double m -> n = m
intro H.n, m:N
H:double n = double m
n = m rewrite <- (div2_double n), H.n, m:N
H:double n = double m
div2 (double m) = m apply div2_double.
Qed.

Lemma succ_double_inj n m : succ_double n = succ_double m -> n = m.n, m:N
succ_double n = succ_double m -> n = m
Proof.n, m:N
succ_double n = succ_double m -> n = m
intro H.n, m:N
H:succ_double n = succ_double m
n = m rewrite <- (div2_succ_double n), H.n, m:N
H:succ_double n = succ_double m
div2 (succ_double m) = m apply div2_succ_double.
Qed.

Lemma succ_double_lt n m : n<m -> succ_double n < double m.n, m:N
n < m -> succ_double n < double m
Proof.n, m:N
n < m -> succ_double n < double m
 destruct n as [|n], m as [|m]; intros H; try easy.n, m:positive
H:pos n < pos m
succ_double (pos n) < double (pos m)
 unfold lt in *; simpl in *.n, m:positive
H:(n ?= m)%positive = Lt
(n~1 ?= m~0)%positive = Lt now rewrite Pos.compare_xI_xO, H.
Qed.

Lemma double_lt_mono n m : n < m -> double n < double m.n, m:N
n < m -> double n < double m
Proof.n, m:N
n < m -> double n < double m
  destruct n as [|n], m as [|m]; intros H; try easy.
Qed.

Lemma double_le_mono n m : n <= m -> double n <= double m.n, m:N
n <= m -> double n <= double m
Proof.n, m:N
n <= m -> double n <= double m
  destruct n as [|n], m as [|m]; intros H; try easy.
Qed.

Lemma succ_double_lt_mono n m : n < m -> succ_double n < succ_double m.n, m:N
n < m -> succ_double n < succ_double m
Proof.n, m:N
n < m -> succ_double n < succ_double m
  destruct n as [|n], m as [|m]; intros H; try easy.
Qed.

Lemma succ_double_le_mono n m : n <= m -> succ_double n <= succ_double m.n, m:N
n <= m -> succ_double n <= succ_double m
Proof.n, m:N
n <= m -> succ_double n <= succ_double m
  destruct n as [|n], m as [|m]; intros H; try easy.
Qed.

0 is the least natural number

Theorem compare_0_r n : (n ?= 0) <> Lt.n:N
(n ?= 0) <> Lt
Proof.n:N
(n ?= 0) <> Lt
now destruct n.
Qed.

Specifications of power

Lemma pow_0_r n : n ^ 0 = 1.n:N
n ^ 0 = 1
Proof.n:N
n ^ 0 = 1 reflexivity. Qed.

Lemma pow_succ_r n p : 0<=p -> n^(succ p) = n * n^p.n, p:N
0 <= p -> n ^ succ p = n * n ^ p
Proof.n, p:N
0 <= p -> n ^ succ p = n * n ^ p
 intros _.n, p:N
n ^ succ p = n * n ^ p
 destruct n, p; simpl; trivial; f_equal.p0, p:positive
(p0 ^ Pos.succ p)%positive = (p0 * p0 ^ p)%positive apply Pos.pow_succ_r.
Qed.

Lemma pow_neg_r n p : p<0 -> n^p = 0.n, p:N
p < 0 -> n ^ p = 0
Proof.n, p:N
p < 0 -> n ^ p = 0
 now destruct p.
Qed.

Specification of square

Lemma square_spec n : square n = n * n.n:N
square n = n * n
Proof.n:N
square n = n * n
 destruct n; trivial.p:positive
square (pos p) = pos p * pos p simpl.p:positive
pos (Pos.square p) = pos (p * p) f_equal.p:positive
Pos.square p = (p * p)%positive apply Pos.square_spec.
Qed.

Specification of Base-2 logarithm

Lemma size_log2 n : n<>0 -> size n = succ (log2 n).n:N
n <> 0 -> size n = succ (log2 n)
Proof.n:N
n <> 0 -> size n = succ (log2 n)
 destruct n as [|[n|n| ]]; trivial.0 <> 0 -> size 0 = succ (log2 0) now destruct 1.
Qed.

Lemma size_gt n : n < 2^(size n).n:N
n < 2 ^ size n
Proof.n:N
n < 2 ^ size n
 destruct n.0 < 2 ^ size 0
p:positive
pos p < 2 ^ size (pos p) reflexivity.p:positive
pos p < 2 ^ size (pos p) simpl.p:positive
pos p < pos (2 ^ Pos.size p) apply Pos.size_gt.
Qed.

Lemma size_le n : 2^(size n) <= succ_double n.n:N
2 ^ size n <= succ_double n
Proof.n:N
2 ^ size n <= succ_double n
 destruct n.2 ^ size 0 <= succ_double 0
p:positive
2 ^ size (pos p) <= succ_double (pos p) discriminate.p:positive
2 ^ size (pos p) <= succ_double (pos p) simpl.p:positive
pos (2 ^ Pos.size p) <= pos p~1
 change (2^Pos.size p <= Pos.succ (p~0))%positive.p:positive
(2 ^ Pos.size p <= Pos.succ p~0)%positive
 apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le.
Qed.

Lemma log2_spec n : 0 < n ->
 2^(log2 n) <= n < 2^(succ (log2 n)).n:N
0 < n -> 2 ^ log2 n <= n < 2 ^ succ (log2 n)
Proof.n:N
0 < n -> 2 ^ log2 n <= n < 2 ^ succ (log2 n)
 destruct n as [|[p|p|]]; discriminate || intros _; simpl; split.p:positive
pos (2 ^ Pos.size p) <= pos p~1
p:positive
pos p~1 < pos (2 ^ Pos.succ (Pos.size p))
p:positive
pos (2 ^ Pos.size p) <= pos p~0
p:positive
pos p~0 < pos (2 ^ Pos.succ (Pos.size p))
1 <= 1
1 < pos (2 ^ 1)
 apply (size_le (pos p)).p:positive
pos p~1 < pos (2 ^ Pos.succ (Pos.size p))
p:positive
pos (2 ^ Pos.size p) <= pos p~0
p:positive
pos p~0 < pos (2 ^ Pos.succ (Pos.size p))
1 <= 1
1 < pos (2 ^ 1)
 apply Pos.size_gt.p:positive
pos (2 ^ Pos.size p) <= pos p~0
p:positive
pos p~0 < pos (2 ^ Pos.succ (Pos.size p))
1 <= 1
1 < pos (2 ^ 1)
 apply Pos.size_le.p:positive
pos p~0 < pos (2 ^ Pos.succ (Pos.size p))
1 <= 1
1 < pos (2 ^ 1)
 apply Pos.size_gt.1 <= 1
1 < pos (2 ^ 1)
 discriminate.1 < pos (2 ^ 1)
 reflexivity.
Qed.

Lemma log2_nonpos n : n<=0 -> log2 n = 0.n:N
n <= 0 -> log2 n = 0
Proof.n:N
n <= 0 -> log2 n = 0
 destruct n; intros Hn.Hn:0 <= 0
log2 0 = 0
p:positive
Hn:pos p <= 0
log2 (pos p) = 0 reflexivity.p:positive
Hn:pos p <= 0
log2 (pos p) = 0 now destruct Hn.
Qed.

Specification of parity functions

Lemma even_spec n : even n = true <-> Even n.n:N
even n = true <-> Even n
Proof.n:N
even n = true <-> Even n
 destruct n.even 0 = true <-> Even 0
p:positive
even (pos p) = true <-> Even (pos p)
 split.even 0 = true -> Even 0
Even 0 -> even 0 = true
p:positive
even (pos p) = true <-> Even (pos p) now exists 0.Even 0 -> even 0 = true
p:positive
even (pos p) = true <-> Even (pos p)
 trivial.p:positive
even (pos p) = true <-> Even (pos p)
 destruct p; simpl; split; try easy.p:positive
Even (pos p~1) -> false = true
p:positive
true = true -> Even (pos p~0)
Even 1 -> false = true
 intros (m,H).p:positive
m:N
H:pos p~1 = 2 * m
false = true
p:positive
true = true -> Even (pos p~0)
Even 1 -> false = true now destruct m.p:positive
true = true -> Even (pos p~0)
Even 1 -> false = true
 now exists (pos p).Even 1 -> false = true
 intros (m,H).m:N
H:1 = 2 * m
false = true now destruct m.
Qed.

Lemma odd_spec n : odd n = true <-> Odd n.n:N
odd n = true <-> Odd n
Proof.n:N
odd n = true <-> Odd n
 destruct n.odd 0 = true <-> Odd 0
p:positive
odd (pos p) = true <-> Odd (pos p)
 split.odd 0 = true -> Odd 0
Odd 0 -> odd 0 = true
p:positive
odd (pos p) = true <-> Odd (pos p) discriminate.Odd 0 -> odd 0 = true
p:positive
odd (pos p) = true <-> Odd (pos p)
 intros (m,H).m:N
H:0 = 2 * m + 1
odd 0 = true
p:positive
odd (pos p) = true <-> Odd (pos p) now destruct m.p:positive
odd (pos p) = true <-> Odd (pos p)
 destruct p; simpl; split; try easy.p:positive
odd (pos p~1) = true -> Odd (pos p~1)
p:positive
Odd (pos p~0) -> odd (pos p~0) = true
odd 1 = true -> Odd 1
 now exists (pos p).p:positive
Odd (pos p~0) -> odd (pos p~0) = true
odd 1 = true -> Odd 1
 intros (m,H).p:positive
m:N
H:pos p~0 = 2 * m + 1
odd (pos p~0) = true
odd 1 = true -> Odd 1 now destruct m.odd 1 = true -> Odd 1
 now exists 0.
Qed.

Specification of the euclidean division

Theorem pos_div_eucl_spec (a:positive)(b:N) :
  let (q,r) := pos_div_eucl a b in pos a = q * b + r.a:positive
b:N
let (q, r) := pos_div_eucl a b in pos a = q * b + r
Proof.a:positive
b:N
let (q, r) := pos_div_eucl a b in pos a = q * b + r
  induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? succ_double r
  then (succ_double q, succ_double r - b)
  else (double q, succ_double r) in
pos a~1 = q * b + r
a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  (* a~1 *)
  destruct pos_div_eucl as (q,r).a:positive
b, q, r:N
IHa:pos a = q * b + r
let (q0, r0) :=
  if b <=? succ_double r
  then (succ_double q, succ_double r - b)
  else (double q, succ_double r) in
pos a~1 = q0 * b + r0
a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  change (pos a~1) with (succ_double (pos a)).a:positive
b, q, r:N
IHa:pos a = q * b + r
let (q0, r0) :=
  if b <=? succ_double r
  then (succ_double q, succ_double r - b)
  else (double q, succ_double r) in
succ_double (pos a) = q0 * b + r0
a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  rewrite IHa, succ_double_add, double_mul.a:positive
b, q, r:N
IHa:pos a = q * b + r
let (q0, r0) :=
  if b <=? succ_double r
  then (succ_double q, succ_double r - b)
  else (double q, succ_double r) in
double q * b + succ_double r = q0 * b + r0
a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  case leb_spec; intros H; trivial.a:positive
b, q, r:N
IHa:pos a = q * b + r
H:b <= succ_double r
double q * b + succ_double r =
succ_double q * b + (succ_double r - b)
a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  rewrite succ_double_mul, <- add_assoc.a:positive
b, q, r:N
IHa:pos a = q * b + r
H:b <= succ_double r
double q * b + succ_double r =
double q * b + (b + (succ_double r - b))
a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r f_equal.a:positive
b, q, r:N
IHa:pos a = q * b + r
H:b <= succ_double r
succ_double r = b + (succ_double r - b)
a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  now rewrite (add_comm b), sub_add.a:positive
b:N
IHa:let (q, r) := pos_div_eucl a b in pos a = q * b + r
let (q, r) :=
  let (q, r) := pos_div_eucl a b in
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q * b + r
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  (* a~0 *)
  destruct pos_div_eucl as (q,r).a:positive
b, q, r:N
IHa:pos a = q * b + r
let (q0, r0) :=
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
pos a~0 = q0 * b + r0
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  change (pos a~0) with (double (pos a)).a:positive
b, q, r:N
IHa:pos a = q * b + r
let (q0, r0) :=
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
double (pos a) = q0 * b + r0
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  rewrite IHa, double_add, double_mul.a:positive
b, q, r:N
IHa:pos a = q * b + r
let (q0, r0) :=
  if b <=? double r
  then (succ_double q, double r - b)
  else (double q, double r) in
double q * b + double r = q0 * b + r0
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  case leb_spec; intros H; trivial.a:positive
b, q, r:N
IHa:pos a = q * b + r
H:b <= double r
double q * b + double r =
succ_double q * b + (double r - b)
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  rewrite succ_double_mul, <- add_assoc.a:positive
b, q, r:N
IHa:pos a = q * b + r
H:b <= double r
double q * b + double r =
double q * b + (b + (double r - b))
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r f_equal.a:positive
b, q, r:N
IHa:pos a = q * b + r
H:b <= double r
double r = b + (double r - b)
b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  now rewrite (add_comm b), sub_add.b:N
let (q, r) :=
  match b with
  | 1 => (1, 0)
  | _ => (0, 1)
  end in
1 = q * b + r
  (* 1 *)
  now destruct b as [|[ | | ]].
Qed.

Theorem div_eucl_spec a b :
 let (q,r) := div_eucl a b in a = b * q + r.a, b:N
let (q, r) := div_eucl a b in a = b * q + r
Proof.a, b:N
let (q, r) := div_eucl a b in a = b * q + r
  destruct a as [|a], b as [|b]; unfold div_eucl; trivial.a, b:positive
let (q, r) := pos_div_eucl a (pos b) in
pos a = pos b * q + r
  generalize (pos_div_eucl_spec a (pos b)).a, b:positive
(let (q, r) := pos_div_eucl a (pos b) in
 pos a = q * pos b + r) ->
let (q, r) := pos_div_eucl a (pos b) in
pos a = pos b * q + r
  destruct pos_div_eucl.a, b:positive
n, n0:N
pos a = n * pos b + n0 -> pos a = pos b * n + n0 now rewrite mul_comm.
Qed.

Theorem div_mod' a b : a = b * (a/b) + (a mod b).a, b:N
a = b * (a / b) + a mod b
Proof.a, b:N
a = b * (a / b) + a mod b
  generalize (div_eucl_spec a b).a, b:N
(let (q, r) := div_eucl a b in a = b * q + r) ->
a = b * (a / b) + a mod b
  unfold div, modulo.a, b:N
(let (q, r) := div_eucl a b in a = b * q + r) ->
a = b * fst (div_eucl a b) + snd (div_eucl a b) now destruct div_eucl.
Qed.

Definition div_mod a b : b<>0 -> a = b * (a/b) + (a mod b).a, b:N
b <> 0 -> a = b * (a / b) + a mod b
Proof.a, b:N
b <> 0 -> a = b * (a / b) + a mod b
 intros _.a, b:N
a = b * (a / b) + a mod b apply div_mod'.
Qed.

Theorem pos_div_eucl_remainder (a:positive) (b:N) :
  b<>0 -> snd (pos_div_eucl a b) < b.a:positive
b:N
b <> 0 -> snd (pos_div_eucl a b) < b
Proof.a:positive
b:N
b <> 0 -> snd (pos_div_eucl a b) < b
  intros Hb.a:positive
b:N
Hb:b <> 0
snd (pos_div_eucl a b) < b
  induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? succ_double r
   then (succ_double q, succ_double r - b)
   else (double q, succ_double r)) < b
a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  (* a~1 *)
  destruct pos_div_eucl as (q,r); simpl in *.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
snd
  (if b <=? succ_double r
   then (succ_double q, succ_double r - b)
   else (double q, succ_double r)) < b
a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  case leb_spec; intros H; simpl; trivial.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
H:b <= succ_double r
succ_double r - b < b
a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  apply add_lt_mono_l with b.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
H:b <= succ_double r
b + (succ_double r - b) < b + b
a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b rewrite add_comm, sub_add by trivial.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
H:b <= succ_double r
succ_double r < b + b
a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].a, b:positive
Hb:pos b <> 0
q, r:N
IHa:r < pos b
H:pos b <= succ_double r
succ_double r < pos b~0
a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  apply (succ_double_lt _ _ IHa).a:positive
b:N
Hb:b <> 0
IHa:snd (pos_div_eucl a b) < b
snd
  (let (q, r) := pos_div_eucl a b in
   if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  (* a~0 *)
  destruct pos_div_eucl as (q,r); simpl in *.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
snd
  (if b <=? double r
   then (succ_double q, double r - b)
   else (double q, double r)) < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  case leb_spec; intros H; simpl; trivial.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
H:b <= double r
double r - b < b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  apply add_lt_mono_l with b.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
H:b <= double r
b + (double r - b) < b + b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b rewrite add_comm, sub_add by trivial.a:positive
b:N
Hb:b <> 0
q, r:N
IHa:r < b
H:b <= double r
double r < b + b
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ].a, b:positive
Hb:pos b <> 0
q, r:N
IHa:r < pos b
H:pos b <= double r
double r < pos b~0
b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  now destruct r.b:N
Hb:b <> 0
snd match b with
    | 1 => (1, 0)
    | _ => (0, 1)
    end < b
  (* 1 *)
  destruct b as [|[ | | ]]; easy || (now destruct Hb).
Qed.

Theorem mod_lt a b : b<>0 -> a mod b < b.a, b:N
b <> 0 -> a mod b < b
Proof.a, b:N
b <> 0 -> a mod b < b
  destruct b as [ |b].a:N
0 <> 0 -> a mod 0 < 0
a:N
b:positive
pos b <> 0 -> a mod pos b < pos b now destruct 1.a:N
b:positive
pos b <> 0 -> a mod pos b < pos b
  destruct a as [ |a].b:positive
pos b <> 0 -> 0 mod pos b < pos b
a, b:positive
pos b <> 0 -> pos a mod pos b < pos b reflexivity.a, b:positive
pos b <> 0 -> pos a mod pos b < pos b
  unfold modulo.a, b:positive
pos b <> 0 -> snd (div_eucl (pos a) (pos b)) < pos b simpl.a, b:positive
pos b <> 0 -> snd (pos_div_eucl a (pos b)) < pos b apply pos_div_eucl_remainder.
Qed.

Theorem mod_bound_pos a b : 0<=a -> 0<b -> 0 <= a mod b < b.a, b:N
0 <= a -> 0 < b -> 0 <= a mod b < b
Proof.a, b:N
0 <= a -> 0 < b -> 0 <= a mod b < b
 intros _ H.a, b:N
H:0 < b
0 <= a mod b < b split.a, b:N
H:0 < b
0 <= a mod b
a, b:N
H:0 < b
a mod b < b apply le_0_l.a, b:N
H:0 < b
a mod b < b apply mod_lt.a, b:N
H:0 < b
b <> 0 now destruct b.
Qed.

Specification of square root

Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.n:N
fst (sqrtrem n) = sqrt n
Proof.n:N
fst (sqrtrem n) = sqrt n
 destruct n.fst (sqrtrem 0) = sqrt 0
p:positive
fst (sqrtrem (pos p)) = sqrt (pos p) reflexivity.p:positive
fst (sqrtrem (pos p)) = sqrt (pos p)
 unfold sqrtrem, sqrt, Pos.sqrt.p:positive
fst
  (let (s, m) := Pos.sqrtrem p in
   match m with
   | Pos.IsPos r => (pos s, pos r)
   | _ => (pos s, 0)
   end) = pos (fst (Pos.sqrtrem p))
 destruct (Pos.sqrtrem p) as (s,r).p, s:positive
r:Pos.mask
fst
  match r with
  | Pos.IsPos r0 => (pos s, pos r0)
  | _ => (pos s, 0)
  end = pos (fst (s, r)) now destruct r.
Qed.

Lemma sqrtrem_spec n :
 let (s,r) := sqrtrem n in n = s*s + r /\ r <= 2*s.n:N
let (s, r) := sqrtrem n in n = s * s + r /\ r <= 2 * s
Proof.n:N
let (s, r) := sqrtrem n in n = s * s + r /\ r <= 2 * s
 destruct n.let (s, r) := sqrtrem 0 in 0 = s * s + r /\ r <= 2 * s
p:positive
let (s, r) := sqrtrem (pos p) in
pos p = s * s + r /\ r <= 2 * s now split.p:positive
let (s, r) := sqrtrem (pos p) in
pos p = s * s + r /\ r <= 2 * s
 generalize (Pos.sqrtrem_spec p).p:positive
Pos.SqrtSpec (Pos.sqrtrem p) p ->
let (s, r) := sqrtrem (pos p) in
pos p = s * s + r /\ r <= 2 * s simpl.p:positive
Pos.SqrtSpec (Pos.sqrtrem p) p ->
let (s, r) :=
  let (s, m) := Pos.sqrtrem p in
  match m with
  | Pos.IsPos r => (pos s, pos r)
  | _ => (pos s, 0)
  end in
pos p = s * s + r /\
r <= match s with
     | 0 => 0
     | pos q => pos q~0
     end
 destruct 1; simpl; subst; now split.
Qed.

Lemma sqrt_spec n : 0<=n ->
 let s := sqrt n in s*s <= n < (succ s)*(succ s).n:N
0 <= n ->
let s := sqrt n in s * s <= n < succ s * succ s
Proof.n:N
0 <= n ->
let s := sqrt n in s * s <= n < succ s * succ s
 intros _.n:N
let s := sqrt n in s * s <= n < succ s * succ s destruct n.let s := sqrt 0 in s * s <= 0 < succ s * succ s
p:positive
let s := sqrt (pos p) in
s * s <= pos p < succ s * succ s now split.p:positive
let s := sqrt (pos p) in
s * s <= pos p < succ s * succ s apply (Pos.sqrt_spec p).
Qed.

Lemma sqrt_neg n : n<0 -> sqrt n = 0.n:N
n < 0 -> sqrt n = 0
Proof.n:N
n < 0 -> sqrt n = 0
 now destruct n.
Qed.

Specification of gcd

The first component of ggcd is gcd

Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.a, b:N
fst (ggcd a b) = gcd a b
Proof.a, b:N
fst (ggcd a b) = gcd a b
 destruct a as [|p], b as [|q]; simpl; auto.p, q:positive
fst
  (let
   '(g, (aa, bb)) := Pos.ggcd p q in
    (pos g, (pos aa, pos bb))) = pos (Pos.gcd p q)
 assert (H := Pos.ggcd_gcd p q).p, q:positive
H:fst (Pos.ggcd p q) = Pos.gcd p q
fst
  (let
   '(g, (aa, bb)) := Pos.ggcd p q in
    (pos g, (pos aa, pos bb))) = pos (Pos.gcd p q)
 destruct Pos.ggcd as (g,(aa,bb)); simpl; now f_equal.
Qed.

The other components of ggcd are indeed the correct factors.

Lemma ggcd_correct_divisors a b :
  let '(g,(aa,bb)) := ggcd a b in
  a=g*aa /\ b=g*bb.a, b:N
let
'(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb
Proof.a, b:N
let
'(g, (aa, bb)) := ggcd a b in a = g * aa /\ b = g * bb
 destruct a as [|p], b as [|q]; simpl; auto.q:positive
0 = 0 /\ pos q = pos (q * 1)
p:positive
pos p = pos (p * 1) /\ 0 = 0
p, q:positive
let
'(g, (aa, bb)) :=
 let
 '(g, (aa, bb)) := Pos.ggcd p q in
  (pos g, (pos aa, pos bb)) in
 pos p = g * aa /\ pos q = g * bb
 now rewrite Pos.mul_1_r.p:positive
pos p = pos (p * 1) /\ 0 = 0
p, q:positive
let
'(g, (aa, bb)) :=
 let
 '(g, (aa, bb)) := Pos.ggcd p q in
  (pos g, (pos aa, pos bb)) in
 pos p = g * aa /\ pos q = g * bb
 now rewrite Pos.mul_1_r.p, q:positive
let
'(g, (aa, bb)) :=
 let
 '(g, (aa, bb)) := Pos.ggcd p q in
  (pos g, (pos aa, pos bb)) in
 pos p = g * aa /\ pos q = g * bb
 generalize (Pos.ggcd_correct_divisors p q).p, q:positive
(let
 '(g, (aa, bb)) := Pos.ggcd p q in
  p = (g * aa)%positive /\ q = (g * bb)%positive) ->
let
'(g, (aa, bb)) :=
 let
 '(g, (aa, bb)) := Pos.ggcd p q in
  (pos g, (pos aa, pos bb)) in
 pos p = g * aa /\ pos q = g * bb
 destruct Pos.ggcd as (g,(aa,bb)); simpl.p, q, g, aa, bb:positive
p = (g * aa)%positive /\ q = (g * bb)%positive ->
pos p = pos (g * aa) /\ pos q = pos (g * bb)
 destruct 1; split; now f_equal.
Qed.

We can use this fact to prove a part of the gcd correctness

Lemma gcd_divide_l a b : (gcd a b | a).a, b:N
(gcd a b | a)
Proof.a, b:N
(gcd a b | a)
 rewrite <- ggcd_gcd.a, b:N
(fst (ggcd a b) | a) generalize (ggcd_correct_divisors a b).a, b:N
(let
 '(g, (aa, bb)) := ggcd a b in
  a = g * aa /\ b = g * bb) -> (fst (ggcd a b) | a)
 destruct ggcd as (g,(aa,bb)); simpl.a, b, g, aa, bb:N
a = g * aa /\ b = g * bb -> (g | a) intros (H,_).a, b, g, aa, bb:N
H:a = g * aa
(g | a) exists aa.a, b, g, aa, bb:N
H:a = g * aa
a = aa * g
  now rewrite mul_comm.
Qed.

Lemma gcd_divide_r a b : (gcd a b | b).a, b:N
(gcd a b | b)
Proof.a, b:N
(gcd a b | b)
 rewrite <- ggcd_gcd.a, b:N
(fst (ggcd a b) | b) generalize (ggcd_correct_divisors a b).a, b:N
(let
 '(g, (aa, bb)) := ggcd a b in
  a = g * aa /\ b = g * bb) -> (fst (ggcd a b) | b)
 destruct ggcd as (g,(aa,bb)); simpl.a, b, g, aa, bb:N
a = g * aa /\ b = g * bb -> (g | b) intros (_,H).a, b, g, aa, bb:N
H:b = g * bb
(g | b) exists bb.a, b, g, aa, bb:N
H:b = g * bb
b = bb * g
  now rewrite mul_comm.
Qed.

We now prove directly that gcd is the greatest amongst common divisors

Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c|gcd a b).a, b, c:N
(c | a) -> (c | b) -> (c | gcd a b)
Proof.a, b, c:N
(c | a) -> (c | b) -> (c | gcd a b)
 destruct a as [ |p], b as [ |q]; simpl; trivial.p, q:positive
c:N
(c | pos p) -> (c | pos q) -> (c | pos (Pos.gcd p q))
 destruct c as [ |r].p, q:positive
(0 | pos p) -> (0 | pos q) -> (0 | pos (Pos.gcd p q))
p, q, r:positive
(pos r | pos p) ->
(pos r | pos q) -> (pos r | pos (Pos.gcd p q)) intros (s,H).p, q:positive
s:N
H:pos p = s * 0
(0 | pos q) -> (0 | pos (Pos.gcd p q))
p, q, r:positive
(pos r | pos p) ->
(pos r | pos q) -> (pos r | pos (Pos.gcd p q)) destruct s; discriminate.p, q, r:positive
(pos r | pos p) ->
(pos r | pos q) -> (pos r | pos (Pos.gcd p q))
 intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *.p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
(pos r | pos (Pos.gcd p q))
 destruct (Pos.gcd_greatest p q r) as (u,H).p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
(r | p)%positive
p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
(r | q)%positive
p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
u:positive
H:Pos.gcd p q = (u * r)%positive
(pos r | pos (Pos.gcd p q))
 exists s.p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
p = (s * r)%positive
p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
(r | q)%positive
p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
u:positive
H:Pos.gcd p q = (u * r)%positive
(pos r | pos (Pos.gcd p q)) now inversion Hs.p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
(r | q)%positive
p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
u:positive
H:Pos.gcd p q = (u * r)%positive
(pos r | pos (Pos.gcd p q))
 exists t.p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
q = (t * r)%positive
p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
u:positive
H:Pos.gcd p q = (u * r)%positive
(pos r | pos (Pos.gcd p q)) now inversion Ht.p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
u:positive
H:Pos.gcd p q = (u * r)%positive
(pos r | pos (Pos.gcd p q))
 exists (pos u).p, q, r, s:positive
Hs:pos p = pos (s * r)
t:positive
Ht:pos q = pos (t * r)
u:positive
H:Pos.gcd p q = (u * r)%positive
pos (Pos.gcd p q) = pos u * pos r simpl; now f_equal.
Qed.

Lemma gcd_nonneg a b : 0 <= gcd a b.a, b:N
0 <= gcd a b
Proof.a, b:N
0 <= gcd a b apply le_0_l. Qed.

Specification of bitwise functions

Correctness proofs for testbit.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.a:N
testbit (2 * a) 0 = false
Proof.a:N
testbit (2 * a) 0 = false
 now destruct a.
Qed.

Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.a:N
testbit (2 * a + 1) 0 = true
Proof.a:N
testbit (2 * a + 1) 0 = true
 now destruct a.
Qed.

Lemma testbit_succ_r_div2 a n : 0<=n ->
 testbit a (succ n) = testbit (div2 a) n.a, n:N
0 <= n -> testbit a (succ n) = testbit (div2 a) n
Proof.a, n:N
0 <= n -> testbit a (succ n) = testbit (div2 a) n
 intros _.a, n:N
testbit a (succ n) = testbit (div2 a) n destruct a as [|[a|a| ]], n as [|n]; simpl; trivial;
  f_equal; apply Pos.pred_N_succ.
Qed.

Lemma testbit_odd_succ a n : 0<=n ->
 testbit (2*a+1) (succ n) = testbit a n.a, n:N
0 <= n -> testbit (2 * a + 1) (succ n) = testbit a n
Proof.a, n:N
0 <= n -> testbit (2 * a + 1) (succ n) = testbit a n
 intros H.a, n:N
H:0 <= n
testbit (2 * a + 1) (succ n) = testbit a n rewrite testbit_succ_r_div2 by trivial.a, n:N
H:0 <= n
testbit (div2 (2 * a + 1)) n = testbit a n f_equal.a, n:N
H:0 <= n
div2 (2 * a + 1) = a now destruct a.
Qed.

Lemma testbit_even_succ a n : 0<=n ->
 testbit (2*a) (succ n) = testbit a n.a, n:N
0 <= n -> testbit (2 * a) (succ n) = testbit a n
Proof.a, n:N
0 <= n -> testbit (2 * a) (succ n) = testbit a n
 intros H.a, n:N
H:0 <= n
testbit (2 * a) (succ n) = testbit a n rewrite testbit_succ_r_div2 by trivial.a, n:N
H:0 <= n
testbit (div2 (2 * a)) n = testbit a n f_equal.a, n:N
H:0 <= n
div2 (2 * a) = a now destruct a.
Qed.

Lemma testbit_neg_r a n : n<0 -> testbit a n = false.a, n:N
n < 0 -> testbit a n = false
Proof.a, n:N
n < 0 -> testbit a n = false
 now destruct n.
Qed.

Correctness proofs for shifts

Lemma shiftr_succ_r a n :
 shiftr a (succ n) = div2 (shiftr a n).a, n:N
shiftr a (succ n) = div2 (shiftr a n)
Proof.a, n:N
shiftr a (succ n) = div2 (shiftr a n)
 destruct n; simpl; trivial.a:N
p:positive
Pos.iter div2 a (Pos.succ p) =
div2 (Pos.iter div2 a p) apply Pos.iter_succ.
Qed.

Lemma shiftl_succ_r a n :
 shiftl a (succ n) = double (shiftl a n).a, n:N
shiftl a (succ n) = double (shiftl a n)
Proof.a, n:N
shiftl a (succ n) = double (shiftl a n)
 destruct n, a; simpl; trivial.p0, p:positive
pos (Pos.iter xO p0 (Pos.succ p)) =
pos (Pos.iter xO p0 p)~0 f_equal.p0, p:positive
Pos.iter xO p0 (Pos.succ p) =
((Pos.iter xO p0 p)~0)%positive apply Pos.iter_succ.
Qed.

Lemma shiftr_spec a n m : 0<=m ->
 testbit (shiftr a n) m = testbit a (m+n).a, n, m:N
0 <= m -> testbit (shiftr a n) m = testbit a (m + n)
Proof.a, n, m:N
0 <= m -> testbit (shiftr a n) m = testbit a (m + n)
 intros _.a, n, m:N
testbit (shiftr a n) m = testbit a (m + n) revert a m.n:N
forall a m : N,
testbit (shiftr a n) m = testbit a (m + n)
 induction n using peano_ind; intros a m.a, m:N
testbit (shiftr a 0) m = testbit a (m + 0)
n:N
IHn:forall a0 m0 : N, testbit (shiftr a0 n) m0 = testbit a0 (m0 + n)
a, m:N
testbit (shiftr a (succ n)) m = testbit a (m + succ n) now rewrite add_0_r.n:N
IHn:forall a0 m0 : N, testbit (shiftr a0 n) m0 = testbit a0 (m0 + n)
a, m:N
testbit (shiftr a (succ n)) m = testbit a (m + succ n)
 rewrite add_comm, add_succ_l, add_comm, <- add_succ_l.n:N
IHn:forall a0 m0 : N, testbit (shiftr a0 n) m0 = testbit a0 (m0 + n)
a, m:N
testbit (shiftr a (succ n)) m = testbit a (succ m + n)
 now rewrite <- IHn, testbit_succ_r_div2, shiftr_succ_r by apply le_0_l.
Qed.

Lemma shiftl_spec_high a n m : 0<=m -> n<=m ->
 testbit (shiftl a n) m = testbit a (m-n).a, n, m:N
0 <= m ->
n <= m -> testbit (shiftl a n) m = testbit a (m - n)
Proof.a, n, m:N
0 <= m ->
n <= m -> testbit (shiftl a n) m = testbit a (m - n)
 intros _ H.a, n, m:N
H:n <= m
testbit (shiftl a n) m = testbit a (m - n)
 rewrite <- (sub_add n m H) at 1.a, n, m:N
H:n <= m
testbit (shiftl a n) (m - n + n) = testbit a (m - n)
 set (m' := m-n).a, n, m:N
H:n <= m
m':=m - n:N
testbit (shiftl a n) (m' + n) = testbit a m' clearbody m'.a, n, m:N
H:n <= m
m':N
testbit (shiftl a n) (m' + n) = testbit a m' clear H m.a, n, m':N
testbit (shiftl a n) (m' + n) = testbit a m' revert a m'.n:N
forall a m' : N,
testbit (shiftl a n) (m' + n) = testbit a m'
 induction n using peano_ind; intros a m.a, m:N
testbit (shiftl a 0) (m + 0) = testbit a m
n:N
IHn:forall a0 m' : N, testbit (shiftl a0 n) (m' + n) = testbit a0 m'
a, m:N
testbit (shiftl a (succ n)) (m + succ n) = testbit a m
 rewrite add_0_r; now destruct a.n:N
IHn:forall a0 m' : N, testbit (shiftl a0 n) (m' + n) = testbit a0 m'
a, m:N
testbit (shiftl a (succ n)) (m + succ n) = testbit a m
 rewrite shiftl_succ_r.n:N
IHn:forall a0 m' : N, testbit (shiftl a0 n) (m' + n) = testbit a0 m'
a, m:N
testbit (double (shiftl a n)) (m + succ n) =
testbit a m
 rewrite add_comm, add_succ_l, add_comm.n:N
IHn:forall a0 m' : N, testbit (shiftl a0 n) (m' + n) = testbit a0 m'
a, m:N
testbit (double (shiftl a n)) (succ (m + n)) =
testbit a m
 now rewrite testbit_succ_r_div2, div2_double by apply le_0_l.
Qed.

Lemma shiftl_spec_low a n m : m<n ->
 testbit (shiftl a n) m = false.a, n, m:N
m < n -> testbit (shiftl a n) m = false
Proof.a, n, m:N
m < n -> testbit (shiftl a n) m = false
 revert a m.n:N
forall a m : N,
m < n -> testbit (shiftl a n) m = false
 induction n using peano_ind; intros a m H.a, m:N
H:m < 0
testbit (shiftl a 0) m = false
n:N
IHn:forall a0 m0 : N, m0 < n -> testbit (shiftl a0 n) m0 = false
a, m:N
H:m < succ n
testbit (shiftl a (succ n)) m = false
 elim (le_0_l m).a, m:N
H:m < 0
(0 ?= m) = Gt
n:N
IHn:forall a0 m0 : N, m0 < n -> testbit (shiftl a0 n) m0 = false
a, m:N
H:m < succ n
testbit (shiftl a (succ n)) m = false now rewrite compare_antisym, H.n:N
IHn:forall a0 m0 : N, m0 < n -> testbit (shiftl a0 n) m0 = false
a, m:N
H:m < succ n
testbit (shiftl a (succ n)) m = false
 rewrite shiftl_succ_r.n:N
IHn:forall a0 m0 : N, m0 < n -> testbit (shiftl a0 n) m0 = false
a, m:N
H:m < succ n
testbit (double (shiftl a n)) m = false
 destruct m.n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
H:0 < succ n
testbit (double (shiftl a n)) 0 = false
n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
p:positive
H:pos p < succ n
testbit (double (shiftl a n)) (pos p) = false now destruct (shiftl a n).n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
p:positive
H:pos p < succ n
testbit (double (shiftl a n)) (pos p) = false
 rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l.n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
p:positive
H:pos p < succ n
testbit (shiftl a n) (Pos.pred_N p) = false
 apply IHn.n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
p:positive
H:pos p < succ n
Pos.pred_N p < n
 apply add_lt_mono_l with 1.n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
p:positive
H:pos p < succ n
1 + Pos.pred_N p < 1 + n rewrite 2 (add_succ_l 0).n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
p:positive
H:pos p < succ n
succ (0 + Pos.pred_N p) < succ (0 + n) simpl.n:N
IHn:forall a0 m : N, m < n -> testbit (shiftl a0 n) m = false
a:N
p:positive
H:pos p < succ n
succ (Pos.pred_N p) < succ n
 now rewrite succ_pos_pred.
Qed.

Definition div2_spec a : div2 a = shiftr a 1.a:N
div2 a = shiftr a 1
Proof.a:N
div2 a = shiftr a 1
 reflexivity.
Qed.

Semantics of bitwise operations

Lemma pos_lxor_spec p p' n :
 testbit (Pos.lxor p p') n = xorb (Pos.testbit p n) (Pos.testbit p' n).p, p':positive
n:N
testbit (Pos.lxor p p') n =
xorb (Pos.testbit p n) (Pos.testbit p' n)
Proof.p, p':positive
n:N
testbit (Pos.lxor p p') n =
xorb (Pos.testbit p n) (Pos.testbit p' n)
 revert p' n.p:positive
forall (p' : positive) (n : N),
testbit (Pos.lxor p p') n =
xorb (Pos.testbit p n) (Pos.testbit p' n)
 induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
 (specialize (IH p'); destruct Pos.lxor; trivial; now rewrite <-IH) ||
 (now destruct Pos.testbit).
Qed.

Lemma lxor_spec a a' n :
 testbit (lxor a a') n = xorb (testbit a n) (testbit a' n).a, a', n:N
testbit (lxor a a') n =
xorb (testbit a n) (testbit a' n)
Proof.a, a', n:N
testbit (lxor a a') n =
xorb (testbit a n) (testbit a' n)
 destruct a, a'; simpl; trivial.p:positive
n:N
Pos.testbit p n =
(if Pos.testbit p n then true else false)
p:positive
n:N
Pos.testbit p n = xorb (Pos.testbit p n) false
p, p0:positive
n:N
testbit (Pos.lxor p p0) n =
xorb (Pos.testbit p n) (Pos.testbit p0 n)
 now destruct Pos.testbit.p:positive
n:N
Pos.testbit p n = xorb (Pos.testbit p n) false
p, p0:positive
n:N
testbit (Pos.lxor p p0) n =
xorb (Pos.testbit p n) (Pos.testbit p0 n)
 now destruct Pos.testbit.p, p0:positive
n:N
testbit (Pos.lxor p p0) n =
xorb (Pos.testbit p n) (Pos.testbit p0 n)
 apply pos_lxor_spec.
Qed.

Lemma pos_lor_spec p p' n :
 Pos.testbit (Pos.lor p p') n = (Pos.testbit p n) || (Pos.testbit p' n).p, p':positive
n:N
Pos.testbit (Pos.lor p p') n =
Pos.testbit p n || Pos.testbit p' n
Proof.p, p':positive
n:N
Pos.testbit (Pos.lor p p') n =
Pos.testbit p n || Pos.testbit p' n
 revert p' n.p:positive
forall (p' : positive) (n : N),
Pos.testbit (Pos.lor p p') n =
Pos.testbit p n || Pos.testbit p' n
 induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
  apply IH || now rewrite orb_false_r.
Qed.

Lemma lor_spec a a' n :
 testbit (lor a a') n = (testbit a n) || (testbit a' n).a, a', n:N
testbit (lor a a') n = testbit a n || testbit a' n
Proof.a, a', n:N
testbit (lor a a') n = testbit a n || testbit a' n
 destruct a, a'; simpl; trivial.p:positive
n:N
Pos.testbit p n = Pos.testbit p n || false
p, p0:positive
n:N
Pos.testbit (Pos.lor p p0) n =
Pos.testbit p n || Pos.testbit p0 n
 now rewrite orb_false_r.p, p0:positive
n:N
Pos.testbit (Pos.lor p p0) n =
Pos.testbit p n || Pos.testbit p0 n
 apply pos_lor_spec.
Qed.

Lemma pos_land_spec p p' n :
 testbit (Pos.land p p') n = (Pos.testbit p n) && (Pos.testbit p' n).p, p':positive
n:N
testbit (Pos.land p p') n =
Pos.testbit p n && Pos.testbit p' n
Proof.p, p':positive
n:N
testbit (Pos.land p p') n =
Pos.testbit p n && Pos.testbit p' n
 revert p' n.p:positive
forall (p' : positive) (n : N),
testbit (Pos.land p p') n =
Pos.testbit p n && Pos.testbit p' n
 induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
 (specialize (IH p'); destruct Pos.land; trivial; now rewrite <-IH) ||
 (now rewrite andb_false_r).
Qed.

Lemma land_spec a a' n :
 testbit (land a a') n = (testbit a n) && (testbit a' n).a, a', n:N
testbit (land a a') n = testbit a n && testbit a' n
Proof.a, a', n:N
testbit (land a a') n = testbit a n && testbit a' n
 destruct a, a'; simpl; trivial.p:positive
n:N
false = Pos.testbit p n && false
p, p0:positive
n:N
testbit (Pos.land p p0) n =
Pos.testbit p n && Pos.testbit p0 n
 now rewrite andb_false_r.p, p0:positive
n:N
testbit (Pos.land p p0) n =
Pos.testbit p n && Pos.testbit p0 n
 apply pos_land_spec.
Qed.

Lemma pos_ldiff_spec p p' n :
 testbit (Pos.ldiff p p') n = (Pos.testbit p n) && negb (Pos.testbit p' n).p, p':positive
n:N
testbit (Pos.ldiff p p') n =
Pos.testbit p n && negb (Pos.testbit p' n)
Proof.p, p':positive
n:N
testbit (Pos.ldiff p p') n =
Pos.testbit p n && negb (Pos.testbit p' n)
 revert p' n.p:positive
forall (p' : positive) (n : N),
testbit (Pos.ldiff p p') n =
Pos.testbit p n && negb (Pos.testbit p' n)
 induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl;
 (specialize (IH p'); destruct Pos.ldiff; trivial; now rewrite <-IH) ||
 (now rewrite andb_true_r).
Qed.

Lemma ldiff_spec a a' n :
 testbit (ldiff a a') n = (testbit a n) && negb (testbit a' n).a, a', n:N
testbit (ldiff a a') n =
testbit a n && negb (testbit a' n)
Proof.a, a', n:N
testbit (ldiff a a') n =
testbit a n && negb (testbit a' n)
 destruct a, a'; simpl; trivial.p:positive
n:N
Pos.testbit p n = Pos.testbit p n && true
p, p0:positive
n:N
testbit (Pos.ldiff p p0) n =
Pos.testbit p n && negb (Pos.testbit p0 n)
 now rewrite andb_true_r.p, p0:positive
n:N
testbit (Pos.ldiff p p0) n =
Pos.testbit p n && negb (Pos.testbit p0 n)
 apply pos_ldiff_spec.
Qed.

Instantiation of generic properties of advanced functions (pow, sqrt, log2, div, gcd, ...)

Include NExtraProp.

In generic statements, the predicates lt and le have been favored, whereas gt and ge don't even exist in the abstract layers. The use of gt and ge is hence not recommended. We provide here the bare minimal results to related them with lt and le.

Lemma gt_lt_iff n m : n > m <-> m < n.n, m:N
n > m <-> m < n
Proof.n, m:N
n > m <-> m < n
 unfold lt, gt.n, m:N
(n ?= m) = Gt <-> (m ?= n) = Lt now rewrite compare_antisym, CompOpp_iff.
Qed.

Lemma gt_lt n m : n > m -> m < n.n, m:N
n > m -> m < n
Proof.n, m:N
n > m -> m < n
 apply gt_lt_iff.
Qed.

Lemma lt_gt n m : n < m -> m > n.n, m:N
n < m -> m > n
Proof.n, m:N
n < m -> m > n
 apply gt_lt_iff.
Qed.

Lemma ge_le_iff n m : n >= m <-> m <= n.n, m:N
n >= m <-> m <= n
Proof.n, m:N
n >= m <-> m <= n
 unfold le, ge.n, m:N
(n ?= m) <> Lt <-> (m ?= n) <> Gt now rewrite compare_antisym, CompOpp_iff.
Qed.

Lemma ge_le n m : n >= m -> m <= n.n, m:N
n >= m -> m <= n
Proof.n, m:N
n >= m -> m <= n
 apply ge_le_iff.
Qed.

Lemma le_ge n m : n <= m -> m >= n.n, m:N
n <= m -> m >= n
Proof.n, m:N
n <= m -> m >= n
 apply ge_le_iff.
Qed.

Auxiliary results about right shift on positive numbers, used in BinInt

Lemma pos_pred_shiftl_low : forall p n m, m<n ->
 testbit (Pos.pred_N (Pos.shiftl p n)) m = true.forall (p : positive) (n m : N),
m < n ->
testbit (Pos.pred_N (Pos.shiftl p n)) m = true
Proof.forall (p : positive) (n m : N),
m < n ->
testbit (Pos.pred_N (Pos.shiftl p n)) m = true
 induction n using peano_ind.p:positive
forall m : N,
m < 0 ->
testbit (Pos.pred_N (Pos.shiftl p 0)) m = true
p:positive
n:N
IHn:forall m : N, m < n -> testbit (Pos.pred_N (Pos.shiftl p n)) m = true
forall m : N,
m < succ n ->
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m = true
 now destruct m.p:positive
n:N
IHn:forall m : N, m < n -> testbit (Pos.pred_N (Pos.shiftl p n)) m = true
forall m : N,
m < succ n ->
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m = true
 intros m H.p:positive
n:N
IHn:forall m0 : N, m0 < n -> testbit (Pos.pred_N (Pos.shiftl p n)) m0 = true
m:N
H:m < succ n
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m = true unfold Pos.shiftl.p:positive
n:N
IHn:forall m0 : N, m0 < n -> testbit (Pos.pred_N (Pos.shiftl p n)) m0 = true
m:N
H:m < succ n
testbit
  (Pos.pred_N
     match succ n with
     | 0%N => p
     | pos n0 => Pos.iter xO p n0
     end) m = true
 destruct n as [|n]; simpl in *.p:positive
IHn:forall m0 : N, m0 < 0 -> testbit (Pos.pred_N p) m0 = true
m:N
H:m < 1
Pos.testbit (Pos.pred_double p) m = true
p, n:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N (Pos.iter xO p n)) m0 = true
m:N
H:m < pos (Pos.succ n)
testbit (Pos.pred_N (Pos.iter xO p (Pos.succ n))) m =
true
 destruct m.p:positive
IHn:forall m : N, m < 0 -> testbit (Pos.pred_N p) m = true
H:0 < 1
Pos.testbit (Pos.pred_double p) 0 = true
p:positive
IHn:forall m : N, m < 0 -> testbit (Pos.pred_N p) m = true
p0:positive
H:pos p0 < 1
Pos.testbit (Pos.pred_double p) (pos p0) = true
p, n:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N (Pos.iter xO p n)) m0 = true
m:N
H:m < pos (Pos.succ n)
testbit (Pos.pred_N (Pos.iter xO p (Pos.succ n))) m =
true now destruct p.p:positive
IHn:forall m : N, m < 0 -> testbit (Pos.pred_N p) m = true
p0:positive
H:pos p0 < 1
Pos.testbit (Pos.pred_double p) (pos p0) = true
p, n:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N (Pos.iter xO p n)) m0 = true
m:N
H:m < pos (Pos.succ n)
testbit (Pos.pred_N (Pos.iter xO p (Pos.succ n))) m =
true elim (Pos.nlt_1_r _ H).p, n:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N (Pos.iter xO p n)) m0 = true
m:N
H:m < pos (Pos.succ n)
testbit (Pos.pred_N (Pos.iter xO p (Pos.succ n))) m =
true
 rewrite Pos.iter_succ.p, n:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N (Pos.iter xO p n)) m0 = true
m:N
H:m < pos (Pos.succ n)
testbit (Pos.pred_N (Pos.iter xO p n)~0) m = true simpl.p, n:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N (Pos.iter xO p n)) m0 = true
m:N
H:m < pos (Pos.succ n)
Pos.testbit (Pos.pred_double (Pos.iter xO p n)) m =
true
 set (u:=Pos.iter xO p n) in *; clearbody u.p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:N
H:m < pos (Pos.succ n)
Pos.testbit (Pos.pred_double u) m = true
 destruct m as [|m].p, n, u:positive
IHn:forall m : N, m < pos n -> testbit (Pos.pred_N u) m = true
H:0 < pos (Pos.succ n)
Pos.testbit (Pos.pred_double u) 0 = true
p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.testbit (Pos.pred_double u) (pos m) = true now destruct u.p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.testbit (Pos.pred_double u) (pos m) = true
 rewrite <- (IHn (Pos.pred_N m)).p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.testbit (Pos.pred_double u) (pos m) =
testbit (Pos.pred_N u) (Pos.pred_N m)
p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.pred_N m < pos n
 rewrite <- (testbit_odd_succ _ (Pos.pred_N m)).p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.testbit (Pos.pred_double u) (pos m) =
testbit (2 * Pos.pred_N u + 1) (succ (Pos.pred_N m))
p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
0 <= Pos.pred_N m
p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.pred_N m < pos n
 rewrite succ_pos_pred.p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.testbit (Pos.pred_double u) (pos m) =
testbit (2 * Pos.pred_N u + 1) (pos m)
p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
0 <= Pos.pred_N m
p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.pred_N m < pos n now destruct u.p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
0 <= Pos.pred_N m
p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.pred_N m < pos n
 apply le_0_l.p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
Pos.pred_N m < pos n
 apply succ_lt_mono.p, n, u:positive
IHn:forall m0 : N, m0 < pos n -> testbit (Pos.pred_N u) m0 = true
m:positive
H:pos m < pos (Pos.succ n)
succ (Pos.pred_N m) < succ (pos n) now rewrite succ_pos_pred.
Qed.

Lemma pos_pred_shiftl_high : forall p n m, n<=m ->
 testbit (Pos.pred_N (Pos.shiftl p n)) m =
 testbit (shiftl (Pos.pred_N p) n) m.forall (p : positive) (n m : N),
n <= m ->
testbit (Pos.pred_N (Pos.shiftl p n)) m =
testbit (shiftl (Pos.pred_N p) n) m
Proof.forall (p : positive) (n m : N),
n <= m ->
testbit (Pos.pred_N (Pos.shiftl p n)) m =
testbit (shiftl (Pos.pred_N p) n) m
 induction n using peano_ind; intros m H.p:positive
m:N
H:0 <= m
testbit (Pos.pred_N (Pos.shiftl p 0)) m =
testbit (shiftl (Pos.pred_N p) 0) m
p:positive
n:N
IHn:forall m0 : N,
n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p n)) m0 =
testbit (shiftl (Pos.pred_N p) n) m0
m:N
H:succ n <= m
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m =
testbit (shiftl (Pos.pred_N p) (succ n)) m
 unfold shiftl.p:positive
m:N
H:0 <= m
testbit (Pos.pred_N (Pos.shiftl p 0)) m =
testbit
  match Pos.pred_N p with
  | 0 => 0
  | pos a => pos (Pos.shiftl a 0)
  end m
p:positive
n:N
IHn:forall m0 : N,
n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p n)) m0 =
testbit (shiftl (Pos.pred_N p) n) m0
m:N
H:succ n <= m
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m =
testbit (shiftl (Pos.pred_N p) (succ n)) m simpl.p:positive
m:N
H:0 <= m
testbit (Pos.pred_N p) m =
testbit
  match Pos.pred_N p with
  | 0 => 0
  | pos a => pos a
  end m
p:positive
n:N
IHn:forall m0 : N,
n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p n)) m0 =
testbit (shiftl (Pos.pred_N p) n) m0
m:N
H:succ n <= m
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m =
testbit (shiftl (Pos.pred_N p) (succ n)) m now destruct (Pos.pred_N p).p:positive
n:N
IHn:forall m0 : N,
n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p n)) m0 =
testbit (shiftl (Pos.pred_N p) n) m0
m:N
H:succ n <= m
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m =
testbit (shiftl (Pos.pred_N p) (succ n)) m
 rewrite shiftl_succ_r.p:positive
n:N
IHn:forall m0 : N,
n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p n)) m0 =
testbit (shiftl (Pos.pred_N p) n) m0
m:N
H:succ n <= m
testbit (Pos.pred_N (Pos.shiftl p (succ n))) m =
testbit (double (shiftl (Pos.pred_N p) n)) m
 destruct n as [|n].p:positive
IHn:forall m0 : N,
0 <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p 0)) m0 =
testbit (shiftl (Pos.pred_N p) 0) m0
m:N
H:succ 0 <= m
testbit (Pos.pred_N (Pos.shiftl p (succ 0))) m =
testbit (double (shiftl (Pos.pred_N p) 0)) m
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:N
H:succ (pos n) <= m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n)))) m =
testbit (double (shiftl (Pos.pred_N p) (pos n))) m
 destruct m as [|m].p:positive
IHn:forall m : N,
0 <= m ->
testbit (Pos.pred_N (Pos.shiftl p 0)) m = testbit (shiftl (Pos.pred_N p) 0) m
H:succ 0 <= 0
testbit (Pos.pred_N (Pos.shiftl p (succ 0))) 0 =
testbit (double (shiftl (Pos.pred_N p) 0)) 0
p:positive
IHn:forall m0 : N,
0 <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p 0)) m0 =
testbit (shiftl (Pos.pred_N p) 0) m0
m:positive
H:succ 0 <= pos m
testbit (Pos.pred_N (Pos.shiftl p (succ 0))) (pos m) =
testbit (double (shiftl (Pos.pred_N p) 0)) (pos m)
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:N
H:succ (pos n) <= m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n)))) m =
testbit (double (shiftl (Pos.pred_N p) (pos n))) m now destruct H.p:positive
IHn:forall m0 : N,
0 <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p 0)) m0 =
testbit (shiftl (Pos.pred_N p) 0) m0
m:positive
H:succ 0 <= pos m
testbit (Pos.pred_N (Pos.shiftl p (succ 0))) (pos m) =
testbit (double (shiftl (Pos.pred_N p) 0)) (pos m)
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:N
H:succ (pos n) <= m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n)))) m =
testbit (double (shiftl (Pos.pred_N p) (pos n))) m now destruct p.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:N
H:succ (pos n) <= m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n)))) m =
testbit (double (shiftl (Pos.pred_N p) (pos n))) m
 destruct m as [|m].p, n:positive
IHn:forall m : N,
pos n <= m ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m =
testbit (shiftl (Pos.pred_N p) (pos n)) m
H:succ (pos n) <= 0
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n)))) 0 =
testbit (double (shiftl (Pos.pred_N p) (pos n))) 0
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n))))
  (pos m) =
testbit (double (shiftl (Pos.pred_N p) (pos n)))
  (pos m) now destruct H.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n))))
  (pos m) =
testbit (double (shiftl (Pos.pred_N p) (pos n)))
  (pos m)
 rewrite <- (succ_pos_pred m).p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n))))
  (succ (Pos.pred_N m)) =
testbit (double (shiftl (Pos.pred_N p) (pos n)))
  (succ (Pos.pred_N m))
 rewrite double_spec, testbit_even_succ by apply le_0_l.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n))))
  (succ (Pos.pred_N m)) =
testbit (shiftl (Pos.pred_N p) (pos n)) (Pos.pred_N m)
 rewrite <- IHn.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
testbit (Pos.pred_N (Pos.shiftl p (succ (pos n))))
  (succ (Pos.pred_N m)) =
testbit (Pos.pred_N (Pos.shiftl p (pos n)))
  (Pos.pred_N m)
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
pos n <= Pos.pred_N m
 rewrite testbit_succ_r_div2 by apply le_0_l.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
testbit
  (div2 (Pos.pred_N (Pos.shiftl p (succ (pos n)))))
  (Pos.pred_N m) =
testbit (Pos.pred_N (Pos.shiftl p (pos n)))
  (Pos.pred_N m)
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
pos n <= Pos.pred_N m
 f_equal.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
div2 (Pos.pred_N (Pos.shiftl p (succ (pos n)))) =
Pos.pred_N (Pos.shiftl p (pos n))
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
pos n <= Pos.pred_N m simpl.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
div2 (Pos.pred_N (Pos.iter xO p (Pos.succ n))) =
Pos.pred_N (Pos.iter xO p n)
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
pos n <= Pos.pred_N m rewrite Pos.iter_succ.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
div2 (Pos.pred_N (Pos.iter xO p n)~0) =
Pos.pred_N (Pos.iter xO p n)
p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
pos n <= Pos.pred_N m
 now destruct (Pos.iter xO p n).p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
pos n <= Pos.pred_N m
 apply succ_le_mono.p, n:positive
IHn:forall m0 : N,
pos n <= m0 ->
testbit (Pos.pred_N (Pos.shiftl p (pos n))) m0 =
testbit (shiftl (Pos.pred_N p) (pos n)) m0
m:positive
H:succ (pos n) <= pos m
succ (pos n) <= succ (Pos.pred_N m) now rewrite succ_pos_pred.
Qed.

Lemma pred_div2_up p : Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p).p:positive
Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p)
Proof.p:positive
Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p)
 destruct p as [p|p| ]; trivial.p:positive
Pos.pred_N (Pos.div2_up p~1) = div2 (Pos.pred_N p~1)
p:positive
Pos.pred_N (Pos.div2_up p~0) = div2 (Pos.pred_N p~0)
 simpl.p:positive
Pos.pred_N (Pos.succ p) = pos p
p:positive
Pos.pred_N (Pos.div2_up p~0) = div2 (Pos.pred_N p~0) apply Pos.pred_N_succ.p:positive
Pos.pred_N (Pos.div2_up p~0) = div2 (Pos.pred_N p~0)
 destruct p; simpl; trivial.
Qed.

End N.

Bind Scope N_scope with N.t N.

Exportation of notations

Numeral Notation N N.of_uint N.to_uint : N_scope.

Infix "+" := N.add : N_scope.
Infix "-" := N.sub : N_scope.
Infix "*" := N.mul : N_scope.
Infix "^" := N.pow : N_scope.

Infix "?=" := N.compare (at level 70, no associativity) : N_scope.

Infix "<=" := N.le : N_scope.
Infix "<" := N.lt : N_scope.
Infix ">=" := N.ge : N_scope.
Infix ">" := N.gt : N_scope.

Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope.
Notation "x <= y < z" := (x <= y /\ y < z) : N_scope.
Notation "x < y < z" := (x < y /\ y < z) : N_scope.
Notation "x < y <= z" := (x < y /\ y <= z) : N_scope.

Infix "=?" := N.eqb (at level 70, no associativity) : N_scope.
Infix "<=?" := N.leb (at level 70, no associativity) : N_scope.
Infix "<?" := N.ltb (at level 70, no associativity) : N_scope.

Infix "/" := N.div : N_scope.
Infix "mod" := N.modulo (at level 40, no associativity) : N_scope.

Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope.

Compatibility notations

Notation N_rect := N_rect (only parsing).
Notation N_rec := N_rec (only parsing).
Notation N_ind := N_ind (only parsing).
Notation N0 := N0 (only parsing).
Notation Npos := N.pos (only parsing).

Notation Ndouble_plus_one := N.succ_double (only parsing).
Notation Nplus := N.add (only parsing).
Notation Nminus := N.sub (only parsing).
Notation Nmult := N.mul (only parsing).

Notation nat_of_N := N.to_nat (only parsing).
Notation N_of_nat := N.of_nat (only parsing).
Notation Nrect := N.peano_rect (only parsing).
Notation Nrect_base := N.peano_rect_base (only parsing).
Notation Nrect_step := N.peano_rect_succ (only parsing).
Notation Nind := N.peano_ind (only parsing).
Notation Nrec := N.peano_rec (only parsing).
Notation Nrec_base := N.peano_rec_base (only parsing).
Notation Nrec_succ := N.peano_rec_succ (only parsing).

Notation Npred_minus := N.pred_sub (only parsing).
Notation Ppred_N_spec := N.pos_pred_spec (only parsing).
Notation Ppred_Nsucc := N.pos_pred_succ (only parsing).
Notation Nplus_0_l := N.add_0_l (only parsing).
Notation Nplus_0_r := N.add_0_r (only parsing).
Notation Nplus_comm := N.add_comm (only parsing).
Notation Nplus_assoc := N.add_assoc (only parsing).
Notation Nplus_succ := N.add_succ_l (only parsing).
Notation Nsucc_0 := N.succ_0_discr (only parsing).
Notation Nminus_N0_Nle := N.sub_0_le (only parsing).
Notation Nminus_0_r := N.sub_0_r (only parsing).
Notation Nminus_succ_r:= N.sub_succ_r (only parsing).
Notation Nmult_0_l := N.mul_0_l (only parsing).
Notation Nmult_1_l := N.mul_1_l (only parsing).
Notation Nmult_1_r := N.mul_1_r (only parsing).
Notation Nmult_comm := N.mul_comm (only parsing).
Notation Nmult_assoc := N.mul_assoc (only parsing).
Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing).
Notation Nle_0 := N.le_0_l (only parsing).
Notation Ncompare_Eq_eq := N.compare_eq (only parsing).
Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing).
Notation Nle_lteq := N.lt_eq_cases (only parsing).
Notation Ncompare_0 := N.compare_0_r (only parsing).
Notation Ndouble_div2 := N.div2_double (only parsing).
Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing).
Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing).
Notation Nlt_not_eq := N.lt_neq (only parsing).
Notation Ngt_Nlt := N.gt_lt (only parsing).

More complex compatibility facts, expressed as lemmas (to preserve scopes for instance)

Lemma Nplus_reg_l n m p : n + m = n + p -> m = p.n, m, p:N
n + m = n + p -> m = p
Proof (proj1 (N.add_cancel_l m p n)).
Lemma Nmult_Sn_m n m : N.succ n * m = m + n * m.n, m:N
N.succ n * m = m + n * m
Proof (eq_trans (N.mul_succ_l n m) (N.add_comm _ _)).
Lemma Nmult_plus_distr_l n m p : p * (n + m) = p * n + p * m.n, m, p:N
p * (n + m) = p * n + p * m
Proof (N.mul_add_distr_l p n m).
Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.n, m, p:N
p <> 0 -> n * p = m * p -> n = m
Proof (fun H => proj1 (N.mul_cancel_r n m p H)).
Lemma Ncompare_antisym n m : CompOpp (n ?= m) = (m ?= n).n, m:N
CompOpp (n ?= m) = (m ?= n)
Proof (eq_sym (N.compare_antisym n m)).

Definition N_ind_double a P f0 f2 fS2 := N.binary_ind P f0 f2 fS2 a.
Definition N_rec_double a P f0 f2 fS2 := N.binary_rec P f0 f2 fS2 a.

Not kept : Ncompare_n_Sm Nplus_lt_cancel_l