PeanoNat.v

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)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Import NAxioms NProperties OrdersFacts.

Implementation of NAxiomsSig by nat

Module Nat
 <: NAxiomsSig
 <: UsualDecidableTypeFull
 <: OrderedTypeFull
 <: TotalOrder.

Operations over nat are defined in a separate module

Include Coq.Init.Nat.

When including property functors, inline t eq zero one two lt le succ

Set Inline Level 50.

All operations are well-defined (trivial here since eq is Leibniz)

Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Instance succ_wd : Proper (eq==>eq) S.
Instance pred_wd : Proper (eq==>eq) pred.
Instance add_wd : Proper (eq==>eq==>eq) plus.
Instance sub_wd : Proper (eq==>eq==>eq) minus.
Instance mul_wd : Proper (eq==>eq==>eq) mult.
Instance pow_wd : Proper (eq==>eq==>eq) pow.
Instance div_wd : Proper (eq==>eq==>eq) div.
Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Instance lt_wd : Proper (eq==>eq==>iff) lt.
Instance testbit_wd : Proper (eq==>eq==>eq) testbit.

Bi-directional induction.

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

Recursion function

Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A :=
  nat_rect (fun _ => A).

Instance recursion_wd {A} (Aeq : relation A) :
 Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.A:Type
Aeq:relation A
Proper (Aeq ==> (eq ==> Aeq ==> Aeq) ==> eq ==> Aeq)
  recursion
Proof.A:Type
Aeq:relation A
Proper (Aeq ==> (eq ==> Aeq ==> Aeq) ==> eq ==> Aeq)
  recursion
intros a a' Ha f f' Hf n n' Hn.A:Type
Aeq:relation A
a, a':A
Ha:Aeq a a'
f, f':nat -> A -> A
Hf:(eq ==> Aeq ==> Aeq)%signature f f'
n, n':nat
Hn:n = n'
Aeq (recursion a f n) (recursion a' f' n') subst n'.A:Type
Aeq:relation A
a, a':A
Ha:Aeq a a'
f, f':nat -> A -> A
Hf:(eq ==> Aeq ==> Aeq)%signature f f'
n:nat
Aeq (recursion a f n) (recursion a' f' n)
induction n; simpl; auto.A:Type
Aeq:relation A
a, a':A
Ha:Aeq a a'
f, f':nat -> A -> A
Hf:(eq ==> Aeq ==> Aeq)%signature f f'
n:nat
IHn:Aeq (recursion a f n) (recursion a' f' n)
Aeq (f n (recursion a f n)) (f' n (recursion a' f' n)) apply Hf; auto.
Qed.

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

Theorem recursion_succ :
  forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A),
    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
      forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).forall (A : Type) (Aeq : relation A) (a : A)
  (f : nat -> A -> A),
Aeq a a ->
Proper (eq ==> Aeq ==> Aeq) f ->
forall n : nat,
Aeq (recursion a f (S n)) (f n (recursion a f n))
Proof.forall (A : Type) (Aeq : relation A) (a : A)
  (f : nat -> A -> A),
Aeq a a ->
Proper (eq ==> Aeq ==> Aeq) f ->
forall n : nat,
Aeq (recursion a f (S n)) (f n (recursion a f n))
unfold Proper, respectful in *; induction n; simpl; auto.
Qed.

Remaining constants not defined in Coq.Init.Nat

NB: Aliasing le is mandatory, since only a Definition can implement an interface Parameter...

Definition eq := @Logic.eq nat.
Definition le := Peano.le.
Definition lt := Peano.lt.

Basic specifications : pred add sub mul

Lemma pred_succ n : pred (S n) = n.n:nat
pred (S n) = n
Proof.n:nat
pred (S n) = n
reflexivity.
Qed.

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

Lemma one_succ : 1 = S 0.1 = 1
Proof.1 = 1
reflexivity.
Qed.

Lemma two_succ : 2 = S 1.2 = 2
Proof.2 = 2
reflexivity.
Qed.

Lemma add_0_l n : 0 + n = n.n:nat
0 + n = n
Proof.n:nat
0 + n = n
reflexivity.
Qed.

Lemma add_succ_l n m : (S n) + m = S (n + m).n, m:nat
S n + m = S (n + m)
Proof.n, m:nat
S n + m = S (n + m)
reflexivity.
Qed.

Lemma sub_0_r n : n - 0 = n.n:nat
n - 0 = n
Proof.n:nat
n - 0 = n
now destruct n.
Qed.

Lemma sub_succ_r n m : n - (S m) = pred (n - m).n, m:nat
n - S m = pred (n - m)
Proof.n, m:nat
n - S m = pred (n - m)
revert m.n:nat
forall m : nat, n - S m = pred (n - m) induction n; destruct m; simpl; auto.n:nat
IHn:forall m : nat, n - S m = pred (n - m)
n - 0 = n apply sub_0_r.
Qed.

Lemma mul_0_l n : 0 * n = 0.n:nat
0 * n = 0
Proof.n:nat
0 * n = 0
reflexivity.
Qed.

Lemma mul_succ_l n m : S n * m = n * m + m.n, m:nat
S n * m = n * m + m
Proof.n, m:nat
S n * m = n * m + m
assert (succ_r : forall x y, x+S y = S(x+y)) by now induction x.n, m:nat
succ_r:forall x y : nat, x + S y = S (x + y)
S n * m = n * m + m
assert (comm : forall x y, x+y = y+x).n, m:nat
succ_r:forall x y : nat, x + S y = S (x + y)
forall x y : nat, x + y = y + x
n, m:nat
succ_r:forall x y : nat, x + S y = S (x + y)
comm:forall x y : nat, x + y = y + x
S n * m = n * m + m
{n, m:nat
succ_r:forall x y : nat, x + S y = S (x + y)
forall x y : nat, x + y = y + x induction x; simpl; auto.n, m:nat
succ_r:forall x0 y : nat, x0 + S y = S (x0 + y)
x:nat
IHx:forall y : nat, x + y = y + x
forall y : nat, S (x + y) = y + S x intros; rewrite succ_r; now f_equal. }n, m:nat
succ_r:forall x y : nat, x + S y = S (x + y)
comm:forall x y : nat, x + y = y + x
S n * m = n * m + m
now rewrite comm.
Qed.

Lemma lt_succ_r n m : n < S m <-> n <= m.n, m:nat
n < S m <-> n <= m
Proof.n, m:nat
n < S m <-> n <= m
split.n, m:nat
n < S m -> n <= m
n, m:nat
n <= m -> n < S m apply Peano.le_S_n.n, m:nat
n <= m -> n < S m induction 1; auto.
Qed.

Boolean comparisons

Lemma eqb_eq n m : eqb n m = true <-> n = m.n, m:nat
(n =? m) = true <-> n = m
Proof.n, m:nat
(n =? m) = true <-> n = m
 revert m.n:nat
forall m : nat, (n =? m) = true <-> n = m
 induction n; destruct m; simpl; rewrite ?IHn; split; try easy.n:nat
IHn:forall m0 : nat, (n =? m0) = true <-> n = m0
m:nat
n = m -> S n = S m
n:nat
IHn:forall m0 : nat, (n =? m0) = true <-> n = m0
m:nat
S n = S m -> n = m
 -n:nat
IHn:forall m0 : nat, (n =? m0) = true <-> n = m0
m:nat
n = m -> S n = S m now intros ->.
 -n:nat
IHn:forall m0 : nat, (n =? m0) = true <-> n = m0
m:nat
S n = S m -> n = m now injection 1.
Qed.

Lemma leb_le n m : (n <=? m) = true <-> n <= m.n, m:nat
(n <=? m) = true <-> n <= m
Proof.n, m:nat
(n <=? m) = true <-> n <= m
 revert m.n:nat
forall m : nat, (n <=? m) = true <-> n <= m
 induction n; destruct m; simpl.true = true <-> 0 <= 0
m:nat
true = true <-> 0 <= S m
n:nat
IHn:forall m : nat, (n <=? m) = true <-> n <= m
false = true <-> S n <= 0
n:nat
IHn:forall m0 : nat, (n <=? m0) = true <-> n <= m0
m:nat
(n <=? m) = true <-> S n <= S m
 -true = true <-> 0 <= 0 now split.
 -m:nat
true = true <-> 0 <= S m split; trivial.m:nat
true = true -> 0 <= S m intros; apply Peano.le_0_n.
 -n:nat
IHn:forall m : nat, (n <=? m) = true <-> n <= m
false = true <-> S n <= 0 now split.
 -n:nat
IHn:forall m0 : nat, (n <=? m0) = true <-> n <= m0
m:nat
(n <=? m) = true <-> S n <= S m rewrite IHn; split.n:nat
IHn:forall m0 : nat, (n <=? m0) = true <-> n <= m0
m:nat
n <= m -> S n <= S m
n:nat
IHn:forall m0 : nat, (n <=? m0) = true <-> n <= m0
m:nat
S n <= S m -> n <= m
   +n:nat
IHn:forall m0 : nat, (n <=? m0) = true <-> n <= m0
m:nat
n <= m -> S n <= S m apply Peano.le_n_S.
   +n:nat
IHn:forall m0 : nat, (n <=? m0) = true <-> n <= m0
m:nat
S n <= S m -> n <= m apply Peano.le_S_n.
Qed.

Lemma ltb_lt n m : (n <? m) = true <-> n < m.n, m:nat
(n <? m) = true <-> n < m
Proof.n, m:nat
(n <? m) = true <-> n < m
 apply leb_le.
Qed.

Decidability of equality over nat.

Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.forall n m : nat, {n = m} + {n <> m}
Proof.forall n m : nat, {n = m} + {n <> m}
  induction n; destruct m.{0 = 0} + {0 <> 0}
m:nat
{0 = S m} + {0 <> S m}
n:nat
IHn:forall m : nat, {n = m} + {n <> m}
{S n = 0} + {S n <> 0}
n:nat
IHn:forall m0 : nat, {n = m0} + {n <> m0}
m:nat
{S n = S m} + {S n <> S m}
  -{0 = 0} + {0 <> 0} now left.
  -m:nat
{0 = S m} + {0 <> S m} now right.
  -n:nat
IHn:forall m : nat, {n = m} + {n <> m}
{S n = 0} + {S n <> 0} now right.
  -n:nat
IHn:forall m0 : nat, {n = m0} + {n <> m0}
m:nat
{S n = S m} + {S n <> S m} destruct (IHn m); [left|right]; auto.
Defined.

Ternary comparison

With nat, it would be easier to prove first compare_spec, then the properties below. But then we wouldn't be able to benefit from functor BoolOrderFacts

Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.n, m:nat
(n ?= m) = Eq <-> n = m
Proof.n, m:nat
(n ?= m) = Eq <-> n = m
 revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy.
Qed.

Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.n, m:nat
(n ?= m) = Lt <-> n < m
Proof.n, m:nat
(n ?= m) = Lt <-> n < m
 revert m; induction n; destruct m; simpl; rewrite ?IHn; split; try easy.m:nat
Lt = Lt -> 0 < S m
n:nat
IHn:forall m0 : nat, (n ?= m0) = Lt <-> n < m0
m:nat
n < m -> S n < S m
n:nat
IHn:forall m0 : nat, (n ?= m0) = Lt <-> n < m0
m:nat
S n < S m -> n < m
 -m:nat
Lt = Lt -> 0 < S m intros _.m:nat
0 < S m apply Peano.le_n_S, Peano.le_0_n.
 -n:nat
IHn:forall m0 : nat, (n ?= m0) = Lt <-> n < m0
m:nat
n < m -> S n < S m apply Peano.le_n_S.
 -n:nat
IHn:forall m0 : nat, (n ?= m0) = Lt <-> n < m0
m:nat
S n < S m -> n < m apply Peano.le_S_n.
Qed.

Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.n, m:nat
(n ?= m) <> Gt <-> n <= m
Proof.n, m:nat
(n ?= m) <> Gt <-> n <= m
 revert m; induction n; destruct m; simpl; rewrite ?IHn.Eq <> Gt <-> 0 <= 0
m:nat
Lt <> Gt <-> 0 <= S m
n:nat
IHn:forall m : nat, (n ?= m) <> Gt <-> n <= m
Gt <> Gt <-> S n <= 0
n:nat
IHn:forall m0 : nat, (n ?= m0) <> Gt <-> n <= m0
m:nat
n <= m <-> S n <= S m
 -Eq <> Gt <-> 0 <= 0 now split.
 -m:nat
Lt <> Gt <-> 0 <= S m split; intros.m:nat
H:Lt <> Gt
0 <= S m
m:nat
H:0 <= S m
Lt <> Gt apply Peano.le_0_n.m:nat
H:0 <= S m
Lt <> Gt easy.
 -n:nat
IHn:forall m : nat, (n ?= m) <> Gt <-> n <= m
Gt <> Gt <-> S n <= 0 split.n:nat
IHn:forall m : nat, (n ?= m) <> Gt <-> n <= m
Gt <> Gt -> S n <= 0
n:nat
IHn:forall m : nat, (n ?= m) <> Gt <-> n <= m
S n <= 0 -> Gt <> Gt now destruct 1.n:nat
IHn:forall m : nat, (n ?= m) <> Gt <-> n <= m
S n <= 0 -> Gt <> Gt inversion 1.
 -n:nat
IHn:forall m0 : nat, (n ?= m0) <> Gt <-> n <= m0
m:nat
n <= m <-> S n <= S m split; intros.n:nat
IHn:forall m0 : nat, (n ?= m0) <> Gt <-> n <= m0
m:nat
H:n <= m
S n <= S m
n:nat
IHn:forall m0 : nat, (n ?= m0) <> Gt <-> n <= m0
m:nat
H:S n <= S m
n <= m now apply Peano.le_n_S.n:nat
IHn:forall m0 : nat, (n ?= m0) <> Gt <-> n <= m0
m:nat
H:S n <= S m
n <= m now apply Peano.le_S_n.
Qed.

Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).n, m:nat
(m ?= n) = CompOpp (n ?= m)
Proof.n, m:nat
(m ?= n) = CompOpp (n ?= m)
 revert m; induction n; destruct m; simpl; trivial.
Qed.

Lemma compare_succ n m : (S n ?= S m) = (n ?= m).n, m:nat
(S n ?= S m) = (n ?= m)
Proof.n, m:nat
(S n ?= S m) = (n ?= m)
 reflexivity.
Qed.


(* BUG: Ajout d'un cas * après preuve finie (deuxième niveau +++*** ) :
    *  --->   Anomaly: Uncaught exception Proofview.IndexOutOfRange(_). Please report. *)

Minimum, maximum

Lemma max_l : forall n m, m <= n -> max n m = n.forall n m : nat, m <= n -> max n m = n
Proof.forall n m : nat, m <= n -> max n m = n
 exact Peano.max_l.
Qed.

Lemma max_r : forall n m, n <= m -> max n m = m.forall n m : nat, n <= m -> max n m = m
Proof.forall n m : nat, n <= m -> max n m = m
 exact Peano.max_r.
Qed.

Lemma min_l : forall n m, n <= m -> min n m = n.forall n m : nat, n <= m -> min n m = n
Proof.forall n m : nat, n <= m -> min n m = n
 exact Peano.min_l.
Qed.

Lemma min_r : forall n m, m <= n -> min n m = m.forall n m : nat, m <= n -> min n m = m
Proof.forall n m : nat, m <= n -> min n m = m
 exact Peano.min_r.
Qed.

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

Include BoolOrderFacts.

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.

Power

Lemma pow_neg_r a b : b<0 -> a^b = 0.a, b:nat
b < 0 -> a ^ b = 0 inversion 1. Qed.

Lemma pow_0_r a : a^0 = 1.a:nat
a ^ 0 = 1
Proof.a:nat
a ^ 0 = 1 reflexivity. Qed.

Lemma pow_succ_r a b : 0<=b -> a^(S b) = a * a^b.a, b:nat
0 <= b -> a ^ S b = a * a ^ b
Proof.a, b:nat
0 <= b -> a ^ S b = a * a ^ b reflexivity. Qed.

Square

Lemma square_spec n : square n = n * n.n:nat
square n = n * n
Proof.n:nat
square n = n * n reflexivity. Qed.

Parity

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

Module Private_Parity.

Lemma Even_1 : ~ Even 1.~ Even 1
Proof.~ Even 1
 intros ([|], H); try discriminate.n:nat
H:1 = 2 * S n
False
 simpl in H.n:nat
H:1 = S (n + S (n + 0))
False now rewrite <- plus_n_Sm in H.
Qed.

Lemma Even_2 n : Even n <-> Even (S (S n)).n:nat
Even n <-> Even (S (S n))
Proof.n:nat
Even n <-> Even (S (S n))
 split; intros (m,H).n, m:nat
H:n = 2 * m
Even (S (S n))
n, m:nat
H:S (S n) = 2 * m
Even n
 -n, m:nat
H:n = 2 * m
Even (S (S n)) exists (S m).n, m:nat
H:n = 2 * m
S (S n) = 2 * S m rewrite H.n, m:nat
H:n = 2 * m
S (S (2 * m)) = 2 * S m simpl.n, m:nat
H:n = 2 * m
S (S (m + (m + 0))) = S (m + S (m + 0)) now rewrite plus_n_Sm.
 -n, m:nat
H:S (S n) = 2 * m
Even n destruct m; try discriminate.n, m:nat
H:S (S n) = 2 * S m
Even n
   exists m.n, m:nat
H:S (S n) = 2 * S m
n = 2 * m simpl in H.n, m:nat
H:S (S n) = S (m + S (m + 0))
n = 2 * m rewrite <- plus_n_Sm in H.n, m:nat
H:S (S n) = S (S (m + (m + 0)))
n = 2 * m now inversion H.
Qed.

Lemma Odd_0 : ~ Odd 0.~ Odd 0
Proof.~ Odd 0
 now intros ([|], H).
Qed.

Lemma Odd_2 n : Odd n <-> Odd (S (S n)).n:nat
Odd n <-> Odd (S (S n))
Proof.n:nat
Odd n <-> Odd (S (S n))
 split; intros (m,H).n, m:nat
H:n = 2 * m + 1
Odd (S (S n))
n, m:nat
H:S (S n) = 2 * m + 1
Odd n
 -n, m:nat
H:n = 2 * m + 1
Odd (S (S n)) exists (S m).n, m:nat
H:n = 2 * m + 1
S (S n) = 2 * S m + 1 rewrite H.n, m:nat
H:n = 2 * m + 1
S (S (2 * m + 1)) = 2 * S m + 1 simpl.n, m:nat
H:n = 2 * m + 1
S (S (m + (m + 0) + 1)) = S (m + S (m + 0) + 1) now rewrite <- (plus_n_Sm m).
 -n, m:nat
H:S (S n) = 2 * m + 1
Odd n destruct m; try discriminate.n, m:nat
H:S (S n) = 2 * S m + 1
Odd n
   exists m.n, m:nat
H:S (S n) = 2 * S m + 1
n = 2 * m + 1 simpl in H.n, m:nat
H:S (S n) = S (m + S (m + 0) + 1)
n = 2 * m + 1 rewrite <- plus_n_Sm in H.n, m:nat
H:S (S n) = S (S (m + S (m + 0) + 0))
n = 2 * m + 1 inversion H.n, m:nat
H:S (S n) = S (S (m + S (m + 0) + 0))
H1:n = m + S (m + 0) + 0
m + S (m + 0) + 0 = 2 * m + 1
   simpl.n, m:nat
H:S (S n) = S (S (m + S (m + 0) + 0))
H1:n = m + S (m + 0) + 0
m + S (m + 0) + 0 = m + (m + 0) + 1 now rewrite <- !plus_n_Sm, <- !plus_n_O.
Qed.

End Private_Parity.
Import Private_Parity.

Lemma even_spec : forall n, even n = true <-> Even n.forall n : nat, even n = true <-> Even n
Proof.forall n : nat, even n = true <-> Even n
 fix even_spec 1.even_spec:forall n : nat, even n = true <-> Even n
forall n : nat, even n = true <-> Even n
  destruct n as [|[|n]]; simpl.even_spec:forall n : nat, even n = true <-> Even n
true = true <-> Even 0
even_spec:forall n : nat, even n = true <-> Even n
false = true <-> Even 1
even_spec:forall n0 : nat,
even n0 = true <-> Even n0
n:nat
even n = true <-> Even (S (S n))
  -even_spec:forall n : nat, even n = true <-> Even n
true = true <-> Even 0 split; [ now exists 0 | trivial ].
  -even_spec:forall n : nat, even n = true <-> Even n
false = true <-> Even 1 split; [ discriminate | intro H; elim (Even_1 H) ].
  -even_spec:forall n0 : nat,
even n0 = true <-> Even n0
n:nat
even n = true <-> Even (S (S n)) rewrite even_spec.even_spec:forall n0 : nat,
even n0 = true <-> Even n0
n:nat
Even n <-> Even (S (S n)) apply Even_2.
Qed.

Lemma odd_spec : forall n, odd n = true <-> Odd n.forall n : nat, odd n = true <-> Odd n
Proof.forall n : nat, odd n = true <-> Odd n
 unfold odd.forall n : nat, negb (even n) = true <-> Odd n
 fix odd_spec 1.odd_spec:forall n : nat,
negb (even n) = true <-> Odd n
forall n : nat, negb (even n) = true <-> Odd n
  destruct n as [|[|n]]; simpl.odd_spec:forall n : nat,
negb (even n) = true <-> Odd n
false = true <-> Odd 0
odd_spec:forall n : nat,
negb (even n) = true <-> Odd n
true = true <-> Odd 1
odd_spec:forall n0 : nat,
negb (even n0) = true <-> Odd n0
n:nat
negb (even n) = true <-> Odd (S (S n))
  -odd_spec:forall n : nat,
negb (even n) = true <-> Odd n
false = true <-> Odd 0 split; [ discriminate | intro H; elim (Odd_0 H) ].
  -odd_spec:forall n : nat,
negb (even n) = true <-> Odd n
true = true <-> Odd 1 split; [ now exists 0 | trivial ].
  -odd_spec:forall n0 : nat,
negb (even n0) = true <-> Odd n0
n:nat
negb (even n) = true <-> Odd (S (S n)) rewrite odd_spec.odd_spec:forall n0 : nat,
negb (even n0) = true <-> Odd n0
n:nat
Odd n <-> Odd (S (S n)) apply Odd_2.
Qed.

Division

Lemma divmod_spec : forall x y q u, u <= y ->
 let (q',u') := divmod x y q u in
 x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.forall x y q u : nat,
u <= y ->
let (q', u') := divmod x y q u in
x + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y
Proof.forall x y q u : nat,
u <= y ->
let (q', u') := divmod x y q u in
x + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y
 induction x.forall y q u : nat,
u <= y ->
let (q', u') := divmod 0 y q u in
0 + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y
x:nat
IHx:forall y q u : nat,
u <= y ->
let (q', u') := divmod x y q u in
x + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y
forall y q u : nat,
u <= y ->
let (q', u') := divmod (S x) y q u in
S x + S y * q + (y - u) = S y * q' + (y - u') /\
u' <= y
 -forall y q u : nat,
u <= y ->
let (q', u') := divmod 0 y q u in
0 + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y simpl; intuition.
 -x:nat
IHx:forall y q u : nat,
u <= y ->
let (q', u') := divmod x y q u in
x + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y
forall y q u : nat,
u <= y ->
let (q', u') := divmod (S x) y q u in
S x + S y * q + (y - u) = S y * q' + (y - u') /\
u' <= y intros y q u H.x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:u <= y
let (q', u') := divmod (S x) y q u in
S x + S y * q + (y - u) = S y * q' + (y - u') /\
u' <= y destruct u; simpl divmod.x:nat
IHx:forall y0 q0 u : nat,
u <= y0 ->
let (q', u') := divmod x y0 q0 u in
x + S y0 * q0 + (y0 - u) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q:nat
H:0 <= y
let (q', u') := divmod x y (S q) y in
S x + S y * q + (y - 0) = S y * q' + (y - u') /\
u' <= y
x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
let (q', u') := divmod x y q u in
S x + S y * q + (y - S u) = S y * q' + (y - u') /\
u' <= y
   +x:nat
IHx:forall y0 q0 u : nat,
u <= y0 ->
let (q', u') := divmod x y0 q0 u in
x + S y0 * q0 + (y0 - u) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q:nat
H:0 <= y
let (q', u') := divmod x y (S q) y in
S x + S y * q + (y - 0) = S y * q' + (y - u') /\
u' <= y generalize (IHx y (S q) y (le_n y)).x:nat
IHx:forall y0 q0 u : nat,
u <= y0 ->
let (q', u') := divmod x y0 q0 u in
x + S y0 * q0 + (y0 - u) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q:nat
H:0 <= y
(let (q', u') := divmod x y (S q) y in
 x + S y * S q + (y - y) = S y * q' + (y - u') /\
 u' <= y) ->
let (q', u') := divmod x y (S q) y in
S x + S y * q + (y - 0) = S y * q' + (y - u') /\
u' <= y destruct divmod as (q',u').x:nat
IHx:forall y0 q0 u : nat,
u <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u in
x + S y0 * q0 + (y0 - u) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q:nat
H:0 <= y
q', u':nat
x + S y * S q + (y - y) = S y * q' + (y - u') /\
u' <= y ->
S x + S y * q + (y - 0) = S y * q' + (y - u') /\
u' <= y
     intros (EQ,LE); split; trivial.x:nat
IHx:forall y0 q0 u : nat,
u <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u in
x + S y0 * q0 + (y0 - u) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q:nat
H:0 <= y
q', u':nat
EQ:x + S y * S q + (y - y) = S y * q' + (y - u')
LE:u' <= y
S x + S y * q + (y - 0) = S y * q' + (y - u')
     rewrite <- EQ, sub_0_r, sub_diag, add_0_r.x:nat
IHx:forall y0 q0 u : nat,
u <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u in
x + S y0 * q0 + (y0 - u) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q:nat
H:0 <= y
q', u':nat
EQ:x + S y * S q + (y - y) = S y * q' + (y - u')
LE:u' <= y
S x + S y * q + y = x + S y * S q
     now rewrite !add_succ_l, <- add_succ_r, <- add_assoc, mul_succ_r.
   +x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
let (q', u') := divmod x y q u in
S x + S y * q + (y - S u) = S y * q' + (y - u') /\
u' <= y assert (H' : u <= y).x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
u <= y
x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
H':u <= y
let (q', u') := divmod x y q u in
S x + S y * q + (y - S u) = S y * q' + (y - u') /\
u' <= y
     {x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
u <= y apply le_trans with (S u); trivial.x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
u <= S u do 2 constructor. }x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
H':u <= y
let (q', u') := divmod x y q u in
S x + S y * q + (y - S u) = S y * q' + (y - u') /\
u' <= y
     generalize (IHx y q u H').x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q', u') := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q' + (y0 - u') /\ u' <= y0
y, q, u:nat
H:S u <= y
H':u <= y
(let (q', u') := divmod x y q u in
 x + S y * q + (y - u) = S y * q' + (y - u') /\
 u' <= y) ->
let (q', u') := divmod x y q u in
S x + S y * q + (y - S u) = S y * q' + (y - u') /\
u' <= y destruct divmod as (q',u').x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q, u:nat
H:S u <= y
H':u <= y
q', u':nat
x + S y * q + (y - u) = S y * q' + (y - u') /\ u' <= y ->
S x + S y * q + (y - S u) = S y * q' + (y - u') /\
u' <= y
     intros (EQ,LE); split; trivial.x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q, u:nat
H:S u <= y
H':u <= y
q', u':nat
EQ:x + S y * q + (y - u) = S y * q' + (y - u')
LE:u' <= y
S x + S y * q + (y - S u) = S y * q' + (y - u')
     rewrite <- EQ.x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q, u:nat
H:S u <= y
H':u <= y
q', u':nat
EQ:x + S y * q + (y - u) = S y * q' + (y - u')
LE:u' <= y
S x + S y * q + (y - S u) = x + S y * q + (y - u)
     rewrite !add_succ_l, <- add_succ_r.x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q, u:nat
H:S u <= y
H':u <= y
q', u':nat
EQ:x + S y * q + (y - u) = S y * q' + (y - u')
LE:u' <= y
x + S y * q + S (y - S u) = x + S y * q + (y - u) f_equal.x:nat
IHx:forall y0 q0 u0 : nat,
u0 <= y0 ->
let (q'0, u'0) := divmod x y0 q0 u0 in
x + S y0 * q0 + (y0 - u0) = S y0 * q'0 + (y0 - u'0) /\ u'0 <= y0
y, q, u:nat
H:S u <= y
H':u <= y
q', u':nat
EQ:x + S y * q + (y - u) = S y * q' + (y - u')
LE:u' <= y
S (y - S u) = y - u now rewrite <- sub_succ_l.
Qed.

Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y.x, y:nat
y <> 0 -> x = y * (x / y) + x mod y
Proof.x, y:nat
y <> 0 -> x = y * (x / y) + x mod y
 intros Hy.x, y:nat
Hy:y <> 0
x = y * (x / y) + x mod y
 destruct y; [ now elim Hy | clear Hy ].x, y:nat
x = S y * (x / S y) + x mod S y
 unfold div, modulo.x, y:nat
x =
S y * fst (divmod x y 0 y) +
(y - snd (divmod x y 0 y))
 generalize (divmod_spec x y 0 y (le_n y)).x, y:nat
(let (q', u') := divmod x y 0 y in
 x + S y * 0 + (y - y) = S y * q' + (y - u') /\
 u' <= y) ->
x =
S y * fst (divmod x y 0 y) +
(y - snd (divmod x y 0 y))
 destruct divmod as (q,u).x, y, q, u:nat
x + S y * 0 + (y - y) = S y * q + (y - u) /\ u <= y ->
x = S y * fst (q, u) + (y - snd (q, u))
 intros (U,V).x, y, q, u:nat
U:x + S y * 0 + (y - y) = S y * q + (y - u)
V:u <= y
x = S y * fst (q, u) + (y - snd (q, u))
 simpl in *.x, y, q, u:nat
U:x + y * 0 + (y - y) = q + y * q + (y - u)
V:u <= y
x = q + y * q + (y - u)
 now rewrite mul_0_r, sub_diag, !add_0_r in U.
Qed.

Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y.x, y:nat
0 <= x -> 0 < y -> 0 <= x mod y < y
Proof.x, y:nat
0 <= x -> 0 < y -> 0 <= x mod y < y
 intros Hx Hy.x, y:nat
Hx:0 <= x
Hy:0 < y
0 <= x mod y < y split.x, y:nat
Hx:0 <= x
Hy:0 < y
0 <= x mod y
x, y:nat
Hx:0 <= x
Hy:0 < y
x mod y < y apply le_0_l.x, y:nat
Hx:0 <= x
Hy:0 < y
x mod y < y
 destruct y; [ now elim Hy | clear Hy ].x, y:nat
Hx:0 <= x
x mod S y < S y
 unfold modulo.x, y:nat
Hx:0 <= x
y - snd (divmod x y 0 y) < S y
 apply lt_succ_r, le_sub_l.
Qed.

Square root

Lemma sqrt_iter_spec : forall k p q r,
 q = p+p -> r<=q ->
 let s := sqrt_iter k p q r in
 s*s <= k + p*p + (q - r) < (S s)*(S s).forall k p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter k p q r in
s * s <= k + p * p + (q - r) < S s * S s
Proof.forall k p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter k p q r in
s * s <= k + p * p + (q - r) < S s * S s
 induction k.forall p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter 0 p q r in
s * s <= 0 + p * p + (q - r) < S s * S s
k:nat
IHk:forall p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter k p q r in s * s <= k + p * p + (q - r) < S s * S s
forall p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter (S k) p q r in
s * s <= S k + p * p + (q - r) < S s * S s
 - (* k = 0 *)forall p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter 0 p q r in
s * s <= 0 + p * p + (q - r) < S s * S s
   simpl; intros p q r Hq Hr.p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p <= p * p + (q - r) < S (p + p * S p)
   split.p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p <= p * p + (q - r)
p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p + (q - r) < S (p + p * S p)
   +p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p <= p * p + (q - r) apply le_add_r.
   +p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p + (q - r) < S (p + p * S p) apply lt_succ_r.p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p + (q - r) <= p + p * S p
     rewrite mul_succ_r.p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p + (q - r) <= p + (p * p + p)
     rewrite add_assoc, (add_comm p), <- add_assoc.p, q, r:nat
Hq:q = p + p
Hr:r <= q
p * p + (q - r) <= p * p + (p + p)
     apply add_le_mono_l.p, q, r:nat
Hq:q = p + p
Hr:r <= q
q - r <= p + p
     rewrite <- Hq.p, q, r:nat
Hq:q = p + p
Hr:r <= q
q - r <= q apply le_sub_l.
 - (* k = S k' *)k:nat
IHk:forall p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter k p q r in s * s <= k + p * p + (q - r) < S s * S s
forall p q r : nat,
q = p + p ->
r <= q ->
let s := sqrt_iter (S k) p q r in
s * s <= S k + p * p + (q - r) < S s * S s
   destruct r.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
q = p + p ->
0 <= q ->
let s := sqrt_iter (S k) p q 0 in
s * s <= S k + p * p + (q - 0) < S s * S s
k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
q = p + p ->
S r <= q ->
let s := sqrt_iter (S k) p q (S r) in
s * s <= S k + p * p + (q - S r) < S s * S s
   + (* r = 0 *)k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
q = p + p ->
0 <= q ->
let s := sqrt_iter (S k) p q 0 in
s * s <= S k + p * p + (q - 0) < S s * S s
     intros Hq _.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
let s := sqrt_iter (S k) p q 0 in
s * s <= S k + p * p + (q - 0) < S s * S s
     replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))).k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
let s := sqrt_iter (S k) p q 0 in
s * s <= k + S p * S p + (S (S q) - S (S q)) <
S s * S s
k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
k + S p * S p + (S (S q) - S (S q)) =
S k + p * p + (q - 0)
     *k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
let s := sqrt_iter (S k) p q 0 in
s * s <= k + S p * S p + (S (S q) - S (S q)) <
S s * S s apply IHk.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
S (S q) = S p + S p
k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
S (S q) <= S (S q)
       simpl.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
S (S q) = S (p + S p)
k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
S (S q) <= S (S q) now rewrite add_succ_r, Hq.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
S (S q) <= S (S q) apply le_n.
     *k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
k + S p * S p + (S (S q) - S (S q)) =
S k + p * p + (q - 0) rewrite sub_diag, sub_0_r, add_0_r.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
k + S p * S p = S k + p * p + q simpl.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
k + S (p + p * S p) = S (k + p * p + q)
       rewrite add_succ_r; f_equal.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
k + (p + p * S p) = k + p * p + q rewrite <- add_assoc; f_equal.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
p + p * S p = p * p + q
       rewrite mul_succ_r, (add_comm p), <- add_assoc.k:nat
IHk:forall p0 q0 r : nat,
q0 = p0 + p0 ->
r <= q0 ->
let s := sqrt_iter k p0 q0 r in s * s <= k + p0 * p0 + (q0 - r) < S s * S s
p, q:nat
Hq:q = p + p
p * p + (p + p) = p * p + q now f_equal.
   + (* r = S r' *)k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
q = p + p ->
S r <= q ->
let s := sqrt_iter (S k) p q (S r) in
s * s <= S k + p * p + (q - S r) < S s * S s
     intros Hq Hr.k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
let s := sqrt_iter (S k) p q (S r) in
s * s <= S k + p * p + (q - S r) < S s * S s
     replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)).k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
let s := sqrt_iter (S k) p q (S r) in
s * s <= k + p * p + (q - r) < S s * S s
k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
k + p * p + (q - r) = S k + p * p + (q - S r)
     *k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
let s := sqrt_iter (S k) p q (S r) in
s * s <= k + p * p + (q - r) < S s * S s apply IHk; trivial.k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
r <= q apply le_trans with (S r); trivial.k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
r <= S r do 2 constructor.
     *k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
k + p * p + (q - r) = S k + p * p + (q - S r) simpl.k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
k + p * p + (q - r) = S (k + p * p + (q - S r)) rewrite <- add_succ_r.k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
k + p * p + (q - r) = k + p * p + S (q - S r) f_equal.k:nat
IHk:forall p0 q0 r0 : nat,
q0 = p0 + p0 ->
r0 <= q0 ->
let s := sqrt_iter k p0 q0 r0 in s * s <= k + p0 * p0 + (q0 - r0) < S s * S s
p, q, r:nat
Hq:q = p + p
Hr:S r <= q
q - r = S (q - S r) rewrite <- sub_succ_l; trivial.
Qed.

Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).n:nat
sqrt n * sqrt n <= n < S (sqrt n) * S (sqrt n)
Proof.n:nat
sqrt n * sqrt n <= n < S (sqrt n) * S (sqrt n)
 set (s:=sqrt n).n:nat
s:=sqrt n:nat
s * s <= n < S s * S s
 replace n with (n + 0*0 + (0-0)).n:nat
s:=sqrt n:nat
s * s <= n + 0 * 0 + (0 - 0) < S s * S s
n:nat
s:=sqrt n:nat
n + 0 * 0 + (0 - 0) = n
 apply sqrt_iter_spec; auto.n:nat
s:=sqrt n:nat
n + 0 * 0 + (0 - 0) = n
 simpl.n:nat
s:=sqrt n:nat
n + 0 + 0 = n now rewrite !add_0_r.
Qed.

Definition sqrt_spec a (Ha:0<=a) := sqrt_specif a.

Lemma sqrt_neg a : a<0 -> sqrt a = 0.a:nat
a < 0 -> sqrt a = 0
Proof.a:nat
a < 0 -> sqrt a = 0 inversion 1. Qed.

Logarithm

Lemma log2_iter_spec : forall k p q r,
 2^(S p) = q + S r -> r < 2^p ->
 let s := log2_iter k p q r in
 2^s <= k + q < 2^(S s).forall k p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p ->
let s := log2_iter k p q r in 2 ^ s <= k + q < 2 ^ S s
Proof.forall k p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p ->
let s := log2_iter k p q r in 2 ^ s <= k + q < 2 ^ S s
 induction k.forall p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p ->
let s := log2_iter 0 p q r in 2 ^ s <= 0 + q < 2 ^ S s
k:nat
IHk:forall p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p -> let s := log2_iter k p q r in 2 ^ s <= k + q < 2 ^ S s
forall p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p ->
let s := log2_iter (S k) p q r in
2 ^ s <= S k + q < 2 ^ S s
 - (* k = 0 *)forall p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p ->
let s := log2_iter 0 p q r in 2 ^ s <= 0 + q < 2 ^ S s
   intros p q r EQ LT.p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
let s := log2_iter 0 p q r in 2 ^ s <= 0 + q < 2 ^ S s simpl log2_iter.p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
let s := p in 2 ^ s <= 0 + q < 2 ^ S s cbv zeta.p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
2 ^ p <= 0 + q < 2 ^ S p
   split.p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
2 ^ p <= 0 + q
p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
0 + q < 2 ^ S p
   +p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
2 ^ p <= 0 + q rewrite add_0_l.p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
2 ^ p <= q
     rewrite (add_le_mono_l _ _ (2^p)).p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
2 ^ p + 2 ^ p <= 2 ^ p + q
     simpl pow in EQ.p, q, r:nat
EQ:2 ^ p + (2 ^ p + 0) = q + S r
LT:r < 2 ^ p
2 ^ p + 2 ^ p <= 2 ^ p + q rewrite add_0_r in EQ.p, q, r:nat
EQ:2 ^ p + 2 ^ p = q + S r
LT:r < 2 ^ p
2 ^ p + 2 ^ p <= 2 ^ p + q rewrite EQ.p, q, r:nat
EQ:2 ^ p + 2 ^ p = q + S r
LT:r < 2 ^ p
q + S r <= 2 ^ p + q
     rewrite add_comm.p, q, r:nat
EQ:2 ^ p + 2 ^ p = q + S r
LT:r < 2 ^ p
S r + q <= 2 ^ p + q apply add_le_mono_r.p, q, r:nat
EQ:2 ^ p + 2 ^ p = q + S r
LT:r < 2 ^ p
S r <= 2 ^ p apply LT.
   +p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
0 + q < 2 ^ S p rewrite EQ, add_comm.p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
q + 0 < q + S r apply add_lt_mono_l.p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
0 < S r
     apply lt_succ_r, le_0_l.
 - (* k = S k' *)k:nat
IHk:forall p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p -> let s := log2_iter k p q r in 2 ^ s <= k + q < 2 ^ S s
forall p q r : nat,
2 ^ S p = q + S r ->
r < 2 ^ p ->
let s := log2_iter (S k) p q r in
2 ^ s <= S k + q < 2 ^ S s
   intros p q r EQ LT.k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S r
LT:r < 2 ^ p
let s := log2_iter (S k) p q r in
2 ^ s <= S k + q < 2 ^ S s destruct r.k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = q + 1
LT:0 < 2 ^ p
let s := log2_iter (S k) p q 0 in
2 ^ s <= S k + q < 2 ^ S s
k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
let s := log2_iter (S k) p q (S r) in
2 ^ s <= S k + q < 2 ^ S s
   + (* r = 0 *)k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = q + 1
LT:0 < 2 ^ p
let s := log2_iter (S k) p q 0 in
2 ^ s <= S k + q < 2 ^ S s
     rewrite add_succ_r, add_0_r in EQ.k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
let s := log2_iter (S k) p q 0 in
2 ^ s <= S k + q < 2 ^ S s
     rewrite add_succ_l, <- add_succ_r.k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
let s := log2_iter (S k) p q 0 in
2 ^ s <= k + S q < 2 ^ S s apply IHk.k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
2 ^ S (S p) = S q + S q
k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
q < 2 ^ S p
     *k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
2 ^ S (S p) = S q + S q rewrite <- EQ.k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
2 ^ S (S p) = 2 ^ S p + 2 ^ S p remember (S p) as p'; simpl.k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q, p':nat
Heqp':p' = S p
EQ:2 ^ p' = S q
LT:0 < 2 ^ p
2 ^ p' + (2 ^ p' + 0) = 2 ^ p' + 2 ^ p' now rewrite add_0_r.
     *k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
q < 2 ^ S p rewrite EQ.k:nat
IHk:forall p0 q0 r : nat,
2 ^ S p0 = q0 + S r ->
r < 2 ^ p0 -> let s := log2_iter k p0 q0 r in 2 ^ s <= k + q0 < 2 ^ S s
p, q:nat
EQ:2 ^ S p = S q
LT:0 < 2 ^ p
q < S q constructor.
   + (* r = S r' *)k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
let s := log2_iter (S k) p q (S r) in
2 ^ s <= S k + q < 2 ^ S s
     rewrite add_succ_l, <- add_succ_r.k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
let s := log2_iter (S k) p q (S r) in
2 ^ s <= k + S q < 2 ^ S s apply IHk.k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
2 ^ S p = S q + S r
k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
r < 2 ^ p
     *k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
2 ^ S p = S q + S r now rewrite add_succ_l, <- add_succ_r.
     *k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
r < 2 ^ p apply le_lt_trans with (S r); trivial.k:nat
IHk:forall p0 q0 r0 : nat,
2 ^ S p0 = q0 + S r0 ->
r0 < 2 ^ p0 -> let s := log2_iter k p0 q0 r0 in 2 ^ s <= k + q0 < 2 ^ S s
p, q, r:nat
EQ:2 ^ S p = q + S (S r)
LT:S r < 2 ^ p
r <= S r do 2 constructor.
Qed.

Lemma log2_spec n : 0<n ->
 2^(log2 n) <= n < 2^(S (log2 n)).n:nat
0 < n -> 2 ^ log2 n <= n < 2 ^ S (log2 n)
Proof.n:nat
0 < n -> 2 ^ log2 n <= n < 2 ^ S (log2 n)
 intros.n:nat
H:0 < n
2 ^ log2 n <= n < 2 ^ S (log2 n)
 set (s:=log2 n).n:nat
H:0 < n
s:=log2 n:nat
2 ^ s <= n < 2 ^ S s
 replace n with (pred n + 1).n:nat
H:0 < n
s:=log2 n:nat
2 ^ s <= pred n + 1 < 2 ^ S s
n:nat
H:0 < n
s:=log2 n:nat
pred n + 1 = n
 apply log2_iter_spec; auto.n:nat
H:0 < n
s:=log2 n:nat
pred n + 1 = n
 rewrite add_1_r.n:nat
H:0 < n
s:=log2 n:nat
S (pred n) = n
 apply succ_pred.n:nat
H:0 < n
s:=log2 n:nat
n <> 0 now apply neq_sym, lt_neq.
Qed.

Lemma log2_nonpos n : n<=0 -> log2 n = 0.n:nat
n <= 0 -> log2 n = 0
Proof.n:nat
n <= 0 -> log2 n = 0
 inversion 1; now subst.
Qed.

Gcd

Definition divide x y := exists z, y=z*x.
Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.

Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).forall a b : nat, (gcd a b | a) /\ (gcd a b | b)
Proof.forall a b : nat, (gcd a b | a) /\ (gcd a b | b)
 fix gcd_divide 1.gcd_divide:forall a b : nat,
(gcd a b | a) /\ (gcd a b | b)
forall a b : nat, (gcd a b | a) /\ (gcd a b | b)
 intros [|a] b; simpl.gcd_divide:forall a b0 : nat,
(gcd a b0 | a) /\ (gcd a b0 | b0)
b:nat
(b | 0) /\ (b | b)
gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
(gcd (a - snd (divmod b a 0 a)) (S a) | S a) /\
(gcd (a - snd (divmod b a 0 a)) (S a) | b)
 split.gcd_divide:forall a b0 : nat,
(gcd a b0 | a) /\ (gcd a b0 | b0)
b:nat
(b | 0)
gcd_divide:forall a b0 : nat,
(gcd a b0 | a) /\ (gcd a b0 | b0)
b:nat
(b | b)
gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
(gcd (a - snd (divmod b a 0 a)) (S a) | S a) /\
(gcd (a - snd (divmod b a 0 a)) (S a) | b)
  now exists 0.gcd_divide:forall a b0 : nat,
(gcd a b0 | a) /\ (gcd a b0 | b0)
b:nat
(b | b)
gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
(gcd (a - snd (divmod b a 0 a)) (S a) | S a) /\
(gcd (a - snd (divmod b a 0 a)) (S a) | b)
  exists 1.gcd_divide:forall a b0 : nat,
(gcd a b0 | a) /\ (gcd a b0 | b0)
b:nat
b = 1 * b
gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
(gcd (a - snd (divmod b a 0 a)) (S a) | S a) /\
(gcd (a - snd (divmod b a 0 a)) (S a) | b) simpl.gcd_divide:forall a b0 : nat,
(gcd a b0 | a) /\ (gcd a b0 | b0)
b:nat
b = b + 0
gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
(gcd (a - snd (divmod b a 0 a)) (S a) | S a) /\
(gcd (a - snd (divmod b a 0 a)) (S a) | b) now rewrite <- plus_n_O.gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
(gcd (a - snd (divmod b a 0 a)) (S a) | S a) /\
(gcd (a - snd (divmod b a 0 a)) (S a) | b)
 fold (b mod (S a)).gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
(gcd (b mod S a) (S a) | S a) /\
(gcd (b mod S a) (S a) | b)
 destruct (gcd_divide (b mod (S a)) (S a)) as (H,H').gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
H:(gcd (b mod S a) (S a) | b mod S a)
H':(gcd (b mod S a) (S a) | S a)
(gcd (b mod S a) (S a) | S a) /\
(gcd (b mod S a) (S a) | b)
 set (a':=S a) in *.gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
a':=S a:nat
H:(gcd (b mod a') a' | b mod a')
H':(gcd (b mod a') a' | a')
(gcd (b mod a') a' | a') /\ (gcd (b mod a') a' | b)
 split; auto.gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
a':=S a:nat
H:(gcd (b mod a') a' | b mod a')
H':(gcd (b mod a') a' | a')
(gcd (b mod a') a' | b)
 rewrite (div_mod b a') at 2 by discriminate.gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
a':=S a:nat
H:(gcd (b mod a') a' | b mod a')
H':(gcd (b mod a') a' | a')
(gcd (b mod a') a' | a' * (b / a') + b mod a')
 destruct H as (u,Hu), H' as (v,Hv).gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
a':=S a:nat
u:nat
Hu:b mod a' = u * gcd (b mod a') a'
v:nat
Hv:a' = v * gcd (b mod a') a'
(gcd (b mod a') a' | a' * (b / a') + b mod a')
 rewrite mul_comm.gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
a':=S a:nat
u:nat
Hu:b mod a' = u * gcd (b mod a') a'
v:nat
Hv:a' = v * gcd (b mod a') a'
(gcd (b mod a') a' | b / a' * a' + b mod a')
 exists ((b/a')*v + u).gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
a':=S a:nat
u:nat
Hu:b mod a' = u * gcd (b mod a') a'
v:nat
Hv:a' = v * gcd (b mod a') a'
b / a' * a' + b mod a' =
(b / a' * v + u) * gcd (b mod a') a'
 rewrite mul_add_distr_r.gcd_divide:forall a0 b0 : nat,
(gcd a0 b0 | a0) /\ (gcd a0 b0 | b0)
a, b:nat
a':=S a:nat
u:nat
Hu:b mod a' = u * gcd (b mod a') a'
v:nat
Hv:a' = v * gcd (b mod a') a'
b / a' * a' + b mod a' =
b / a' * v * gcd (b mod a') a' + u * gcd (b mod a') a'
 now rewrite <- mul_assoc, <- Hv, <- Hu.
Qed.

Lemma gcd_divide_l : forall a b, (gcd a b | a).forall a b : nat, (gcd a b | a)
Proof.forall a b : nat, (gcd a b | a)
 intros.a, b:nat
(gcd a b | a) apply gcd_divide.
Qed.

Lemma gcd_divide_r : forall a b, (gcd a b | b).forall a b : nat, (gcd a b | b)
Proof.forall a b : nat, (gcd a b | b)
 intros.a, b:nat
(gcd a b | b) apply gcd_divide.
Qed.

Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).forall a b c : nat,
(c | a) -> (c | b) -> (c | gcd a b)
Proof.forall a b c : nat,
(c | a) -> (c | b) -> (c | gcd a b)
 fix gcd_greatest 1.gcd_greatest:forall a b c : nat,
(c | a) -> (c | b) -> (c | gcd a b)
forall a b c : nat,
(c | a) -> (c | b) -> (c | gcd a b)
 intros [|a] b; simpl; auto.gcd_greatest:forall a0 b0 c : nat,
(c | a0) -> (c | b0) -> (c | gcd a0 b0)
a, b:nat
forall c : nat,
(c | S a) ->
(c | b) -> (c | gcd (a - snd (divmod b a 0 a)) (S a))
 fold (b mod (S a)).gcd_greatest:forall a0 b0 c : nat,
(c | a0) -> (c | b0) -> (c | gcd a0 b0)
a, b:nat
forall c : nat,
(c | S a) -> (c | b) -> (c | gcd (b mod S a) (S a))
 intros c H H'.gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
H:(c | S a)
H':(c | b)
(c | gcd (b mod S a) (S a)) apply gcd_greatest; auto.gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
H:(c | S a)
H':(c | b)
(c | b mod S a)
 set (a':=S a) in *.gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
a':=S a:nat
H:(c | a')
H':(c | b)
(c | b mod a')
 rewrite (div_mod b a') in H' by discriminate.gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
a':=S a:nat
H:(c | a')
H':(c | a' * (b / a') + b mod a')
(c | b mod a')
 destruct H as (u,Hu), H' as (v,Hv).gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
a':=S a:nat
u:nat
Hu:a' = u * c
v:nat
Hv:a' * (b / a') + b mod a' = v * c
(c | b mod a')
 exists (v - (b/a')*u).gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
a':=S a:nat
u:nat
Hu:a' = u * c
v:nat
Hv:a' * (b / a') + b mod a' = v * c
b mod a' = (v - b / a' * u) * c
 rewrite mul_comm in Hv.gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
a':=S a:nat
u:nat
Hu:a' = u * c
v:nat
Hv:b / a' * a' + b mod a' = v * c
b mod a' = (v - b / a' * u) * c
 rewrite mul_sub_distr_r, <- Hv, <- mul_assoc, <-Hu.gcd_greatest:forall a0 b0 c0 : nat,
(c0 | a0) ->
(c0 | b0) -> (c0 | gcd a0 b0)
a, b, c:nat
a':=S a:nat
u:nat
Hu:a' = u * c
v:nat
Hv:b / a' * a' + b mod a' = v * c
b mod a' = b / a' * a' + b mod a' - b / a' * a'
 now rewrite add_comm, add_sub.
Qed.

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

Bitwise operations

Lemma div2_double n : div2 (2*n) = n.n:nat
div2 (2 * n) = n
Proof.n:nat
div2 (2 * n) = n
 induction n; trivial.n:nat
IHn:div2 (2 * n) = n
div2 (2 * S n) = S n
 simpl mul.n:nat
IHn:div2 (2 * n) = n
div2 (S (n + S (n + 0))) = S n rewrite add_succ_r.n:nat
IHn:div2 (2 * n) = n
div2 (S (S (n + (n + 0)))) = S n simpl.n:nat
IHn:div2 (2 * n) = n
S (div2 (n + (n + 0))) = S n now f_equal.
Qed.

Lemma div2_succ_double n : div2 (S (2*n)) = n.n:nat
div2 (S (2 * n)) = n
Proof.n:nat
div2 (S (2 * n)) = n
 induction n; trivial.n:nat
IHn:div2 (S (2 * n)) = n
div2 (S (2 * S n)) = S n
 simpl.n:nat
IHn:div2 (S (2 * n)) = n
S (div2 (n + S (n + 0))) = S n f_equal.n:nat
IHn:div2 (S (2 * n)) = n
div2 (n + S (n + 0)) = n now rewrite add_succ_r.
Qed.

Lemma le_div2 n : div2 (S n) <= n.n:nat
div2 (S n) <= n
Proof.n:nat
div2 (S n) <= n
 revert n.forall n : nat, div2 (S n) <= n
 fix le_div2 1.le_div2:forall n : nat, div2 (S n) <= n
forall n : nat, div2 (S n) <= n
 destruct n; simpl; trivial.le_div2:forall n0 : nat, div2 (S n0) <= n0
n:nat
S (div2 n) <= S n apply lt_succ_r.le_div2:forall n0 : nat, div2 (S n0) <= n0
n:nat
div2 n <= n
 destruct n; [simpl|]; trivial.le_div2:forall n0 : nat, div2 (S n0) <= n0
n:nat
div2 (S n) <= S n now constructor.
Qed.

Lemma lt_div2 n : 0 < n -> div2 n < n.n:nat
0 < n -> div2 n < n
Proof.n:nat
0 < n -> div2 n < n
 destruct n.0 < 0 -> div2 0 < 0
n:nat
0 < S n -> div2 (S n) < S n
 -0 < 0 -> div2 0 < 0 inversion 1.
 -n:nat
0 < S n -> div2 (S n) < S n intros _.n:nat
div2 (S n) < S n apply lt_succ_r, le_div2.
Qed.

Lemma div2_decr a n : a <= S n -> div2 a <= n.a, n:nat
a <= S n -> div2 a <= n
Proof.a, n:nat
a <= S n -> div2 a <= n
 destruct a; intros H.n:nat
H:0 <= S n
div2 0 <= n
a, n:nat
H:S a <= S n
div2 (S a) <= n
 -n:nat
H:0 <= S n
div2 0 <= n simpl.n:nat
H:0 <= S n
0 <= n apply le_0_l.
 -a, n:nat
H:S a <= S n
div2 (S a) <= n apply succ_le_mono in H.a, n:nat
H:a <= n
div2 (S a) <= n
   apply le_trans with a; [ apply le_div2 | trivial ].
Qed.

Lemma double_twice : forall n, double n = 2*n.forall n : nat, double n = 2 * n
Proof.forall n : nat, double n = 2 * n
 simpl; intros.n:nat
double n = n + (n + 0) now rewrite add_0_r.
Qed.

Lemma testbit_0_l : forall n, testbit 0 n = false.forall n : nat, testbit 0 n = false
Proof.forall n : nat, testbit 0 n = false
 now induction n.
Qed.

Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.a:nat
testbit (2 * a + 1) 0 = true
Proof.a:nat
testbit (2 * a + 1) 0 = true
 unfold testbit.a:nat
odd (2 * a + 1) = true rewrite odd_spec.a:nat
Odd (2 * a + 1) now exists a.
Qed.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.a:nat
testbit (2 * a) 0 = false
Proof.a:nat
testbit (2 * a) 0 = false
 unfold testbit, odd.a:nat
negb (even (2 * a)) = false rewrite (proj2 (even_spec _)); trivial.a:nat
Even (2 * a)
 now exists a.
Qed.

Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n.a, n:nat
testbit (2 * a + 1) (S n) = testbit a n
Proof.a, n:nat
testbit (2 * a + 1) (S n) = testbit a n
 unfold testbit; fold testbit.a, n:nat
testbit (div2 (2 * a + 1)) n = testbit a n
 rewrite add_1_r.a, n:nat
testbit (div2 (S (2 * a))) n = testbit a n f_equal.a, n:nat
div2 (S (2 * a)) = a
 apply div2_succ_double.
Qed.

Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n.a, n:nat
testbit (2 * a) (S n) = testbit a n
Proof.a, n:nat
testbit (2 * a) (S n) = testbit a n
 unfold testbit; fold testbit.a, n:nat
testbit (div2 (2 * a)) n = testbit a n f_equal.a, n:nat
div2 (2 * a) = a apply div2_double.
Qed.

Lemma shiftr_specif : forall a n m,
 testbit (shiftr a n) m = testbit a (m+n).forall a n m : nat,
testbit (shiftr a n) m = testbit a (m + n)
Proof.forall a n m : nat,
testbit (shiftr a n) m = testbit a (m + n)
 induction n; intros m.a, m:nat
testbit (shiftr a 0) m = testbit a (m + 0)
a, n:nat
IHn:forall m0 : nat, testbit (shiftr a n) m0 = testbit a (m0 + n)
m:nat
testbit (shiftr a (S n)) m = testbit a (m + S n) trivial.a, m:nat
testbit (shiftr a 0) m = testbit a (m + 0)
a, n:nat
IHn:forall m0 : nat, testbit (shiftr a n) m0 = testbit a (m0 + n)
m:nat
testbit (shiftr a (S n)) m = testbit a (m + S n)
 now rewrite add_0_r.a, n:nat
IHn:forall m0 : nat, testbit (shiftr a n) m0 = testbit a (m0 + n)
m:nat
testbit (shiftr a (S n)) m = testbit a (m + S n)
 now rewrite add_succ_r, <- add_succ_l, <- IHn.
Qed.

Lemma shiftl_specif_high : forall a n m, n<=m ->
 testbit (shiftl a n) m = testbit a (m-n).forall a n m : nat,
n <= m -> testbit (shiftl a n) m = testbit a (m - n)
Proof.forall a n m : nat,
n <= m -> testbit (shiftl a n) m = testbit a (m - n)
 induction n; intros m H.a, m:nat
H:0 <= m
testbit (shiftl a 0) m = testbit a (m - 0)
a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:S n <= m
testbit (shiftl a (S n)) m = testbit a (m - S n) trivial.a, m:nat
H:0 <= m
testbit (shiftl a 0) m = testbit a (m - 0)
a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:S n <= m
testbit (shiftl a (S n)) m = testbit a (m - S n)
 now rewrite sub_0_r.a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:S n <= m
testbit (shiftl a (S n)) m = testbit a (m - S n)
 destruct m.a, n:nat
IHn:forall m : nat, n <= m -> testbit (shiftl a n) m = testbit a (m - n)
H:S n <= 0
testbit (shiftl a (S n)) 0 = testbit a (0 - S n)
a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:S n <= S m
testbit (shiftl a (S n)) (S m) = testbit a (S m - S n) inversion H.a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:S n <= S m
testbit (shiftl a (S n)) (S m) = testbit a (S m - S n)
 simpl.a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:S n <= S m
testbit (div2 (double (shiftl a n))) m =
testbit a (m - n) apply succ_le_mono in H.a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:n <= m
testbit (div2 (double (shiftl a n))) m =
testbit a (m - n)
 change (shiftl a (S n)) with (double (shiftl a n)).a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:n <= m
testbit (div2 (double (shiftl a n))) m =
testbit a (m - n)
 rewrite double_twice, div2_double.a, n:nat
IHn:forall m0 : nat, n <= m0 -> testbit (shiftl a n) m0 = testbit a (m0 - n)
m:nat
H:n <= m
testbit (shiftl a n) m = testbit a (m - n) now apply IHn.
Qed.

Lemma shiftl_spec_low : forall a n m, m<n ->
 testbit (shiftl a n) m = false.forall a n m : nat,
m < n -> testbit (shiftl a n) m = false
Proof.forall a n m : nat,
m < n -> testbit (shiftl a n) m = false
 induction n; intros m H.a, m:nat
H:m < 0
testbit (shiftl a 0) m = false
a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:m < S n
testbit (shiftl a (S n)) m = false inversion H.a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:m < S n
testbit (shiftl a (S n)) m = false
 change (shiftl a (S n)) with (double (shiftl a n)).a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:m < S n
testbit (double (shiftl a n)) m = false
 destruct m; simpl.a, n:nat
IHn:forall m : nat, m < n -> testbit (shiftl a n) m = false
H:0 < S n
odd (double (shiftl a n)) = false
a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
testbit (div2 (double (shiftl a n))) m = false
 unfold odd.a, n:nat
IHn:forall m : nat, m < n -> testbit (shiftl a n) m = false
H:0 < S n
negb (even (double (shiftl a n))) = false
a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
testbit (div2 (double (shiftl a n))) m = false apply negb_false_iff.a, n:nat
IHn:forall m : nat, m < n -> testbit (shiftl a n) m = false
H:0 < S n
even (double (shiftl a n)) = true
a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
testbit (div2 (double (shiftl a n))) m = false
 apply even_spec.a, n:nat
IHn:forall m : nat, m < n -> testbit (shiftl a n) m = false
H:0 < S n
Even (double (shiftl a n))
a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
testbit (div2 (double (shiftl a n))) m = false exists (shiftl a n).a, n:nat
IHn:forall m : nat, m < n -> testbit (shiftl a n) m = false
H:0 < S n
double (shiftl a n) = 2 * shiftl a n
a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
testbit (div2 (double (shiftl a n))) m = false apply double_twice.a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
testbit (div2 (double (shiftl a n))) m = false
 rewrite double_twice, div2_double.a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
testbit (shiftl a n) m = false apply IHn.a, n:nat
IHn:forall m0 : nat, m0 < n -> testbit (shiftl a n) m0 = false
m:nat
H:S m < S n
m < n
 now apply succ_le_mono.
Qed.

Lemma div2_bitwise : forall op n a b,
 div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).forall (op : bool -> bool -> bool) (n a b : nat),
div2 (bitwise op (S n) a b) =
bitwise op n (div2 a) (div2 b)
Proof.forall (op : bool -> bool -> bool) (n a b : nat),
div2 (bitwise op (S n) a b) =
bitwise op n (div2 a) (div2 b)
 intros.op:bool -> bool -> bool
n, a, b:nat
div2 (bitwise op (S n) a b) =
bitwise op n (div2 a) (div2 b) unfold bitwise; fold bitwise.op:bool -> bool -> bool
n, a, b:nat
div2
  ((if op (odd a) (odd b) then 1 else 0) +
   2 * bitwise op n (div2 a) (div2 b)) =
bitwise op n (div2 a) (div2 b)
 destruct (op (odd a) (odd b)).op:bool -> bool -> bool
n, a, b:nat
div2 (1 + 2 * bitwise op n (div2 a) (div2 b)) =
bitwise op n (div2 a) (div2 b)
op:bool -> bool -> bool
n, a, b:nat
div2 (0 + 2 * bitwise op n (div2 a) (div2 b)) =
bitwise op n (div2 a) (div2 b)
 now rewrite div2_succ_double.op:bool -> bool -> bool
n, a, b:nat
div2 (0 + 2 * bitwise op n (div2 a) (div2 b)) =
bitwise op n (div2 a) (div2 b)
 now rewrite add_0_l, div2_double.
Qed.

Lemma odd_bitwise : forall op n a b,
 odd (bitwise op (S n) a b) = op (odd a) (odd b).forall (op : bool -> bool -> bool) (n a b : nat),
odd (bitwise op (S n) a b) = op (odd a) (odd b)
Proof.forall (op : bool -> bool -> bool) (n a b : nat),
odd (bitwise op (S n) a b) = op (odd a) (odd b)
 intros.op:bool -> bool -> bool
n, a, b:nat
odd (bitwise op (S n) a b) = op (odd a) (odd b) unfold bitwise; fold bitwise.op:bool -> bool -> bool
n, a, b:nat
odd
  ((if op (odd a) (odd b) then 1 else 0) +
   2 * bitwise op n (div2 a) (div2 b)) =
op (odd a) (odd b)
 destruct (op (odd a) (odd b)).op:bool -> bool -> bool
n, a, b:nat
odd (1 + 2 * bitwise op n (div2 a) (div2 b)) = true
op:bool -> bool -> bool
n, a, b:nat
odd (0 + 2 * bitwise op n (div2 a) (div2 b)) = false
 apply odd_spec.op:bool -> bool -> bool
n, a, b:nat
Odd (1 + 2 * bitwise op n (div2 a) (div2 b))
op:bool -> bool -> bool
n, a, b:nat
odd (0 + 2 * bitwise op n (div2 a) (div2 b)) = false rewrite add_comm.op:bool -> bool -> bool
n, a, b:nat
Odd (2 * bitwise op n (div2 a) (div2 b) + 1)
op:bool -> bool -> bool
n, a, b:nat
odd (0 + 2 * bitwise op n (div2 a) (div2 b)) = false eexists; eauto.op:bool -> bool -> bool
n, a, b:nat
odd (0 + 2 * bitwise op n (div2 a) (div2 b)) = false
 unfold odd.op:bool -> bool -> bool
n, a, b:nat
negb (even (0 + 2 * bitwise op n (div2 a) (div2 b))) =
false apply negb_false_iff.op:bool -> bool -> bool
n, a, b:nat
even (0 + 2 * bitwise op n (div2 a) (div2 b)) = true apply even_spec.op:bool -> bool -> bool
n, a, b:nat
Even (0 + 2 * bitwise op n (div2 a) (div2 b))
 rewrite add_0_l; eexists; eauto.
Qed.

Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) ->
 forall n m a b, a<=n ->
 testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).forall op : bool -> bool -> bool,
(forall b : bool, op false b = false) ->
forall n m a b : nat,
a <= n ->
testbit (bitwise op n a b) m =
op (testbit a m) (testbit b m)
Proof.forall op : bool -> bool -> bool,
(forall b : bool, op false b = false) ->
forall n m a b : nat,
a <= n ->
testbit (bitwise op n a b) m =
op (testbit a m) (testbit b m)
 intros op Hop.op:bool -> bool -> bool
Hop:forall b : bool, op false b = false
forall n m a b : nat,
a <= n ->
testbit (bitwise op n a b) m =
op (testbit a m) (testbit b m)
 induction n; intros m a b Ha.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
m, a, b:nat
Ha:a <= 0
testbit (bitwise op 0 a b) m =
op (testbit a m) (testbit b m)
op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m)
 simpl.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
m, a, b:nat
Ha:a <= 0
testbit 0 m = op (testbit a m) (testbit b m)
op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m) inversion Ha; subst.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
m, b:nat
Ha:0 <= 0
testbit 0 m = op (testbit 0 m) (testbit b m)
op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m) now rewrite testbit_0_l.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m)
 destruct m.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m a0 b0 : nat,
a0 <= n -> testbit (bitwise op n a0 b0) m = op (testbit a0 m) (testbit b0 m)
a, b:nat
Ha:a <= S n
testbit (bitwise op (S n) a b) 0 =
op (testbit a 0) (testbit b 0)
op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (bitwise op (S n) a b) (S m) =
op (testbit a (S m)) (testbit b (S m))
 apply odd_bitwise.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (bitwise op (S n) a b) (S m) =
op (testbit a (S m)) (testbit b (S m))
 unfold testbit; fold testbit.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (div2 (bitwise op (S n) a b)) m =
op (testbit (div2 a) m) (testbit (div2 b) m) rewrite div2_bitwise.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
testbit (bitwise op n (div2 a) (div2 b)) m =
op (testbit (div2 a) m) (testbit (div2 b) m)
 apply IHn.op:bool -> bool -> bool
Hop:forall b0 : bool, op false b0 = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
div2 a <= n now apply div2_decr.
Qed.

Lemma testbit_bitwise_2 : forall op, op false false = false ->
 forall n m a b, a<=n -> b<=n ->
 testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).forall op : bool -> bool -> bool,
op false false = false ->
forall n m a b : nat,
a <= n ->
b <= n ->
testbit (bitwise op n a b) m =
op (testbit a m) (testbit b m)
Proof.forall op : bool -> bool -> bool,
op false false = false ->
forall n m a b : nat,
a <= n ->
b <= n ->
testbit (bitwise op n a b) m =
op (testbit a m) (testbit b m)
 intros op Hop.op:bool -> bool -> bool
Hop:op false false = false
forall n m a b : nat,
a <= n ->
b <= n ->
testbit (bitwise op n a b) m =
op (testbit a m) (testbit b m)
 induction n; intros m a b Ha Hb.op:bool -> bool -> bool
Hop:op false false = false
m, a, b:nat
Ha:a <= 0
Hb:b <= 0
testbit (bitwise op 0 a b) m =
op (testbit a m) (testbit b m)
op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m)
 simpl.op:bool -> bool -> bool
Hop:op false false = false
m, a, b:nat
Ha:a <= 0
Hb:b <= 0
testbit 0 m = op (testbit a m) (testbit b m)
op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m) inversion Ha; inversion Hb; subst.op:bool -> bool -> bool
Hop:op false false = false
m:nat
Ha, Hb:0 <= 0
testbit 0 m = op (testbit 0 m) (testbit 0 m)
op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m) now rewrite testbit_0_l.op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op (S n) a b) m =
op (testbit a m) (testbit b m)
 destruct m.op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m a0 b0 : nat,
a0 <= n ->
b0 <= n -> testbit (bitwise op n a0 b0) m = op (testbit a0 m) (testbit b0 m)
a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op (S n) a b) 0 =
op (testbit a 0) (testbit b 0)
op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op (S n) a b) (S m) =
op (testbit a (S m)) (testbit b (S m))
 apply odd_bitwise.op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op (S n) a b) (S m) =
op (testbit a (S m)) (testbit b (S m))
 unfold testbit; fold testbit.op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (div2 (bitwise op (S n) a b)) m =
op (testbit (div2 a) m) (testbit (div2 b) m) rewrite div2_bitwise.op:bool -> bool -> bool
Hop:op false false = false
n:nat
IHn:forall m0 a0 b0 : nat,
a0 <= n ->
b0 <= n ->
testbit (bitwise op n a0 b0) m0 = op (testbit a0 m0) (testbit b0 m0)
m, a, b:nat
Ha:a <= S n
Hb:b <= S n
testbit (bitwise op n (div2 a) (div2 b)) m =
op (testbit (div2 a) m) (testbit (div2 b) m)
 apply IHn; now apply div2_decr.
Qed.

Lemma land_spec a b n :
 testbit (land a b) n = testbit a n && testbit b n.a, b, n:nat
testbit (land a b) n = testbit a n && testbit b n
Proof.a, b, n:nat
testbit (land a b) n = testbit a n && testbit b n
 unfold land.a, b, n:nat
testbit (bitwise andb a a b) n =
testbit a n && testbit b n apply testbit_bitwise_1; trivial.
Qed.

Lemma ldiff_spec a b n :
 testbit (ldiff a b) n = testbit a n && negb (testbit b n).a, b, n:nat
testbit (ldiff a b) n =
testbit a n && negb (testbit b n)
Proof.a, b, n:nat
testbit (ldiff a b) n =
testbit a n && negb (testbit b n)
 unfold ldiff.a, b, n:nat
testbit
  (bitwise (fun b0 b' : bool => b0 && negb b') a a b)
  n = testbit a n && negb (testbit b n) apply testbit_bitwise_1; trivial.
Qed.

Lemma lor_spec a b n :
 testbit (lor a b) n = testbit a n || testbit b n.a, b, n:nat
testbit (lor a b) n = testbit a n || testbit b n
Proof.a, b, n:nat
testbit (lor a b) n = testbit a n || testbit b n
 unfold lor.a, b, n:nat
testbit (bitwise orb (max a b) a b) n =
testbit a n || testbit b n apply testbit_bitwise_2.a, b, n:nat
false || false = false
a, b, n:nat
a <= max a b
a, b, n:nat
b <= max a b
 -a, b, n:nat
false || false = false trivial.
 -a, b, n:nat
a <= max a b destruct (compare_spec a b).a, b, n:nat
H:a = b
a <= max a b
a, b, n:nat
H:a < b
a <= max a b
a, b, n:nat
H:b < a
a <= max a b
   +a, b, n:nat
H:a = b
a <= max a b rewrite max_l; subst; trivial.
   +a, b, n:nat
H:a < b
a <= max a b apply lt_le_incl in H.a, b, n:nat
H:a <= b
a <= max a b now rewrite max_r.
   +a, b, n:nat
H:b < a
a <= max a b apply lt_le_incl in H.a, b, n:nat
H:b <= a
a <= max a b now rewrite max_l.
 -a, b, n:nat
b <= max a b destruct (compare_spec a b).a, b, n:nat
H:a = b
b <= max a b
a, b, n:nat
H:a < b
b <= max a b
a, b, n:nat
H:b < a
b <= max a b
   +a, b, n:nat
H:a = b
b <= max a b rewrite max_r; subst; trivial.
   +a, b, n:nat
H:a < b
b <= max a b apply lt_le_incl in H.a, b, n:nat
H:a <= b
b <= max a b now rewrite max_r.
   +a, b, n:nat
H:b < a
b <= max a b apply lt_le_incl in H.a, b, n:nat
H:b <= a
b <= max a b now rewrite max_l.
Qed.

Lemma lxor_spec a b n :
 testbit (lxor a b) n = xorb (testbit a n) (testbit b n).a, b, n:nat
testbit (lxor a b) n =
xorb (testbit a n) (testbit b n)
Proof.a, b, n:nat
testbit (lxor a b) n =
xorb (testbit a n) (testbit b n)
 unfold lxor.a, b, n:nat
testbit (bitwise xorb (max a b) a b) n =
xorb (testbit a n) (testbit b n) apply testbit_bitwise_2.a, b, n:nat
xorb false false = false
a, b, n:nat
a <= max a b
a, b, n:nat
b <= max a b
 -a, b, n:nat
xorb false false = false trivial.
 -a, b, n:nat
a <= max a b destruct (compare_spec a b).a, b, n:nat
H:a = b
a <= max a b
a, b, n:nat
H:a < b
a <= max a b
a, b, n:nat
H:b < a
a <= max a b
   +a, b, n:nat
H:a = b
a <= max a b rewrite max_l; subst; trivial.
   +a, b, n:nat
H:a < b
a <= max a b apply lt_le_incl in H.a, b, n:nat
H:a <= b
a <= max a b now rewrite max_r.
   +a, b, n:nat
H:b < a
a <= max a b apply lt_le_incl in H.a, b, n:nat
H:b <= a
a <= max a b now rewrite max_l.
 -a, b, n:nat
b <= max a b destruct (compare_spec a b).a, b, n:nat
H:a = b
b <= max a b
a, b, n:nat
H:a < b
b <= max a b
a, b, n:nat
H:b < a
b <= max a b
   +a, b, n:nat
H:a = b
b <= max a b rewrite max_r; subst; trivial.
   +a, b, n:nat
H:a < b
b <= max a b apply lt_le_incl in H.a, b, n:nat
H:a <= b
b <= max a b now rewrite max_r.
   +a, b, n:nat
H:b < a
b <= max a b apply lt_le_incl in H.a, b, n:nat
H:b <= a
b <= max a b now rewrite max_l.
Qed.

Lemma div2_spec a : div2 a = shiftr a 1.a:nat
div2 a = shiftr a 1
Proof.a:nat
div2 a = shiftr a 1
 reflexivity.
Qed.

Aliases with extra dummy hypothesis, to fulfil the interface

Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ' a n.
Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ' a n.
Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.a, n:nat
H:n < 0
testbit a n = false
Proof.a, n:nat
H:n < 0
testbit a n = false inversion H. Qed.

Definition shiftl_spec_high a n m (_:0<=m) := shiftl_specif_high a n m.
Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m.

Properties of advanced functions (pow, sqrt, log2, ...)

Include NExtraProp.

Properties of tail-recursive addition and multiplication

Lemma tail_add_spec n m : tail_add n m = n + m.n, m:nat
tail_add n m = n + m
Proof.n, m:nat
tail_add n m = n + m
 revert m.n:nat
forall m : nat, tail_add n m = n + m induction n as [|n IH]; simpl; trivial.n:nat
IH:forall m : nat, tail_add n m = n + m
forall m : nat, tail_add n (S m) = S (n + m)
 intros.n:nat
IH:forall m0 : nat, tail_add n m0 = n + m0
m:nat
tail_add n (S m) = S (n + m) now rewrite IH, add_succ_r.
Qed.

Lemma tail_addmul_spec r n m : tail_addmul r n m = r + n * m.r, n, m:nat
tail_addmul r n m = r + n * m
Proof.r, n, m:nat
tail_addmul r n m = r + n * m
 revert m r.n:nat
forall m r : nat, tail_addmul r n m = r + n * m induction n as [| n IH]; simpl; trivial.n:nat
IH:forall m r : nat, tail_addmul r n m = r + n * m
forall m r : nat,
tail_addmul (tail_add m r) n m = r + (m + n * m)
 intros.n:nat
IH:forall m0 r0 : nat,
tail_addmul r0 n m0 = r0 + n * m0
m, r:nat
tail_addmul (tail_add m r) n m = r + (m + n * m) rewrite IH, tail_add_spec.n:nat
IH:forall m0 r0 : nat,
tail_addmul r0 n m0 = r0 + n * m0
m, r:nat
m + r + n * m = r + (m + n * m)
 rewrite add_assoc.n:nat
IH:forall m0 r0 : nat,
tail_addmul r0 n m0 = r0 + n * m0
m, r:nat
m + r + n * m = r + m + n * m f_equal.n:nat
IH:forall m0 r0 : nat,
tail_addmul r0 n m0 = r0 + n * m0
m, r:nat
m + r = r + m apply add_comm.
Qed.

Lemma tail_mul_spec n m : tail_mul n m = n * m.n, m:nat
tail_mul n m = n * m
Proof.n, m:nat
tail_mul n m = n * m
 unfold tail_mul.n, m:nat
tail_addmul 0 n m = n * m now rewrite tail_addmul_spec.
Qed.

End Nat.

Re-export notations that should be available even when the Nat module is not imported.

Bind Scope nat_scope with Nat.t nat.

Infix "^" := Nat.pow : nat_scope.
Infix "=?" := Nat.eqb (at level 70) : nat_scope.
Infix "<=?" := Nat.leb (at level 70) : nat_scope.
Infix "<?" := Nat.ltb (at level 70) : nat_scope.
Infix "?=" := Nat.compare (at level 70) : nat_scope.
Infix "/" := Nat.div : nat_scope.
Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.

Hint Unfold Nat.le : core.
Hint Unfold Nat.lt : core.

Nat contains an order tactic for natural numbers

Note that Nat.order is domain-agnostic: it will not prove 1<=2 or x≤x+x, but rather things like x≤y → y≤x → x=y.

Section TestOrder.
 Let test : forall x y, x<=y -> y<=x -> x=y.forall x y : nat, x <= y -> y <= x -> x = y
 Proof.forall x y : nat, x <= y -> y <= x -> x = y
 Nat.order.
 Qed.
End TestOrder.