Specification of : interval |
Require Export Setoid.
Set Implicit Arguments.
Set Strict Implicit.
Preliminaries |
|
Fixpoint comp (A:Type) (f : A -> A -> A) (x:A) (u : nat -> A) (n:nat) {struct n}: A :=
match n with O => x | S p => f (u p) (comp f x u p) end.
Lemma comp0 : forall (A:Type) (f : A -> A -> A) (x:A) (u : nat -> A),
comp f x u 0 = x.
Lemma compS : forall (A:Type) (f : A -> A -> A) (x:A) (u : nat -> A) (n:nat),
comp f x u (S n) = f (u n) (comp f x u n).
monotonicity of sequences for an arbitrary relation |
Definition mon_seq (A:Type) (le : A -> A -> Prop) (f:nat ->A)
:= forall n m, (n <= m) -> (le (f n) (f m)).
Definition decr_seq (A:Type) (le : A -> A -> Prop) (f:nat ->A)
:= forall n m, (n <= m) -> (le (f m) (f n)).
Specification of |
|
Module Type Universe.
Parameter U : Type.
Bind Scope U_scope with U.
Parameters Ueq Ule : U -> U -> Prop.
Parameters U0 U1 : U.
Parameters Uplus Umult : U -> U -> U.
Parameter Uinv : U -> U.
Parameter Unth : nat -> U.
Infix "+" := Uplus : U_scope.
Infix "*" := Umult : U_scope.
Infix "==" := Ueq (at level 70) : U_scope.
Infix "<=" := Ule : U_scope.
Open Scope U_scope.
Properties |
Hypothesis Ueq_refl : forall x:U, x == x.
Hypothesis Ueq_sym : forall x y:U, x == y -> y == x.
Hypothesis Udiff_0_1 : ~(U0 == U1).
Hypothesis Upos : forall x:U, (U0 <= x).
Hypothesis Unit : forall x:U, (x <= U1).
Hypothesis Uplus_sym : forall x y:U, (x + y) == (y + x).
Hypothesis Uplus_assoc : forall x y z:U, (x + (y + z)) == (x + y + z).
Hypothesis Uplus_zero_left : forall x:U, (U0 + x) == x.
Hypothesis Umult_sym : forall x y:U, (x * y) == (y * x).
Hypothesis Umult_assoc : forall x y z:U, (x * (y * z)) == (x * y * z).
Hypothesis Umult_one_left : forall x:U, (U1 * x) == x.
Hypothesis Uinv_one : (Uinv U1) == U0.
Hypothesis Uinv_opp_left : forall x, (Uinv x) + x == U1.
| holds when does not overflow |
Hypothesis Uinv_plus_left
: forall x y, y <= (Uinv x) -> Uinv (x + y) + x == Uinv y.
| holds when does not overflow |
Hypothesis Udistr_plus_right : forall x y z:U,
(x <= Uinv y) -> ((x + y) * z) == (x * z + y * z).
Hypothesis Udistr_inv_right :
forall x y:U, Uinv (x * y) == (Uinv x) * y + (Uinv y).
| The relation is reflexive, transitive and anti-symmetric |
Hypothesis Ueq_le : forall x y:U, x == y -> x <= y.
Hypothesis Ule_trans
: forall x y z:U, (x <= y) -> (y <= z) -> (x <= z).
Hypothesis Ule_antisym
: forall x y:U, (x <= y) -> (y <= x) -> (x == y).
| Totality of the order |
Hypothesis Ueq_double_neg
: forall x y : U, ~~(x == y) -> (x == y).
Hypothesis Ule_total
: forall x y : U, (x <= y) \/ (y <= x).
| The relation is compatible with operators |
Hypothesis Uplus_le_compat_right :
forall x y z:U, (x <= y) -> (x + z) <= (y + z).
Hypothesis Umult_le_compat_right :
forall x y z:U, (x <= y) -> (x * z) <= (y * z).
Hypothesis Uinv_le_compat
: forall x y:U, x <= y -> Uinv y <= Uinv x.
| Properties of simplification in case there is no overflow |
Hypothesis Uplus_le_simpl_right :
forall x y z:U, (z <= (Uinv x)) -> ((x + z) <= (y + z)) -> (x <= y).
Hypothesis Umult_le_simpl_left :
forall x y z: U, ~(U0 == z) -> (z * x) <= (z * y) -> x <= y .
Unth
|
Hypothesis Unth_prop :
forall n, (Unth n) == Uinv (comp Uplus U0 (fun k => Unth n) n).
archimedian |
Hypothesis archimedian :
forall x, ~x == U0 -> exists n, Unth n <= x.
least upper bound, corresponds to limit for increasing sequences |
Variable lub : (nat -> U) -> U.
Hypothesis le_lub : forall (f : nat -> U) (n:nat), (f n) <= (lub f).
Hypothesis lub_le : forall (f : nat -> U) (x:U),
(forall n:nat, f n <= x) -> (lub f) <= x.
stability properties of lubs |
Hypothesis lub_eq_plus_cte_right :
forall (f : nat -> U) (k:U), lub (fun n => (f n) + k) == (lub f) + k.
Hypothesis lub_eq_mult : forall k : U, forall f : nat -> U,
lub (fun n => (k * (f n))) == k * lub f.
End Universe.