1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(*i $Id: Rdefinitions.v 10751 2008-04-04 10:23:35Z herbelin $ i*)
11
(*********************************************************)
12
(** Definitions for the axiomatization *)
13
(*********************************************************)
15
Require Export ZArith_base.
19
(* Declare Scope positive_scope with Key R *)
20
Delimit Scope R_scope with R.
22
(* Automatically open scope R_scope for arguments of type R *)
23
Bind Scope R_scope with R.
25
Open Local Scope R_scope.
29
Parameter Rplus : R -> R -> R.
30
Parameter Rmult : R -> R -> R.
31
Parameter Ropp : R -> R.
32
Parameter Rinv : R -> R.
33
Parameter Rlt : R -> R -> Prop.
34
Parameter up : R -> Z.
36
Infix "+" := Rplus : R_scope.
37
Infix "*" := Rmult : R_scope.
38
Notation "- x" := (Ropp x) : R_scope.
39
Notation "/ x" := (Rinv x) : R_scope.
41
Infix "<" := Rlt : R_scope.
43
(***********************************************************)
46
Definition Rgt (r1 r2:R) : Prop := r2 < r1.
49
Definition Rle (r1 r2:R) : Prop := r1 < r2 \/ r1 = r2.
52
Definition Rge (r1 r2:R) : Prop := Rgt r1 r2 \/ r1 = r2.
55
Definition Rminus (r1 r2:R) : R := r1 + - r2.
58
Definition Rdiv (r1 r2:R) : R := r1 * / r2.
62
Infix "-" := Rminus : R_scope.
63
Infix "/" := Rdiv : R_scope.
65
Infix "<=" := Rle : R_scope.
66
Infix ">=" := Rge : R_scope.
67
Infix ">" := Rgt : R_scope.
69
Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope.
70
Notation "x <= y < z" := (x <= y /\ y < z) : R_scope.
71
Notation "x < y < z" := (x < y /\ y < z) : R_scope.
72
Notation "x < y <= z" := (x < y /\ y <= z) : R_scope.