From 88cf0acb11ae2b4a7e0fb7df8289c15eb0748f19 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:28 +0000 Subject: BinNatDef containing all functions of BinNat, misc adaptations in BinPos git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14102 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/PArith/BinPos.v | 19 ++++++++++++++++++- theories/PArith/BinPosDef.v | 15 --------------- 2 files changed, 18 insertions(+), 16 deletions(-) (limited to 'theories/PArith') diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v index 67d193a6d..4ef91362f 100644 --- a/theories/PArith/BinPos.v +++ b/theories/PArith/BinPos.v @@ -34,7 +34,7 @@ Module Pos <: UsualDecidableTypeFull <: TotalOrder. -(** * The definitions of operations are now in a separate file *) +(** * Definitions of operations, now in a separate file *) Include BinPosDef.Pos. @@ -42,10 +42,27 @@ Include BinPosDef.Pos. Definition shiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p. Definition shiftr_nat (p:positive)(n:nat) := iter_nat n _ div2 p. +(** * Logical Predicates *) + Definition eq := @Logic.eq t. Definition eq_equiv := @eq_equivalence t. Include BackportEq. +Definition lt x y := (x ?= y) = Lt. +Definition gt x y := (x ?= y) = Gt. +Definition le x y := (x ?= y) <> Gt. +Definition ge x y := (x ?= y) <> Lt. + +Infix "<=" := le : positive_scope. +Infix "<" := lt : positive_scope. +Infix ">=" := ge : positive_scope. +Infix ">" := gt : positive_scope. + +Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope. +Notation "x < y < z" := (x < y /\ y < z) : positive_scope. +Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope. + (**********************************************************************) (** * Properties of operations over positive numbers *) diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 10c882188..cf7e450f4 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -265,21 +265,6 @@ Definition compare x y := compare_cont x y Eq. Infix "?=" := compare (at level 70, no associativity) : positive_scope. -Definition lt x y := (x ?= y) = Lt. -Definition gt x y := (x ?= y) = Gt. -Definition le x y := (x ?= y) <> Gt. -Definition ge x y := (x ?= y) <> Lt. - -Infix "<=" := le : positive_scope. -Infix "<" := lt : positive_scope. -Infix ">=" := ge : positive_scope. -Infix ">" := gt : positive_scope. - -Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope. -Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope. -Notation "x < y < z" := (x < y /\ y < z) : positive_scope. -Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope. - Definition min p p' := match p ?= p' with | Lt | Eq => p -- cgit v1.2.3