# Library CoLoR.Util.Nat.NatUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-04-02
• Frederic Blanqui, 2009-05-11
useful definitions and lemmas on natural numbers

Set Implicit Arguments.

Declare implicit arguments.

Tactics.

Ltac coq_omega := omega.
Tactic Notation "omega" := intros; omega.
Tactic Notation "lia" := intros; lia.
Tactic Notation "nia" := intros; nia.

Ltac max :=
match goal with
| |- context [max ?x ?y] => gen (le_max_l x y); gen (le_max_r x y)
end; omega.

Properties of ordering relations on nat.

Instance le_preorder : PreOrder le.

Instance lt_trans : Transitive lt.

Instance ge_preorder : PreOrder ge.

Instance gt_trans : Transitive gt.

Boolean function for equality.

Fixpoint beq_nat (x y : nat) :=
match x, y with
| 0, 0 => true
| S x', S y' => beq_nat x' y'
| _, _ => false
end.

Lemma beq_nat_ok : forall x y, beq_nat x y = true <-> x = y.

Ltac case_beq_nat := case_beq beq_nat beq_nat_ok.

Lemma eq_nat_dec_refl : forall n, eq_nat_dec n n = left (n<>n) (eq_refl n).

Boolean functions for orderings.

Fixpoint bgt_nat (x y : nat) :=
match x, y with
| 0, _ => false
| S _, 0 => true
| S x', S y' => bgt_nat x' y'
end.

Lemma bgt_nat_ok : forall x y, bgt_nat x y = true <-> x > y.

Ltac check_gt := rewrite <- bgt_nat_ok; check_eq.

Lemma bgt_nat_ko : forall x y, bgt_nat x y = false <-> x <= y.

Fixpoint bge_nat (x y : nat) :=
match x, y with
| 0, 0 => true
| 0, _ => false
| S _, 0 => true
| S x', S y' => bge_nat x' y'
end.

Lemma bge_nat_ok : forall x y, bge_nat x y = true <-> x >= y.

Ltac check_ge := rewrite <- bge_nat_ok; check_eq.

Definition blt_nat x y := bgt_nat y x.

Lemma blt_nat_ok : forall x y, blt_nat x y = true <-> x < y.

Definition bne_nat x y := negb (beq_nat x y).

Lemma bne_nat_ok : forall x y, bne_nat x y = true <-> x <> y.

Unicity of equality and ordering proofs on nat.

Lemma eq_unique : forall (n m : nat) (h1 h2 : n = m), h1 = h2.

Scheme le_ind_dep := Induction for le Sort Prop.

Lemma le_unique : forall n m (h1 h2 : n <= m), h1 = h2.

Lemma lt_unique : forall n m (h1 h2 : n < m), h1 = h2.

Lemma lt_Sn_nS : forall m n (H : m < n), lt_S_n (lt_n_S H) = H.

Lemma lt_nS_Sn : forall m n (H : S m < S n), lt_n_S (lt_S_n H) = H.

Lemmas on the maximum of two numbers.

Lemma max_assoc : forall a b c, max a (max b c) = max (max a b) c.

Lemma le_max_intro_l x y z : x <= y -> x <= max y z.

Lemma lt_max_intro_l x y z : x < y -> x < max y z.

Lemma le_max_intro_r x y z : x <= z -> x <= max y z.

Lemma lt_max_intro_r x y z : x < z -> x < max y z.

Lemma le_max_elim_l x y z : max x y <= z -> x <= z.

Lemma le_max_elim_r x y z : max x y <= z -> y <= z.

Lemma max_ge_compat x y x' y' : x >= x' -> y >= y' -> max x y >= max x' y'.

Lemma max_gt_compat x y x' y' : x > x' -> y > y' -> max x y > max x' y'.

Lemma min_gt_compat x y x' y' : x > x' -> y > y' -> min x y > min x' y'.

Lemma max_lt x y z : max y z < x <-> y < x /\ z < x.

Lemma gt_max x y z : x > max y z <-> x > y /\ x > z.

Lemma max_0_r x : max x 0 = x.

Lemmas on the minimum of two numbers.

Lemma elim_min_l x y z : x <= z -> min x y <= z.

Lemma elim_min_r : forall x y z, y <= z -> min x y <= z.

Lemma lt_min_intro_l x y z : x < z -> min x y < z.

Lemma lt_min_intro_r x y z : y < z -> min x y < z.

Lemma le_min_intro_l x y z : x <= z -> min x y <= z.

Lemma le_min_intro_r x y z : y <= z -> min x y <= z.

Lemma min_ge_compat x y x' y' : x >= x' -> y >= y' -> min x y >= min x' y'.

Decidability of ordering relations on nat.

Lemma ge_dec : rel_dec ge.

Lemma gt_dec : rel_dec gt.

Lemma lt_ge_dec x y : {x < y} + {x >= y}.

Euclidian division.

Lemma mult_is_not_O m n : m * n <> 0 <-> m <> 0 /\ n <> 0.

Lemma mult_lt_r_elim : forall x x' y, x * y < x' * y -> x < x'.

Lemma eucl_div_unique b q1 r1 q2 r2 :
b > r1 -> b > r2 -> q1 * b + r1 = q2 * b + r2 -> q1 = q2 /\ r1 = r2.

Iteration of a function.

Section iter.

Variables (A : Type) (a : A) (f : A -> A).

Fixpoint iter i :=
match i with
| 0 => a
| S i' => f (iter i')
end.

End iter.

Section iter_prop.

Variables (A : Type) (f : A -> A).

Lemma iter_com : forall a i, iter (f a) f i = f (iter a f i).

Lemma red_iter : forall R : relation A,
(forall x y, R x y -> R (f x) (f y)) ->
forall i x y, R x y -> R (iter x f i) (iter y f i).

End iter_prop.

Arithmetical lemmas.

Lemma le_plus : forall x y, x <= y -> exists k, y = k + x.

Lemma le_lt_S : forall i k, i <= k -> i < S k.

Lemma i_lt_n : forall n i j : nat, n = i + S j -> i < n.

Lemma S_neq_O : forall n, S n = O -> False.

Lemma plus_reg_l_inv : forall n1 n2 p2, n2=p2 -> n1+n2=n1+p2.

Lemma plus_reg_r_inv : forall n1 p1 n2, n1=p1 -> n1+n2=p1+n2.

Lemma plus_minus_eq : forall v p, v+p-p=v.

Lemma le_minus_plus : forall v p, p<=v -> v-p+p=v.

Lemma plus_1_S : forall n, n+1 = S n.

Lemma lt_from_le : forall x y, 0 < y -> x <= y-1 -> x < y.

Lemma le_from_lt : forall x y, x < y+1 -> x <= y.

Lemma lt_pm : forall n k x, n < x -> x <= n+k -> x-n-1 < k.

Lemma le_plus_r : forall k l, k <= k+l.

Lemma misc1 : forall x k, S k = x+2+k-x-1.

Lemma misc2 : forall x k, k = x+2+k-(x+1)-1.

Lemma mult_gt_0 : forall i j, i > 0 -> j > 0 -> i * j > 0.

Lemma mult_lt_compat_lr : forall i j k l,
i <= j -> j > 0 -> k < l -> i * k < j * l.

Lemma S_add_S : forall n1 n2 n, n1 + S n2 = n -> S n1 + S n2 = S n.

Lemma gt_plus : forall l k, l > k -> exists m, l = (m + 1) + k.

Given a non-null function F, Interval_list F i is the pair (S(i),S(i+1) where S(0)=0 and S(i+1)=S(i)+F(i).

Section Interval_list.

Variables (F : nat -> nat) (HFi : forall i, exists y, F i = S y).

Fixpoint Interval_list i : nat * nat :=
match i with
| 0 => (0, F 0)
| S i' => let x := snd (Interval_list i') in (x, x + F i)
end.

Lemma int_exPi : forall i, exists j, fst (F' j) <= i /\ i < snd (F' j).

End Interval_list.

Monotone functions on nat.

Section mon.

Variables (A : Type) (ltA : relation A) (ht : transitive ltA) (f : nat->A).

Lemma monS : (forall x, ltA (f x) (f (S x)))
-> (forall x y, x < y -> ltA (f x) (f y)).

End mon.

Smallest natural number satisfying some satisfiable property.

Section smallest.

Variables (P : nat -> Prop) (P_dec : forall x, {P x}+{~P x}).

Section smallest_aux.

Variables (n : nat) (h : P n).

Fixpoint smallest_aux acc k :=
match k with
| 0 => if P_dec k then 0 else acc
| S k' => smallest_aux (if P_dec k then k else acc) k'
end.

Definition smallest := smallest_aux n n.

Lemma smallest_aux_ok : forall k acc, P acc -> P (smallest_aux acc k).

Lemma smallest_ok : P smallest.

Lemma smallest_aux_le_max_args l :
forall k acc, acc <= l -> k <= l -> smallest_aux acc k <= l.

Lemma smallest_le_arg : smallest <= n.

Lemma smallest_aux_plus_exists m :
forall k acc, exists acc', smallest_aux acc (k + m) = smallest_aux acc' m.

Lemma smallest_aux_plus m : P (S m) ->
forall k acc acc', smallest_aux acc (k + S m) = smallest_aux acc' (S m).

Lemma smallest_aux_le_exists k l acc :
k <= l -> exists acc', smallest_aux acc l = smallest_aux acc' k.

Lemma smallest_aux_le k l acc acc' :
k <= l -> P (S k) -> smallest_aux acc (S l) = smallest_aux acc' (S k).

End smallest_aux.

Lemma smallest_inv_le k l : k <= l -> P k -> smallest l = smallest k.

Lemma smallest_inv m n : P m -> P n -> smallest m = smallest n.

Lemma smallest_comp m n : P m -> P n -> smallest m <= n.

End smallest.