From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/Numbers/Natural/Binary/NBinary.v | 141 +-----------------------------
 1 file changed, 3 insertions(+), 138 deletions(-)

(limited to 'theories/Numbers/Natural/Binary')

diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 029fdfca..43ca67dd 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,150 +8,15 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NBinary.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 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.
+(** * [BinNat.N] already implements [NAxiomSig] *)
 
-Module Export NBinaryPropMod := NPropFunct NBinaryAxiomsMod.
+Module N <: NAxiomsSig := N.
 
 (*
 Require Import NDefOps.
-- 
cgit v1.2.3