diff options
Diffstat (limited to 'theories/Numbers/Natural/Binary')
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinDefs.v | 267 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 173 |
2 files changed, 170 insertions, 270 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v deleted file mode 100644 index fc2bd2df..00000000 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ /dev/null @@ -1,267 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* Evgeny Makarov, INRIA, 2007 *) -(************************************************************************) - -(*i $Id: NBinDefs.v 11040 2008-06-03 00:04:16Z letouzey $ i*) - -Require Import BinPos. -Require Export BinNat. -Require Import NSub. - -Open Local Scope N_scope. - -(** Implementation of [NAxiomsSig] module type via [BinNat.N] *) - -Module NBinaryAxiomsMod <: NAxiomsSig. -Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. -Module Export NZAxiomsMod <: NZAxiomsSig. - -Definition NZ := N. -Definition NZeq := @eq N. -Definition NZ0 := N0. -Definition NZsucc := Nsucc. -Definition NZpred := Npred. -Definition NZadd := Nplus. -Definition NZsub := Nminus. -Definition NZmul := Nmult. - -Theorem NZeq_equiv : equiv N NZeq. -Proof (eq_equiv N). - -Add Relation N NZeq - reflexivity proved by (proj1 NZeq_equiv) - symmetry proved by (proj2 (proj2 NZeq_equiv)) - transitivity proved by (proj1 (proj2 NZeq_equiv)) -as NZeq_rel. - -Add Morphism NZsucc with signature NZeq ==> NZeq as NZsucc_wd. -Proof. -congruence. -Qed. - -Add Morphism NZpred with signature NZeq ==> NZeq as NZpred_wd. -Proof. -congruence. -Qed. - -Add Morphism NZadd with signature NZeq ==> NZeq ==> NZeq as NZadd_wd. -Proof. -congruence. -Qed. - -Add Morphism NZsub with signature NZeq ==> NZeq ==> NZeq as NZsub_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmul with signature NZeq ==> NZeq ==> NZeq as NZmul_wd. -Proof. -congruence. -Qed. - -Theorem NZinduction : - forall A : NZ -> Prop, predicate_wd NZeq A -> - A N0 -> (forall n, A n <-> A (NZsucc n)) -> forall n : NZ, A n. -Proof. -intros A A_wd A0 AS. apply Nrect. assumption. intros; now apply -> AS. -Qed. - -Theorem NZpred_succ : forall n : NZ, NZpred (NZsucc n) = n. -Proof. -destruct n as [| p]; simpl. reflexivity. -case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ). -intro H; false_hyp H Psucc_not_one. -Qed. - -Theorem NZadd_0_l : forall n : NZ, N0 + n = n. -Proof. -reflexivity. -Qed. - -Theorem NZadd_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m). -Proof. -destruct n; destruct m. -simpl in |- *; reflexivity. -unfold NZsucc, NZadd, Nsucc, Nplus. rewrite <- Pplus_one_succ_l; reflexivity. -simpl in |- *; reflexivity. -simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. -Qed. - -Theorem NZsub_0_r : forall n : NZ, n - N0 = n. -Proof. -now destruct n. -Qed. - -Theorem NZsub_succ_r : forall n m : NZ, n - (NZsucc m) = NZpred (n - m). -Proof. -destruct n as [| p]; destruct m as [| q]; try reflexivity. -now destruct p. -simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. -now destruct (Pminus_mask p q) as [| r |]; [| destruct r |]. -Qed. - -Theorem NZmul_0_l : forall n : NZ, N0 * n = N0. -Proof. -destruct n; reflexivity. -Qed. - -Theorem NZmul_succ_l : forall n m : NZ, (NZsucc n) * m = n * m + m. -Proof. -destruct n as [| n]; destruct m as [| m]; simpl; try reflexivity. -now rewrite Pmult_Sn_m, Pplus_comm. -Qed. - -End NZAxiomsMod. - -Definition NZlt := Nlt. -Definition NZle := Nle. -Definition NZmin := Nmin. -Definition NZmax := Nmax. - -Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. -Proof. -unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZle with signature NZeq ==> NZeq ==> iff as NZle_wd. -Proof. -unfold NZeq; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism NZmin with signature NZeq ==> NZeq ==> NZeq as NZmin_wd. -Proof. -congruence. -Qed. - -Add Morphism NZmax with signature NZeq ==> NZeq ==> NZeq as NZmax_wd. -Proof. -congruence. -Qed. - -Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m. -Proof. -intros n m. unfold Nle, Nlt. rewrite <- Ncompare_eq_correct. -destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now right. -now elim H1. destruct H1; discriminate. -Qed. - -Theorem NZlt_irrefl : forall n : NZ, ~ n < n. -Proof. -intro n; unfold Nlt; now rewrite Ncompare_refl. -Qed. - -Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc 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. elimtype False; 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. elimtype False; now apply H. -Qed. - -Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n. -Proof. -unfold NZmin, Nmin, Nle; intros n m H. -destruct (n ?= m); try reflexivity. now elim H. -Qed. - -Theorem NZmin_r : forall n m : N, m <= n -> NZmin n m = m. -Proof. -unfold NZmin, 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 NZmax_l : forall n m : N, m <= n -> NZmax n m = n. -Proof. -unfold NZmax, 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 NZmax_r : forall n m : N, n <= m -> NZmax n m = m. -Proof. -unfold NZmax, Nmax, Nle; intros n m H. -destruct (n ?= m); try reflexivity. now elim H. -Qed. - -End NZOrdAxiomsMod. - -Definition recursion (A : Type) (a : A) (f : N -> A -> A) (n : N) := - Nrect (fun _ => A) a f n. -Implicit Arguments recursion [A]. - -Theorem pred_0 : Npred N0 = N0. -Proof. -reflexivity. -Qed. - -Theorem recursion_wd : -forall (A : Type) (Aeq : relation A), - forall a a' : A, Aeq a a' -> - forall f f' : N -> A -> A, fun2_eq NZeq Aeq Aeq f f' -> - forall x x' : N, x = x' -> - Aeq (recursion a f x) (recursion a' f' x'). -Proof. -unfold fun2_wd, NZeq, fun2_eq. -intros A Aeq 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 -> fun2_wd NZeq Aeq Aeq f -> - forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)). -Proof. -unfold NZeq, recursion, fun2_wd; 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. - -End NBinaryAxiomsMod. - -Module Export NBinarySubPropMod := NSubPropFunct 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 compute in (log 100000). *) (* 98 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. -*) -(* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *) - 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 *) + +*) |