diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZAxioms.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 42 |
1 files changed, 34 insertions, 8 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 33236cde..fcd98787 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.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,8 +8,6 @@ (** Initial Author : Evgeny Makarov, INRIA, 2007 *) -(*i $Id: NZAxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Equalities Orders NumPrelude GenericMinMax. (** Axiomatization of a domain with zero, successor, predecessor, @@ -20,7 +18,7 @@ Require Export Equalities Orders NumPrelude GenericMinMax. *) Module Type ZeroSuccPred (Import T:Typ). - Parameter Inline zero : t. + Parameter Inline(20) zero : t. Parameters Inline succ pred : t -> t. End ZeroSuccPred. @@ -28,8 +26,6 @@ Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T). Notation "0" := zero. Notation S := succ. Notation P := pred. - Notation "1" := (S 0). - Notation "2" := (S 1). End ZeroSuccPredNotation. Module Type ZeroSuccPred' (T:Typ) := @@ -44,9 +40,33 @@ Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E). A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n. End IsNZDomain. -Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain. -Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain. +(** Axiomatization of some more constants + + Simply denoting "1" for (S 0) and so on works ok when implementing + by nat, but leaves some (Nsucc N0) when implementing by N. +*) + +Module Type OneTwo (Import T:Typ). + Parameter Inline(20) one two : t. +End OneTwo. +Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T). + Notation "1" := one. + Notation "2" := two. +End OneTwoNotation. + +Module Type OneTwo' (T:Typ) := OneTwo T <+ OneTwoNotation T. + +Module Type IsOneTwo (E:Eq')(Z:ZeroSuccPred' E)(O:OneTwo' E). + Import E Z O. + Axiom one_succ : 1 == S 0. + Axiom two_succ : 2 == S 1. +End IsOneTwo. + +Module Type NZDomainSig := + EqualityType <+ ZeroSuccPred <+ IsNZDomain <+ OneTwo <+ IsOneTwo. +Module Type NZDomainSig' := + EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo. (** Axiomatization of basic operations : [+] [-] [*] *) @@ -117,3 +137,9 @@ Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare. Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare. Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare. +(** A square function *) + +Module Type NZSquare (Import NZ : NZBasicFunsSig'). + Parameter Inline square : t -> t. + Axiom square_spec : forall n, square n == n * n. +End NZSquare. |