diff options
Diffstat (limited to 'theories/Numbers')
21 files changed, 74 insertions, 161 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v index b73410256..05b8ede94 100644 --- a/theories/Numbers/Integer/Axioms/ZAxioms.v +++ b/theories/Numbers/Integer/Axioms/ZAxioms.v @@ -1,5 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. +Require Export ZDomain. Module Type IntSignature. Declare Module Export DomainModule : DomainSignature. @@ -25,7 +24,6 @@ Axiom induction : End IntSignature. - Module IntProperties (Export IntModule : IntSignature). Module Export DomainPropertiesModule := DomainProperties DomainModule. Open Local Scope ZScope. diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v index b48684ba8..1a29eddf2 100644 --- a/theories/Numbers/Integer/Axioms/ZDomain.v +++ b/theories/Numbers/Integer/Axioms/ZDomain.v @@ -1,4 +1,4 @@ -Require Import NumPrelude. +Require Export NumPrelude. Module Type DomainSignature. diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v index 3bf4d61f5..803bfe43b 100644 --- a/theories/Numbers/Integer/Axioms/ZOrder.v +++ b/theories/Numbers/Integer/Axioms/ZOrder.v @@ -1,6 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. -Require Import ZAxioms. +Require Export ZAxioms. Module Type OrderSignature. Declare Module Export IntModule : IntSignature. diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v index f455400b7..484607094 100644 --- a/theories/Numbers/Integer/Axioms/ZPlus.v +++ b/theories/Numbers/Integer/Axioms/ZPlus.v @@ -1,6 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. -Require Import ZAxioms. +Require Export ZAxioms. Module Type PlusSignature. Declare Module Export IntModule : IntSignature. diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v index 4f677355b..dd311b49a 100644 --- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v +++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v @@ -1,8 +1,8 @@ -Require Import ZOrder. -Require Import ZPlus. +Require Export ZOrder. +Require Export ZPlus. -Module PlusOrderProperties (Export PlusModule : PlusSignature) - (Export OrderModule : OrderSignature with +Module PlusOrderProperties (PlusModule : PlusSignature) + (OrderModule : OrderSignature with Module IntModule := PlusModule.IntModule). (* Warning: Notation _ == _ was already used in scope ZScope !!! *) Module Export PlusPropertiesModule := PlusProperties PlusModule. diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v index ff0de6196..052dcf66f 100644 --- a/theories/Numbers/Integer/Axioms/ZTimes.v +++ b/theories/Numbers/Integer/Axioms/ZTimes.v @@ -1,7 +1,4 @@ -Require Import NumPrelude. -Require Import ZDomain. -Require Import ZAxioms. -Require Import ZPlus. +Require Export ZPlus. Module Type TimesSignature. Declare Module Export PlusModule : PlusSignature. diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v index 460a13bf4..a72636a42 100644 --- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v +++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v @@ -1,12 +1,9 @@ -Require Import ZPlus. -Require Import ZTimes. -Require Import ZOrder. -Require Import ZPlusOrder. +Require Export ZTimes. +Require Export ZPlusOrder. -Module TimesOrderProperties (Export TimesModule : TimesSignature) - (Export OrderModule : OrderSignature with +Module TimesOrderProperties (TimesModule : TimesSignature) + (OrderModule : OrderSignature with Module IntModule := TimesModule.PlusModule.IntModule). - Module Export TimesPropertiesModule := TimesProperties TimesModule. Module Export PlusOrderPropertiesModule := PlusOrderProperties TimesModule.PlusModule OrderModule. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 02f73f4d1..2ca4bc5d8 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -1,21 +1,12 @@ -Require Import NDomain. -Require Import NAxioms. -Require Import NPlus. -Require Import NTimes. -Require Import NLt. -Require Import NPlusLt. -Require Import NTimesLt. - -Require Import ZDomain. -Require Import ZAxioms. -Require Import ZPlus. -Require Import ZTimes. -Require Import ZOrder. -Require Import ZPlusOrder. -Require Import ZTimesOrder. - -Module NatPairsDomain (NPlusModule : NPlus.PlusSignature) <: - ZDomain.DomainSignature. +Require Export NTimesLt. +Require Export ZTimesOrder. + +Module NatPairsDomain (Export NPlusModule : NPlus.PlusSignature) : + ZDomain.DomainSignature + with Definition Z := (N * N)%type. + with Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat. + with Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat. + Module Export NPlusPropertiesModule := NPlus.PlusProperties NPlusModule. Definition Z : Set := (N * N)%type. diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v index 7d8fb573a..ad17e5255 100644 --- a/theories/Numbers/Natural/Axioms/NAxioms.v +++ b/theories/Numbers/Natural/Axioms/NAxioms.v @@ -174,7 +174,7 @@ Implicit Arguments recursion_S [A]. End NatSignature. -Module NatProperties (Import NatModule : NatSignature). +Module NatProperties (Export NatModule : NatSignature). Module Export DomainPropertiesModule := DomainProperties DomainModule. Open Local Scope NScope. diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v index 1d35bfbc4..85ff0eb72 100644 --- a/theories/Numbers/Natural/Axioms/NDepRec.v +++ b/theories/Numbers/Natural/Axioms/NDepRec.v @@ -1,6 +1,4 @@ -Require Import NAxioms. -Require Import NPlus. -Require Import NTimes. +Require Export NTimes. (* Here we allow dependent recursion only for domains with Libniz equality. The reason is that, if the domain is A : nat -> Set, then (A @@ -28,9 +26,10 @@ Axiom dep_recursion_S : End DepRecSignature. -Module DepRecTimesProperties (Import DepRecModule : DepRecSignature) - (Import TimesModule : TimesSignature - with Module PlusModule.NatModule := DepRecModule.NatModule). +Module DepRecTimesProperties + (Export DepRecModule : DepRecSignature) + (TimesModule : TimesSignature + with Module PlusModule.NatModule := DepRecModule.NatModule). Module Export TimesPropertiesModule := TimesProperties TimesModule. Open Local Scope NScope. diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v index 9dc8e4078..de2ddf116 100644 --- a/theories/Numbers/Natural/Axioms/NDomain.v +++ b/theories/Numbers/Natural/Axioms/NDomain.v @@ -61,7 +61,7 @@ Notation "x # y" := ((E x y) -> False) (at level 70) : NScope. End DomainEqSignature. -Module DomainProperties (Import DomainModule : DomainSignature). +Module DomainProperties (Export DomainModule : DomainSignature). (* It also accepts module of type NatDomainEq *) Open Local Scope NScope. diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v index fdf3418ed..83bcf8ebe 100644 --- a/theories/Numbers/Natural/Axioms/NIso.v +++ b/theories/Numbers/Natural/Axioms/NIso.v @@ -1,4 +1,4 @@ -Require Import NAxioms. +Require Export NAxioms. Module Homomorphism (Nat1 Nat2 : NatSignature). diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v index a70b3f95b..254db11d6 100644 --- a/theories/Numbers/Natural/Axioms/NLt.v +++ b/theories/Numbers/Natural/Axioms/NLt.v @@ -14,8 +14,8 @@ Axiom lt_0 : forall x, ~ (x < 0). Axiom lt_S : forall x y, x < S y <-> x < y \/ x == y. End LtSignature. -Module LtProperties (Import LtModule : LtSignature). -Module Import NatPropertiesModule := NatProperties NatModule. +Module LtProperties (Export LtModule : LtSignature). +Module Export NatPropertiesModule := NatProperties NatModule. Open Local Scope NScope. Theorem lt_n_Sn : forall n, n < S n. diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v index 03f3cd86e..38af96b1d 100644 --- a/theories/Numbers/Natural/Axioms/NMiscFunct.v +++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v @@ -1,11 +1,6 @@ -Require Import Bool. (* To get the negb function *) -Require Import NAxioms. -Require Import NStrongRec. -Require Import NPlus. -Require Import NTimes. -Require Import NLt. -Require Import NPlusLt. -Require Import NTimesLt. +Require Export Bool. (* To get the negb function *) +Require Export NStrongRec. +Require Export NTimesLt. Module MiscFunctFunctor (NatMod : NatSignature). Module Export NatPropertiesModule := NatProperties NatMod. @@ -318,7 +313,7 @@ Qed. End DefaultPlusModule. Module DefaultTimesModule <: TimesSignature. -Module Import PlusModule := DefaultPlusModule. +Module PlusModule := DefaultPlusModule. Definition times := times. @@ -361,11 +356,11 @@ Qed. End DefaultLtModule. -Module Import DefaultPlusProperties := PlusProperties DefaultPlusModule. -Module Import DefaultTimesProperties := TimesProperties DefaultTimesModule. -Module Import DefaultLtProperties := LtProperties DefaultLtModule. -Module Import DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule. -Module Import DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule. +Module Export DefaultPlusProperties := PlusProperties DefaultPlusModule. +Module Export DefaultTimesProperties := TimesProperties DefaultTimesModule. +Module Export DefaultLtProperties := LtProperties DefaultLtModule. +Module Export DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule. +Module Export DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule. (*Opaque MiscFunctFunctor.plus. Check plus_comm. (* This produces the following *) diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v index d2ef81018..63cc8a40f 100644 --- a/theories/Numbers/Natural/Axioms/NPlus.v +++ b/theories/Numbers/Natural/Axioms/NPlus.v @@ -17,7 +17,7 @@ Axiom plus_Sn_m : forall n m, (S n) + m == S (n + m). End PlusSignature. -Module PlusProperties (Import PlusModule : PlusSignature). +Module PlusProperties (Export PlusModule : PlusSignature). Module Export NatPropertiesModule := NatProperties NatModule. Open Local Scope NScope. diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusLt.v index 77bd80012..3724f9ec5 100644 --- a/theories/Numbers/Natural/Axioms/NPlusLt.v +++ b/theories/Numbers/Natural/Axioms/NPlusLt.v @@ -1,8 +1,8 @@ Require Export NPlus. Require Export NLt. -Module PlusLtProperties (Import PlusModule : PlusSignature) - (Import LtModule : LtSignature with +Module PlusLtProperties (PlusModule : PlusSignature) + (LtModule : LtSignature with Module NatModule := PlusModule.NatModule). Module Export PlusPropertiesModule := PlusProperties PlusModule. Module Export LtPropertiesModule := LtProperties LtModule. diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v index 5e8223108..a2e73f99a 100644 --- a/theories/Numbers/Natural/Axioms/NStrongRec.v +++ b/theories/Numbers/Natural/Axioms/NStrongRec.v @@ -1,7 +1,7 @@ -Require Import NAxioms. +Require Export NAxioms. -Module StrongRecProperties (Import NatModule : NatSignature). -Module Export DomainPropertiesModule := DomainProperties NatModule.DomainModule. +Module StrongRecProperties (NatModule : NatSignature). +Module Export NatPropertiesModule := NatProperties NatModule. Open Local Scope NScope. Section StrongRecursion. diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v index 6a7e9ba39..4d1d2b0ca 100644 --- a/theories/Numbers/Natural/Axioms/NTimes.v +++ b/theories/Numbers/Natural/Axioms/NTimes.v @@ -15,7 +15,7 @@ Axiom times_Sn_m : forall n m, (S n) * m == m + n * m. End TimesSignature. -Module TimesProperties (Import TimesModule : TimesSignature). +Module TimesProperties (Export TimesModule : TimesSignature). Module Export PlusPropertiesModule := PlusProperties PlusModule. Open Local Scope NScope. diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesLt.v index c728f05a8..36989f1b3 100644 --- a/theories/Numbers/Natural/Axioms/NTimesLt.v +++ b/theories/Numbers/Natural/Axioms/NTimesLt.v @@ -1,13 +1,13 @@ -Require Export NLt. Require Export NTimes. Require Export NPlusLt. -Module TimesLtProperties (Import TimesModule : TimesSignature) - (Import LtModule : LtSignature with +Module TimesLtProperties (TimesModule : TimesSignature) + (LtModule : LtSignature with Module NatModule := TimesModule.PlusModule.NatModule). -Module Export TimesPropertiesModule := TimesProperties TimesModule. -Module Export LtPropertiesModule := LtProperties LtModule. -Module Export PlusLtPropertiesModule := PlusLtProperties TimesModule.PlusModule LtModule. +Module Export TimesPropertiesModule := + TimesProperties TimesModule. +Module Export PlusLtPropertiesModule := + PlusLtProperties TimesModule.PlusModule LtModule. Open Local Scope NScope. Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 47b39bfeb..77fbdcaf7 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -1,18 +1,16 @@ Require Import NArith. Require Import Ndec. -Require Import NDepRec. -Require Import NAxioms. -Require Import NPlus. -Require Import NTimes. -Require Import NLt. -Require Import NPlusLt. -Require Import NTimesLt. -Require Import NMiscFunct. +Require Export NDepRec. +Require Export NTimesLt. +Require Export NMiscFunct. -Open Scope N_scope. +Open Local Scope N_scope. -Module BinaryDomain <: DomainEqSignature. +Module BinaryDomain : DomainEqSignature + with Definition N := N + with Definition E := (@eq N) + with Definition e := Neqb. Definition N := N. Definition E := (@eq N). @@ -188,17 +186,16 @@ Qed. End BinaryLt. -Module Export BinaryPlusProperties := PlusProperties BinaryPlus. -Module Export BinaryTimesProperties := TimesProperties BinaryTimes. -Module Export BinaryDepRecTimesProperties := - DepRecTimesProperties BinaryDepRec BinaryTimes. -Module Export BinaryLtProperties := LtProperties BinaryLt. -Module Export BinaryPlusLtProperties := PlusLtProperties BinaryPlus BinaryLt. Module Export BinaryTimesLtProperties := TimesLtProperties BinaryTimes BinaryLt. -Module Export BinaryRecEx := MiscFunctFunctor BinaryNat. +(*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*) + +(* Just 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 @@ -211,11 +208,5 @@ match n with | 0 => 0 | Npos p => binposlog p end. - +*) (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *) - - -(*Check nat_total_order : forall n m : N, (n = m -> False) -> lt n m \/ lt m n. -Check mult_positive : forall n m : N, lt 0 n -> lt 0 m -> lt 0 (n * m).*) - -Close Scope N_scope. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 057a0e5ac..00248a53c 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -1,10 +1,6 @@ -Require Import NDepRec. -Require Import NPlus. -Require Import NTimes. -Require Import NLt. -Require Import NPlusLt. -Require Import NTimesLt. -Require Import NMiscFunct. +Require Export NDepRec. +Require Export NTimesLt. +Require Export NMiscFunct. Module PeanoDomain : DomainEqSignature with Definition N := nat @@ -31,8 +27,6 @@ Add Relation N E as E_rel. End PeanoDomain. -Open Scope NScope. -Import PeanoDomain. Module PeanoNat <: NatSignature. Module Export DomainModule := PeanoDomain. @@ -40,13 +34,6 @@ Module Export DomainModule := PeanoDomain. Definition O := 0. Definition S := S. -(* For the following line, it is important that we declared -PeanoDomain module above to be transparent, i.e., we used "<:" -operator intead of ":". If we used ":", then the value of N, i.e., -nat, would not be visible here. Therefore, the type of E, which is -N -> N -> Prop, would not be coercible to nat -> nat -> Prop. -So we would not be able to claim that S is a morphism with respect -to E. The same goes for defining * in terms of +, etc. *) Add Morphism S with signature E ==> E as S_wd. Proof. congruence. @@ -161,11 +148,6 @@ Qed. End PeanoTimes. -(* Some checks: -Check times_eq_1 : forall n m, n * m = 1 -> n = 1 /\ m = 1. -Eval compute in times_eq_0_dec 0 5. -Eval compute in times_eq_0_dec 5 0. *) - Module PeanoLt <: LtSignature. Module Export NatModule := PeanoNat. @@ -190,43 +172,10 @@ End PeanoLt. (* Obtaining properties for +, *, <, and their combinations *) -Module Export PeanoPlusProperties := PlusProperties PeanoPlus. -Module Export PeanoTimesProperties := TimesProperties PeanoTimes. -Module Export PeanoLtProperties := LtProperties PeanoLt. -Module Export PeanoPlusLtProperties := PlusLtProperties PeanoPlus PeanoLt. Module Export PeanoTimesLtProperties := TimesLtProperties PeanoTimes PeanoLt. Module Export PeanoDepRecTimesProperties := DepRecTimesProperties PeanoDepRec PeanoTimes. -Module MiscFunctModule := MiscFunctFunctor PeanoNat. - -(*Eval compute in MiscFunctModule.lt 6 5.*) - -(*Set Printing All.*) -(*Check plus_comm. -Goal forall x y : nat, x + y = y + x. -intros x y. -rewrite plus_comm. reflexivity. (* does now work -- but the next line does *) -apply plus_comm.*) - -(*Opaque plus. -Eval compute in (forall n m : N, E m (PeanoPlus.Nat.S (PeanoPlus.plus n m)) -> False). - -Eval compute in (plus_eq_1_dec 1 1). -Opaque plus_eq_1_dec. -Check plus_eq_1. -Eval compute in (forall m n : N, - E (PeanoPlus.plus m n) (PeanoPlus.Nat.S PeanoPlus.Nat.O) -> - (plus_eq_1_dec m n = true -> - E m PeanoPlus.Nat.O /\ E n (PeanoPlus.Nat.S PeanoPlus.Nat.O)) /\ - (plus_eq_1_dec m n = false -> - E m (PeanoPlus.Nat.S PeanoPlus.Nat.O) /\ E n PeanoPlus.Nat.O)).*) - -(*Require Import rec_ex. - -Module Import PeanoRecursionExamples := RecursionExamples PeanoNat. +(*Module MiscFunctModule := MiscFunctFunctor PeanoNat.*) +(* The instruction above adds about 1M to the size of the .vo file !!! *) -Eval compute in mult 3 15. -Eval compute in e 100 100. -Eval compute in log 8. -Eval compute in half 0.*) |