-
Notifications
You must be signed in to change notification settings - Fork 0
/
Utheory.v
96 lines (69 loc) · 3.36 KB
/
Utheory.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
(** * Utheory.v: Specification of $U$, interval $[0,1]$ *)
From ALEA Require Export Misc.
From ALEA Require Export Ccpo.
Set Implicit Arguments.
Open Scope O_scope.
(** ** Basic operators of $U$ *)
(** - Constants : $0$ and $1$
- Constructor : [Unth] $n (\equiv \frac{1}{n+1})$
- Operations : $x+y~(\equiv min (x+y,1))$, $x*y$, [inv] $x~(\equiv 1 -x)$
- Relations : $x\leq y$, $x==y$
*)
Module Type Universe.
Parameter U : cpo.
Declare Scope U_scope.
Parameter U1 : U.
Parameters Uplus Umult Udiv: U -> U -> U.
Parameter Uinv : U -> U.
Parameter Unth : nat -> U.
(*
Definition Uplus x y := UPlus x y.
Definition Umult x y := UMult x y.
*)
Infix "+" := Uplus : U_scope.
Infix "*" := Umult : U_scope.
Infix "/" := Udiv : U_scope.
Notation "[1-] x" := (Uinv x) (at level 35, right associativity) : U_scope.
Notation "1" := U1 : U_scope.
Notation "[1/]1+ n" := (Unth n) (at level 35, right associativity) : U_scope.
Open Scope U_scope.
(** ** Basic Properties *)
Parameter Udiff_0_1 : ~0 == 1.
Parameter Unit : forall x:U, x <= 1.
Parameter Uplus_sym : forall x y:U, x + y == y + x.
Parameter Uplus_assoc : forall x y z:U, x + (y + z) == x + y + z.
Parameter Uplus_zero_left : forall x:U, 0 + x == x.
Parameter Umult_sym : forall x y:U, x * y == y * x.
Parameter Umult_assoc : forall x y z:U, x * (y * z) == x * y * z.
Parameter Umult_one_left : forall x:U, 1 * x == x.
Parameter Uinv_one : [1-] 1 == 0.
Parameter Uinv_opp_left : forall x, [1-] x + x == 1.
Parameter Umult_div : forall x y, ~0 == y -> x <= y -> y * (x/y) == x.
Parameter Udiv_le_one : forall x y, ~0 == y -> y <= x -> (x/y) == 1.
Parameter Udiv_by_zero : forall x y, 0 == y -> (x/y) == 0.
(** - Property : $1 - (x+y) + x=1-y$ holds when $x+y$ does not overflow *)
Parameter Uinv_plus_left : forall x y, y <= [1-] x -> [1-] (x + y) + x == [1-] y.
(** - Property : $(x + y) \times z = x \times z + y \times z$
holds when $x+y$ does not overflow *)
Parameter Udistr_plus_right : forall x y z (H : x <= [1-] y), (x + y) * z == x * z + y * z.
(** - Property : $1 - (x \times y) = (1 - x)\times y + (1-y)$ *)
Parameter Udistr_inv_right : forall x y:U, [1-] (x * y) == ([1-] x) * y + [1-] y.
(** - Totality of the order *)
Parameter Ule_class : forall x y : U, class (x <= y).
Parameter Ule_total : forall x y : U, orc (x<=y) (y<=x).
Arguments Ule_total : clear implicits.
(** - The relation $x\leq y$ is compatible with operators *)
Parameter Uplus_le_compat_right : forall x y z:U, y <= z -> x + y <= x + z.
Parameter Umult_le_compat_right : forall x y z:U, y <= z -> x * y <= x * z.
Parameter Uinv_le_compat : forall x y:U, x <= y -> [1-] y <= [1-] x.
(** - Properties of simplification in case there is no overflow *)
Parameter Uplus_le_simpl_right : forall x y z, z <= [1-] x -> x + z <= y + z -> x <= y.
Parameter Umult_le_simpl_left : forall x y z: U, ~0 == z -> z * x <= z * y -> x <= y .
(** - Property [Unth] $\frac{1}{n+1} == 1 - n \times \frac{1}{n+1}$ *)
Parameter Unth_prop : forall n, [1/]1+n == [1-](comp Uplus 0 (fun k => [1/]1+n) n).
(** - Archimedian property *)
Parameter archimedian : forall x, ~0 == x -> exc (fun n => [1/]1+n <= x).
(** - Stability properties of lubs with respect to [+] and [*] *)
Parameter Uplus_right_continuous : forall k, continuous (mk_fmono (Uplus_le_compat_right k)).
Parameter Umult_right_continuous : forall k, continuous (mk_fmono (Umult_le_compat_right k)).
End Universe.