(************************************************************************)
(*         *   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.
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.
Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
Program Instance div_wd : Proper (eq==>eq==>eq) div.
Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
Program 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.
Proof.
intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
Qed.

(** 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.
Proof.
intros a a' Ha f f' Hf n n' Hn. subst n'.
induction n; simpl; auto. apply Hf; auto.
Qed.

Theorem recursion_0 :
  forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a.
Proof.
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)).
Proof.
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.
Proof.
reflexivity.
Qed.

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

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

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

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

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

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

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

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

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

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

(** ** Boolean comparisons *)

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

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

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

(** ** Decidability of equality over [nat]. *)

Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.
Proof.
  induction n; destruct m.
  - now left.
  - now right.
  - now right.
  - 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.
Proof.
 revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy.
Qed.

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

Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
Proof.
 revert m; induction n; destruct m; simpl; rewrite ?IHn.
 - now split.
 - split; intros. apply Peano.le_0_n. easy.
 - split. now destruct 1. inversion 1.
 - split; intros. now apply Peano.le_n_S. now apply Peano.le_S_n.
Qed.

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

Lemma compare_succ n m : (S n ?= S m) = (n ?= m).
Proof.
 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.
Proof.
 exact Peano.max_l.
Qed.

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

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

Lemma min_r : forall n m, m <= n -> min n m = m.
Proof.
 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. inversion 1. Qed.

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

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

(** ** Square *)

Lemma square_spec n : square n = n * n.
Proof. 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.
Proof.
 intros ([|], H); try discriminate.
 simpl in H. now rewrite <- plus_n_Sm in H.
Qed.

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

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

Lemma Odd_2 n : Odd n <-> Odd (S (S n)).
Proof.
 split; intros (m,H).
 - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m).
 - destruct m; try discriminate.
   exists m. simpl in H. rewrite <- plus_n_Sm in H. inversion H.
   simpl. 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.
Proof.
 fix even_spec 1.
  destruct n as [|[|n]]; simpl.
  - split; [ now exists 0 | trivial ].
  - split; [ discriminate | intro H; elim (Even_1 H) ].
  - rewrite even_spec. apply Even_2.
Qed.

Lemma odd_spec : forall n, odd n = true <-> Odd n.
Proof.
 unfold odd.
 fix odd_spec 1.
  destruct n as [|[|n]]; simpl.
  - split; [ discriminate | intro H; elim (Odd_0 H) ].
  - split; [ now exists 0 | trivial ].
  - rewrite odd_spec. 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.
Proof.
 induction x.
 - simpl; intuition.
 - intros y q u H. destruct u; simpl divmod.
   + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u').
     intros (EQ,LE); split; trivial.
     rewrite <- EQ, sub_0_r, sub_diag, add_0_r.
     now rewrite !add_succ_l, <- add_succ_r, <- add_assoc, mul_succ_r.
   + assert (H' : u <= y).
     { apply le_trans with (S u); trivial. do 2 constructor. }
     generalize (IHx y q u H'). destruct divmod as (q',u').
     intros (EQ,LE); split; trivial.
     rewrite <- EQ.
     rewrite !add_succ_l, <- add_succ_r. f_equal. now rewrite <- sub_succ_l.
Qed.

Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y.
Proof.
 intros Hy.
 destruct y; [ now elim Hy | clear Hy ].
 unfold div, modulo.
 generalize (divmod_spec x y 0 y (le_n y)).
 destruct divmod as (q,u).
 intros (U,V).
 simpl in *.
 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.
Proof.
 intros Hx Hy. split. apply le_0_l.
 destruct y; [ now elim Hy | clear Hy ].
 unfold modulo.
 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).
Proof.
 induction k.
 - (* k = 0 *)
   simpl; intros p q r Hq Hr.
   split.
   + apply le_add_r.
   + apply lt_succ_r.
     rewrite mul_succ_r.
     rewrite add_assoc, (add_comm p), <- add_assoc.
     apply add_le_mono_l.
     rewrite <- Hq. apply le_sub_l.
 - (* k = S k' *)
   destruct r.
   + (* r = 0 *)
     intros Hq _.
     replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))).
     * apply IHk.
       simpl. now rewrite add_succ_r, Hq. apply le_n.
     * rewrite sub_diag, sub_0_r, add_0_r. simpl.
       rewrite add_succ_r; f_equal. rewrite <- add_assoc; f_equal.
       rewrite mul_succ_r, (add_comm p), <- add_assoc. now f_equal.
   + (* r = S r' *)
     intros Hq Hr.
     replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)).
     * apply IHk; trivial. apply le_trans with (S r); trivial. do 2 constructor.
     * simpl. rewrite <- add_succ_r. f_equal. rewrite <- sub_succ_l; trivial.
Qed.

Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).
Proof.
 set (s:=sqrt n).
 replace n with (n + 0*0 + (0-0)).
 apply sqrt_iter_spec; auto.
 simpl. 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.
Proof. 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).
Proof.
 induction k.
 - (* k = 0 *)
   intros p q r EQ LT. simpl log2_iter. cbv zeta.
   split.
   + rewrite add_0_l.
     rewrite (add_le_mono_l _ _ (2^p)).
     simpl pow in EQ. rewrite add_0_r in EQ. rewrite EQ.
     rewrite add_comm. apply add_le_mono_r. apply LT.
   + rewrite EQ, add_comm. apply add_lt_mono_l.
     apply lt_succ_r, le_0_l.
 - (* k = S k' *)
   intros p q r EQ LT. destruct r.
   + (* r = 0 *)
     rewrite add_succ_r, add_0_r in EQ.
     rewrite add_succ_l, <- add_succ_r. apply IHk.
     * rewrite <- EQ. remember (S p) as p'; simpl. now rewrite add_0_r.
     * rewrite EQ. constructor.
   + (* r = S r' *)
     rewrite add_succ_l, <- add_succ_r. apply IHk.
     * now rewrite add_succ_l, <- add_succ_r.
     * apply le_lt_trans with (S r); trivial. do 2 constructor.
Qed.

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

Lemma log2_nonpos n : n<=0 -> log2 n = 0.
Proof.
 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).
Proof.
 fix gcd_divide 1.
 intros [|a] b; simpl.
 split.
  now exists 0.
  exists 1. simpl. now rewrite <- plus_n_O.
 fold (b mod (S a)).
 destruct (gcd_divide (b mod (S a)) (S a)) as (H,H').
 set (a':=S a) in *.
 split; auto.
 rewrite (div_mod b a') at 2 by discriminate.
 destruct H as (u,Hu), H' as (v,Hv).
 rewrite mul_comm.
 exists ((b/a')*v + u).
 rewrite mul_add_distr_r.
 now rewrite <- mul_assoc, <- Hv, <- Hu.
Qed.

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

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

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

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


(** ** Bitwise operations *)

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

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

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

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

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

Lemma double_twice : forall n, double n = 2*n.
Proof.
 simpl; intros. now rewrite add_0_r.
Qed.

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

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

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

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

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

Lemma shiftr_specif : forall a n m,
 testbit (shiftr a n) m = testbit a (m+n).
Proof.
 induction n; intros m. trivial.
 now rewrite add_0_r.
 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).
Proof.
 induction n; intros m H. trivial.
 now rewrite sub_0_r.
 destruct m. inversion H.
 simpl. apply succ_le_mono in H.
 change (shiftl a (S n)) with (double (shiftl a n)).
 rewrite double_twice, div2_double. now apply IHn.
Qed.

Lemma shiftl_spec_low : forall a n m, m<n ->
 testbit (shiftl a n) m = false.
Proof.
 induction n; intros m H. inversion H.
 change (shiftl a (S n)) with (double (shiftl a n)).
 destruct m; simpl.
 unfold odd. apply negb_false_iff.
 apply even_spec. exists (shiftl a n). apply double_twice.
 rewrite double_twice, div2_double. apply IHn.
 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).
Proof.
 intros. unfold bitwise; fold bitwise.
 destruct (op (odd a) (odd b)).
 now rewrite div2_succ_double.
 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).
Proof.
 intros. unfold bitwise; fold bitwise.
 destruct (op (odd a) (odd b)).
 apply odd_spec. rewrite add_comm. eexists; eauto.
 unfold odd. apply negb_false_iff. apply even_spec.
 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).
Proof.
 intros op Hop.
 induction n; intros m a b Ha.
 simpl. inversion Ha; subst. now rewrite testbit_0_l.
 destruct m.
 apply odd_bitwise.
 unfold testbit; fold testbit. rewrite div2_bitwise.
 apply IHn. 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).
Proof.
 intros op Hop.
 induction n; intros m a b Ha Hb.
 simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l.
 destruct m.
 apply odd_bitwise.
 unfold testbit; fold testbit. rewrite div2_bitwise.
 apply IHn; now apply div2_decr.
Qed.

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

Lemma ldiff_spec a b n :
 testbit (ldiff a b) n = testbit a n && negb (testbit b n).
Proof.
 unfold ldiff. apply testbit_bitwise_1; trivial.
Qed.

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

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

Lemma div2_spec a : div2 a = shiftr a 1.
Proof.
 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.
Proof. 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.
Proof.
 revert m. induction n as [|n IH]; simpl; trivial.
 intros. now rewrite IH, add_succ_r.
Qed.

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

Lemma tail_mul_spec n m : tail_mul n m = n * m.
Proof.
 unfold tail_mul. 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.
 Proof.
 Nat.order.
 Qed.
End TestOrder.