diff options
Diffstat (limited to 'theories/Numbers/Natural/BigN/BigN.v')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 198 |
1 files changed, 0 insertions, 198 deletions
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 *) |