From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Numbers/Natural/BigN/BigN.v | 198 -----------------------------------
 1 file changed, 198 deletions(-)
 delete mode 100644 theories/Numbers/Natural/BigN/BigN.v

(limited to 'theories/Numbers/Natural/BigN/BigN.v')

diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
deleted file mode 100644
index e8ff516f..00000000
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ /dev/null
@@ -1,198 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** * Efficient arbitrary large natural numbers in base 2^31 *)
-
-(** Initial Author: Arnaud Spiwack *)
-
-Require Export Int31.
-Require Import CyclicAxioms Cyclic31 Ring31 NSig NSigNAxioms NMake
-  NProperties GenericMinMax.
-
-(** The following [BigN] module regroups both the operations and
-    all the abstract properties:
-
-    - [NMake.Make Int31Cyclic] provides the operations and basic specs
-       w.r.t. ZArith
-    - [NTypeIsNAxioms] shows (mainly) that these operations implement
-      the interface [NAxioms]
-    - [NProp] adds all generic properties derived from [NAxioms]
-    - [MinMax*Properties] provides properties of [min] and [max].
-
-*)
-
-Delimit Scope bigN_scope with bigN.
-
-Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
-  NMake.Make Int31Cyclic
-  <+ NTypeIsNAxioms
-  <+ NBasicProp [no inline] <+ NExtraProp [no inline]
-  <+ HasEqBool2Dec [no inline]
-  <+ MinMaxLogicalProperties [no inline]
-  <+ MinMaxDecProperties [no inline].
-
-(** Notations about [BigN] *)
-
-Local Open Scope bigN_scope.
-
-Notation bigN := BigN.t.
-Bind Scope bigN_scope with bigN BigN.t BigN.t'.
-Arguments BigN.N0 _%int31.
-Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
-Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
-Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
-Infix "+" := BigN.add : bigN_scope.
-Infix "-" := BigN.sub : bigN_scope.
-Infix "*" := BigN.mul : bigN_scope.
-Infix "/" := BigN.div : bigN_scope.
-Infix "^" := BigN.pow : bigN_scope.
-Infix "?=" := BigN.compare : bigN_scope.
-Infix "=?" := BigN.eqb (at level 70, no associativity) : bigN_scope.
-Infix "<=?" := BigN.leb (at level 70, no associativity) : bigN_scope.
-Infix "<?" := BigN.ltb (at level 70, no associativity) : bigN_scope.
-Infix "==" := BigN.eq (at level 70, no associativity) : bigN_scope.
-Notation "x != y" := (~x==y) (at level 70, no associativity) : bigN_scope.
-Infix "<" := BigN.lt : bigN_scope.
-Infix "<=" := BigN.le : bigN_scope.
-Notation "x > y" := (y < x) (only parsing) : bigN_scope.
-Notation "x >= y" := (y <= x) (only parsing) : bigN_scope.
-Notation "x < y < z" := (x<y /\ y<z) : bigN_scope.
-Notation "x < y <= z" := (x<y /\ y<=z) : bigN_scope.
-Notation "x <= y < z" := (x<=y /\ y<z) : bigN_scope.
-Notation "x <= y <= z" := (x<=y /\ y<=z) : bigN_scope.
-Notation "[ i ]" := (BigN.to_Z i) : bigN_scope.
-Infix "mod" := BigN.modulo (at level 40, no associativity) : bigN_scope.
-
-(** Example of reasoning about [BigN] *)
-
-Theorem succ_pred: forall q : bigN,
-  0 < q -> BigN.succ (BigN.pred q) == q.
-Proof.
-intros; apply BigN.succ_pred.
-intro H'; rewrite H' in H; discriminate.
-Qed.
-
-(** [BigN] is a semi-ring *)
-
-Lemma BigNring : semi_ring_theory 0 1 BigN.add BigN.mul BigN.eq.
-Proof.
-constructor.
-exact BigN.add_0_l. exact BigN.add_comm. exact BigN.add_assoc.
-exact BigN.mul_1_l. exact BigN.mul_0_l. exact BigN.mul_comm.
-exact BigN.mul_assoc. exact BigN.mul_add_distr_r.
-Qed.
-
-Lemma BigNeqb_correct : forall x y, (x =? y) = true -> x==y.
-Proof. now apply BigN.eqb_eq. Qed.
-
-Lemma BigNpower : power_theory 1 BigN.mul BigN.eq BigN.of_N BigN.pow.
-Proof.
-constructor.
-intros. red. rewrite BigN.spec_pow, BigN.spec_of_N.
-rewrite Zpower_theory.(rpow_pow_N).
-destruct n; simpl. reflexivity.
-induction p; simpl; intros; BigN.zify; rewrite ?IHp; auto.
-Qed.
-
-Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
- (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
-Proof.
-constructor. unfold id. intros a b.
-BigN.zify.
-case Z.eqb_spec.
-BigN.zify. auto with zarith.
-intros NEQ.
-generalize (BigN.spec_div_eucl a b).
-generalize (Z_div_mod_full [a] [b] NEQ).
-destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1 as EQr EQq.
-BigN.zify. rewrite EQr, EQq; auto.
-Qed.
-
-
-(** Detection of constants *)
-
-Ltac isStaticWordCst t :=
- match t with
- | W0 => constr:(true)
- | WW ?t1 ?t2 =>
-   match isStaticWordCst t1 with
-   | false => constr:(false)
-   | true => isStaticWordCst t2
-   end
- | _ => isInt31cst t
- end.
-
-Ltac isBigNcst t :=
- match t with
- | BigN.N0 ?t => isStaticWordCst t
- | BigN.N1 ?t => isStaticWordCst t
- | BigN.N2 ?t => isStaticWordCst t
- | BigN.N3 ?t => isStaticWordCst t
- | BigN.N4 ?t => isStaticWordCst t
- | BigN.N5 ?t => isStaticWordCst t
- | BigN.N6 ?t => isStaticWordCst t
- | BigN.Nn ?n ?t => match isnatcst n with
-   | true => isStaticWordCst t
-   | false => constr:(false)
-   end
- | BigN.zero => constr:(true)
- | BigN.one => constr:(true)
- | BigN.two => constr:(true)
- | _ => constr:(false)
- end.
-
-Ltac BigNcst t :=
- match isBigNcst t with
- | true => constr:(t)
- | false => constr:(NotConstant)
- end.
-
-Ltac BigN_to_N t :=
- match isBigNcst t with
- | true => eval vm_compute in (BigN.to_N t)
- | false => constr:(NotConstant)
- end.
-
-Ltac Ncst t :=
- match isNcst t with
- | true => constr:(t)
- | false => constr:(NotConstant)
- end.
-
-(** Registration for the "ring" tactic *)
-
-Add Ring BigNr : BigNring
- (decidable BigNeqb_correct,
-  constants [BigNcst],
-  power_tac BigNpower [BigN_to_N],
-  div BigNdiv).
-
-Section TestRing.
-Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
-intros. ring_simplify. reflexivity.
-Qed.
-End TestRing.
-
-(** We benefit also from an "order" tactic *)
-
-Ltac bigN_order := BigN.order.
-
-Section TestOrder.
-Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
-Proof. bigN_order. Qed.
-End TestOrder.
-
-(** We can use at least a bit of (r)omega by translating to [Z]. *)
-
-Section TestOmega.
-Let test : forall x y : bigN, x<=y -> y<=x -> x==y.
-Proof. intros x y. BigN.zify. omega. Qed.
-End TestOmega.
-
-(** Todo: micromega *)
-- 
cgit v1.2.3