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.