diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZAxioms.v')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v new file mode 100644 index 00000000..c4a4b6b8 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -0,0 +1,65 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id: ZAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NZAxioms. + +Set Implicit Arguments. + +Module Type ZAxiomsSig. +Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. + +Delimit Scope IntScope with Int. +Notation Z := NZ. +Notation Zeq := NZeq. +Notation Z0 := NZ0. +Notation Z1 := (NZsucc NZ0). +Notation S := NZsucc. +Notation P := NZpred. +Notation Zadd := NZadd. +Notation Zmul := NZmul. +Notation Zsub := NZsub. +Notation Zlt := NZlt. +Notation Zle := NZle. +Notation Zmin := NZmin. +Notation Zmax := NZmax. +Notation "x == y" := (NZeq x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. +Notation "0" := NZ0 : IntScope. +Notation "1" := (NZsucc NZ0) : IntScope. +Notation "x + y" := (NZadd x y) : IntScope. +Notation "x - y" := (NZsub x y) : IntScope. +Notation "x * y" := (NZmul x y) : IntScope. +Notation "x < y" := (NZlt x y) : IntScope. +Notation "x <= y" := (NZle x y) : IntScope. +Notation "x > y" := (NZlt y x) (only parsing) : IntScope. +Notation "x >= y" := (NZle y x) (only parsing) : IntScope. + +Parameter Zopp : Z -> Z. + +(*Notation "- 1" := (Zopp 1) : IntScope. +Check (-1).*) + +Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. + +Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. +Notation "- 1" := (Zopp (NZsucc NZ0)) : IntScope. + +Open Local Scope IntScope. + +(* Integers are obtained by postulating that every number has a predecessor *) +Axiom Zsucc_pred : forall n : Z, S (P n) == n. + +Axiom Zopp_0 : - 0 == 0. +Axiom Zopp_succ : forall n : Z, - (S n) == P (- n). + +End ZAxiomsSig. + |