Library Coq.Numbers.Natural.Peano.NPeano

Require Import
Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat Div2 Wf_nat
NAxioms NProperties.

Functions not already defined

Fixpoint leb n m :=
  match n, m with
    | O, _ => true
    | _, O => false
    | S n´, S m´ => leb n´ m´
  end.

Definition ltb n m := leb (S n) m.

Infix "<=?" := leb (at level 70) : nat_scope.
Infix "<?" := ltb (at level 70) : nat_scope.

Lemma leb_le n m : (n <=? m ) = true <-> n <= m.

Lemma ltb_lt n m : (n <? m ) = true <-> n < m.

Fixpoint pow n m :=
  match m with
    | O => 1
    | S m => n * (pow n m )
  end.

Infix "^" := pow : nat_scope.

Lemma pow_0_r : forall a, a ^0 = 1.

Lemma pow_succ_r : forall a b, 0<=b -> a ^(S b ) = a * a ^b.

Definition square n := n * n.

Lemma square_spec n : square n = n * n.

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

Fixpoint even n :=
  match n with
    | O => true
    | 1 => false
    | S (S n´) => even n´
  end.

Definition odd n := negb (even n).

Lemma even_spec : forall n, even n = true <-> Even n.

Lemma odd_spec : forall n, odd n = true <-> Odd n.

Lemma Even_equiv : forall n, Even n <-> Even.even n.

Lemma Odd_equiv : forall n, Odd n <-> Even.odd n.

Fixpoint divmod x y q u :=
  match x with
    | 0 => (q ,u )
    | S x´ => match u with
                | 0 => divmod x´ y (S q) y
                | S u´ => divmod x´ y q u´
              end
  end.

Definition div x y :=
  match y with
    | 0 => y
    | S y´ => fst (divmod x y´ 0 y´)
  end.

Definition modulo x y :=
  match y with
    | 0 => y
    | S y´ => y´ - snd (divmod x y´ 0 y´)
  end.

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

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.

Lemma div_mod : forall x y, y <>0 -> x = y *(x /y ) + x mod y.

Lemma mod_bound_pos : forall x y, 0<=x -> 0<y -> 0 <= x mod y < y.

Square root

The following square root function is linear (and tail-recursive). With Peano representation, we can't do better. For faster algorithm, see Psqrt/Zsqrt/Nsqrt...

We search the square root of n = k + p^2 + (q - r) with q = 2p and 0<=r<=q. We start with p=q=r=0, hence looking for the square root of n = k. Then we progressively decrease k and r. When k = S k' and r=0, it means we can use (S p) as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2. When k reaches 0, we have found the biggest p^2 square contained in n, hence the square root of n is p.

Fixpoint sqrt_iter k p q r :=
  match k with
    | O => p
    | S k´ => match r with
                | O => sqrt_iter k´ (S p) (S (S q)) (S (S q))
                | S r´ => sqrt_iter k´ p q r´
              end
  end.

Definition sqrt n := sqrt_iter n 0 0 0.

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 ).

Lemma sqrt_spec : forall n,
(sqrt n )*(sqrt n ) <= n < S (sqrt n) * S (sqrt n).

A linear tail-recursive base-2 logarithm

In log2_iter, we maintain the logarithm p of the counter q, while r is the distance between q and the next power of 2, more precisely q + S r = 2^(S p) and r<2^p. At each recursive call, q goes up while r goes down. When r is 0, we know that q has almost reached a power of 2, and we increase p at the next call, while resetting r to q.

Graphically (numbers are q, stars are r) :

                    10
                  9
                8
              7   *
            6       *
          5           ...
        4
      3   *
    2       *
  1   *       *
0   *   *       *

We stop when k, the global downward counter reaches 0. At that moment, q is the number we're considering (since k+q is invariant), and p its logarithm.

Fixpoint log2_iter k p q r :=
  match k with
    | O => p
    | S k´ => match r with
                | O => log2_iter k´ (S p) (S q) q
                | S r´ => log2_iter k´ p (S q) r´
              end
  end.

Definition log2 n := log2_iter (pred n) 0 1 0.

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 ).

Lemma log2_spec : forall n, 0<n ->
2^(log2 n ) <= n < 2^(S (log2 n)).

Lemma log2_nonpos : forall n, n <=0 -> log2 n = 0.

Gcd

We use Euclid algorithm, which is normally not structural, but Coq is now clever enough to accept this (behind modulo there is a subtraction, which now preserves being a subterm)

Bitwise operations

We provide here some bitwise operations for unary numbers. Some might be really naive, they are just there for fullfiling the same interface as other for natural representations. As soon as binary representations such as NArith are available, it is clearly better to convert to/from them and use their ops.

Fixpoint testbit a n :=
match n with
   | O => odd a
   | S n => testbit (div2 a) n
end.

Definition shiftl a n := iter_nat n _ double a.
Definition shiftr a n := iter_nat n _ div2 a.

Fixpoint bitwise (op:bool->bool->bool) n a b :=
match n with
  | O => O
  | S n´ =>
    (if op (odd a) (odd b) then 1 else 0) +
    2*(bitwise op n´ (div2 a) (div2 b))
end.

Definition land a b := bitwise andb a a b.
Definition lor a b := bitwise orb (max a b) a b.
Definition ldiff a b := bitwise (fun b b´ => b && negb b´) a a b.
Definition lxor a b := bitwise xorb (max a b) a b.

Lemma double_twice : forall n, double n = 2*n.

Lemma testbit_0_l : forall n, testbit 0 n = false.

Lemma testbit_odd_0 a : testbit (2*a +1) 0 = true.

Lemma testbit_even_0 a : testbit (2*a) 0 = false.

Lemma testbit_odd_succ a n : testbit (2*a +1) (S n) = testbit a n.

Lemma testbit_even_succ a n : testbit (2*a) (S n) = testbit a n.

Lemma shiftr_spec : forall a n m,
testbit (shiftr a n) m = testbit a (m +n).

Lemma shiftl_spec_high : forall a n m, n <=m ->
testbit (shiftl a n) m = testbit a (m -n).

Lemma shiftl_spec_low : forall a n m, m <n ->
testbit (shiftl a n) m = false.

Lemma div2_bitwise : forall op n a b,
div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).

Lemma odd_bitwise : forall op n a b,
odd (bitwise op (S n) a b) = op (odd a) (odd b).

Lemma div2_decr : forall a n, a <= S n -> div2 a <= n.

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).

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).

Lemma land_spec : forall a b n,
testbit (land a b) n = testbit a n && testbit b n.

Lemma ldiff_spec : forall a b n,
testbit (ldiff a b) n = testbit a n && negb (testbit b n).

Lemma lor_spec : forall a b n,
testbit (lor a b) n = testbit a n || testbit b n.

Lemma lxor_spec : forall a b n,
testbit (lxor a b) n = xorb (testbit a n) (testbit b n).

Implementation of NAxiomsSig by nat

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

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.

Basic operations.

Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
Local Obligation Tactic := simpl_relation.
Program Instance succ_wd : Proper (eq ==>eq) S.
Program Instance pred_wd : Proper (eq ==>eq) pred.
Program Instance add_wd : Proper (eq ==>eq ==>eq) plus.
Program Instance sub_wd : Proper (eq ==>eq ==>eq) minus.
Program Instance mul_wd : Proper (eq ==>eq ==>eq) mult.

Theorem pred_succ : forall n : nat, pred (S n) = n.

Theorem one_succ : 1 = S 0.

Theorem two_succ : 2 = S 1.

Theorem add_0_l : forall n : nat, 0 + n = n.

Theorem add_succ_l : forall n m : nat, (S n ) + m = S (n + m).

Theorem sub_0_r : forall n : nat, n - 0 = n.

Theorem sub_succ_r : forall n m : nat, n - (S m ) = pred (n - m).

Theorem mul_0_l : forall n : nat, 0 * n = 0.

Theorem mul_succ_l : forall n m : nat, S n * m = n * m + m.

Order on natural numbers

Program Instance lt_wd : Proper (eq ==>eq ==>iff) lt.

Theorem lt_succ_r : forall n m : nat, n < S m <-> n <= m.

Theorem lt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.

Theorem lt_irrefl : forall n : nat, ~ (n < n ).

Facts specific to natural numbers, not integers.

Theorem pred_0 : pred 0 = 0.

Recursion fonction

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.

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

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)).

The instantiation of operations. Placing them at the very end avoids having indirections in above lemmas.

Definition t := nat.
Definition eq := @eq nat.
Definition eqb := beq_nat.
Definition compare := nat_compare.
Definition zero := 0.
Definition one := 1.
Definition two := 2.
Definition succ := S.
Definition pred := pred.
Definition add := plus.
Definition sub := minus.
Definition mul := mult.
Definition lt := lt.
Definition le := le.
Definition ltb := ltb.
Definition leb := leb.

Definition min := min.
Definition max := max.
Definition max_l := max_l.
Definition max_r := max_r.
Definition min_l := min_l.
Definition min_r := min_r.

Definition eqb_eq := beq_nat_true_iff.
Definition compare_spec := nat_compare_spec.
Definition eq_dec := eq_nat_dec.
Definition leb_le := leb_le.
Definition ltb_lt := ltb_lt.

Definition Even := Even.
Definition Odd := Odd.
Definition even := even.
Definition odd := odd.
Definition even_spec := even_spec.
Definition odd_spec := odd_spec.

Program Instance pow_wd : Proper (eq ==>eq ==>eq) pow.
Definition pow_0_r := pow_0_r.
Definition pow_succ_r := pow_succ_r.
Lemma pow_neg_r : forall a b, b <0 -> a ^b = 0.
Definition pow := pow.

Definition square := square.
Definition square_spec := square_spec.

Definition log2_spec := log2_spec.
Definition log2_nonpos := log2_nonpos.
Definition log2 := log2.

Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
Lemma sqrt_neg : forall a, a <0 -> sqrt a = 0.
Definition sqrt := sqrt.

Definition div := div.
Definition modulo := modulo.
Program Instance div_wd : Proper (eq ==>eq ==>eq) div.
Program Instance mod_wd : Proper (eq ==>eq ==>eq) modulo.
Definition div_mod := div_mod.
Definition mod_bound_pos := mod_bound_pos.

Definition divide := divide.
Definition gcd := gcd.
Definition gcd_divide_l := gcd_divide_l.
Definition gcd_divide_r := gcd_divide_r.
Definition gcd_greatest := gcd_greatest.
Lemma gcd_nonneg : forall a b, 0<=gcd a b.

Definition testbit := testbit.
Definition shiftl := shiftl.
Definition shiftr := shiftr.
Definition lxor := lxor.
Definition land := land.
Definition lor := lor.
Definition ldiff := ldiff.
Definition div2 := div2.

Program Instance testbit_wd : Proper (eq ==>eq ==>Logic.eq) testbit.
Definition testbit_odd_0 := testbit_odd_0.
Definition testbit_even_0 := testbit_even_0.
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.
Definition shiftl_spec_low := shiftl_spec_low.
Definition shiftl_spec_high a n m (_:0<=m) := shiftl_spec_high a n m.
Definition shiftr_spec a n m (_:0<=m) := shiftr_spec a n m.
Definition lxor_spec := lxor_spec.
Definition land_spec := land_spec.
Definition lor_spec := lor_spec.
Definition ldiff_spec := ldiff_spec.
Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _.

Generic Properties

Include NProp
<+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.

End Nat.

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.
End TestOrder.

Library Coq.Numbers.Natural.Peano.NPeano

Gcd

Bitwise operations

Implementation of NAxiomsSig by nat

Navigation