diff options
Diffstat (limited to 'theories/Arith/PeanoNat.v')
| -rw-r--r-- | theories/Arith/PeanoNat.v | 755 |
1 files changed, 755 insertions, 0 deletions
diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v new file mode 100644 index 00000000..799031a2 --- /dev/null +++ b/theories/Arith/PeanoNat.v @@ -0,0 +1,755 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* 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 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 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 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 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 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. + +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. |