diff options
Diffstat (limited to 'theories/Numbers/Natural/Binary/NBinary.v')
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 173 |
1 files changed, 170 insertions, 3 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 2c99128d..e593f4a5 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -8,8 +8,175 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NBinary.v 10934 2008-05-15 21:58:20Z letouzey $ i*) +(*i $Id$ i*) -Require Export NBinDefs. -Require Export NArithRing. +Require Import BinPos. +Require Export BinNat. +Require Import NAxioms NProperties. +Local Open Scope N_scope. + +(** * Implementation of [NAxiomsSig] module type via [BinNat.N] *) + +Module NBinaryAxiomsMod <: NAxiomsSig. + +(** Bi-directional induction. *) + +Theorem bi_induction : + forall A : N -> Prop, Proper (eq==>iff) A -> + A N0 -> (forall n, A n <-> A (Nsucc n)) -> forall n : N, A n. +Proof. +intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS. +Qed. + +(** Basic operations. *) + +Definition eq_equiv : Equivalence (@eq N) := eq_equivalence. +Local Obligation Tactic := simpl_relation. +Program Instance succ_wd : Proper (eq==>eq) Nsucc. +Program Instance pred_wd : Proper (eq==>eq) Npred. +Program Instance add_wd : Proper (eq==>eq==>eq) Nplus. +Program Instance sub_wd : Proper (eq==>eq==>eq) Nminus. +Program Instance mul_wd : Proper (eq==>eq==>eq) Nmult. + +Definition pred_succ := Npred_succ. +Definition add_0_l := Nplus_0_l. +Definition add_succ_l := Nplus_succ. +Definition sub_0_r := Nminus_0_r. +Definition sub_succ_r := Nminus_succ_r. +Definition mul_0_l := Nmult_0_l. +Definition mul_succ_l n m := eq_trans (Nmult_Sn_m n m) (Nplus_comm _ _). + +(** Order *) + +Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt. + +Definition lt_eq_cases := Nle_lteq. +Definition lt_irrefl := Nlt_irrefl. + +Theorem lt_succ_r : forall n m, n < (Nsucc m) <-> n <= m. +Proof. +intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl; +split; intro H; try reflexivity; try discriminate. +destruct p; simpl; intros; discriminate. exfalso; now apply H. +apply -> Pcompare_p_Sq in H. destruct H as [H | H]. +now rewrite H. now rewrite H, Pcompare_refl. +apply <- Pcompare_p_Sq. case_eq ((p ?= q)%positive Eq); intro H1. +right; now apply Pcompare_Eq_eq. now left. exfalso; now apply H. +Qed. + +Theorem min_l : forall n m, n <= m -> Nmin n m = n. +Proof. +unfold Nmin, Nle; intros n m H. +destruct (n ?= m); try reflexivity. now elim H. +Qed. + +Theorem min_r : forall n m, m <= n -> Nmin n m = m. +Proof. +unfold Nmin, Nle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +now apply -> Ncompare_eq_correct. +rewrite <- Ncompare_antisym, H1 in H; elim H; auto. +Qed. + +Theorem max_l : forall n m, m <= n -> Nmax n m = n. +Proof. +unfold Nmax, Nle; intros n m H. +case_eq (n ?= m); intro H1; try reflexivity. +symmetry; now apply -> Ncompare_eq_correct. +rewrite <- Ncompare_antisym, H1 in H; elim H; auto. +Qed. + +Theorem max_r : forall n m : N, n <= m -> Nmax n m = m. +Proof. +unfold Nmax, Nle; intros n m H. +destruct (n ?= m); try reflexivity. now elim H. +Qed. + +(** Part specific to natural numbers, not integers. *) + +Theorem pred_0 : Npred 0 = 0. +Proof. +reflexivity. +Qed. + +Definition recursion (A : Type) : A -> (N -> A -> A) -> N -> A := + Nrect (fun _ => A). +Implicit Arguments recursion [A]. + +Instance recursion_wd A (Aeq : relation A) : + Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A). +Proof. +intros a a' Eaa' f f' Eff'. +intro x; pattern x; apply Nrect. +intros x' H; now rewrite <- H. +clear x. +intros x IH x' H; rewrite <- H. +unfold recursion in *. do 2 rewrite Nrect_step. +now apply Eff'; [| apply IH]. +Qed. + +Theorem recursion_0 : + forall (A : Type) (a : A) (f : N -> A -> A), recursion a f N0 = a. +Proof. +intros A a f; unfold recursion; now rewrite Nrect_base. +Qed. + +Theorem recursion_succ : + forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A), + Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> + forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)). +Proof. +unfold recursion; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect. +rewrite Nrect_step; rewrite Nrect_base; now apply f_wd. +clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|]. +now rewrite Nrect_step. +Qed. + +(** The instantiation of operations. + Placing them at the very end avoids having indirections in above lemmas. *) + +Definition t := N. +Definition eq := @eq N. +Definition zero := N0. +Definition succ := Nsucc. +Definition pred := Npred. +Definition add := Nplus. +Definition sub := Nminus. +Definition mul := Nmult. +Definition lt := Nlt. +Definition le := Nle. +Definition min := Nmin. +Definition max := Nmax. + +End NBinaryAxiomsMod. + +Module Export NBinaryPropMod := NPropFunct NBinaryAxiomsMod. + +(* +Require Import NDefOps. +Module Import NBinaryDefOpsMod := NdefOpsPropFunct NBinaryAxiomsMod. + +(* Some fun comparing the efficiency of the generic log defined +by strong (course-of-value) recursion and the log defined by recursion +on notation *) + +Time Eval vm_compute in (log 500000). (* 11 sec *) + +Fixpoint binposlog (p : positive) : N := +match p with +| xH => 0 +| xO p' => Nsucc (binposlog p') +| xI p' => Nsucc (binposlog p') +end. + +Definition binlog (n : N) : N := +match n with +| 0 => 0 +| Npos p => binposlog p +end. + +Time Eval vm_compute in (binlog 500000). (* 0 sec *) +Time Eval vm_compute in (binlog 1000000000000000000000000000000). (* 0 sec *) + +*) |