Library ALEA.Uprop
Add Rec LoadPath "." as ALEA.
Set Implicit Arguments.
Require Export Utheory.
Require Export Arith.
Require Export Omega.
Open Local Scope U_scope.
Notation "[1/] n" := (Unth (pred n)) (at level 35, right associativity).
Lemma Uplus_le_compat_right : forall x y z:U, y <= z -> x + y <= x + z.
Hint Resolve Uplus_le_compat_right.
Instance Uplus_mon2 : monotonic2 Uplus.
Save.
Hint Resolve Uplus_mon2.
Lemma Uplus_le_compat_left : forall x y z:U, x <= y -> x + z <= y + z.
Hint Resolve Uplus_le_compat_left.
Lemma Uplus_le_compat : forall x y z t, x <= y -> z <= t -> x + z <= y + t.
Hint Immediate Uplus_le_compat.
Lemma Uplus_eq_compat_left : forall x y z:U, x == y -> x + z == y + z.
Hint Resolve Uplus_eq_compat_left.
Lemma Uplus_eq_compat_right : forall x y z:U, x == y -> (z + x) == (z + y).
Hint Resolve Uplus_eq_compat_left Uplus_eq_compat_right.
Add Morphism Uplus with signature Oeq ==> Oeq ==> Oeq as Uplus_eq_compat.
Qed.
Hint Immediate Uplus_eq_compat.
Add Morphism Uinv with signature Oeq ==> Oeq as Uinv_eq_compat.
Qed.
Hint Resolve Uinv_eq_compat.
Lemma Uplus_zero_right : forall x:U, x + 0 == x.
Hint Resolve Uplus_zero_right.
Lemma Uinv_opp_left : forall x, [1-] x + x == 1.
Hint Resolve Uinv_opp_left.
Lemma Uinv_opp_right : forall x, x + [1-] x == 1.
Hint Resolve Uinv_opp_right.
Lemma Uinv_inv : forall x : U, [1-] [1-] x == x.
Hint Resolve Uinv_inv.
Lemma Unit : forall x:U, x <= 1.
Hint Resolve Unit.
Lemma Uinv_zero : [1-] 0 = 1.
Lemma Ueq_class : forall x y:U, class (x==y).
Lemma Ueq_double_neg : forall x y : U, ~ ~ (x == y) -> x == y.
Hint Resolve Ueq_class.
Hint Immediate Ueq_double_neg.
Lemma Ule_orc : forall x y : U, orc (x<=y) (~ x<=y).
Implicit Arguments Ule_orc [].
Lemma Ueq_orc : forall x y:U, orc (x==y) (~ x==y).
Implicit Arguments Ueq_orc [].
Lemma Upos : forall x:U, 0 <= x.
Lemma Ule_0_1 : 0 <= 1.
Hint Resolve Upos Ule_0_1.
Definition UPlus : U -m> U -m> U := mon2 Uplus.
Definition UPlus_simpl : forall x y, UPlus x y = x+y.
Save.
Instance Uplus_continuous2 : continuous2 (mon2 Uplus).
Save.
Hint Resolve Uplus_continuous2.
Lemma Uplus_lub_eq : forall f g : nat -m> U,
lub f + lub g == lub ((UPlus @2 f) g).
Lemma Umult_le_compat_right : forall x y z:U, y <= z -> x * y <= x * z.
Hint Resolve Umult_le_compat_right.
Instance Umult_mon2 : monotonic2 Umult.
Save.
Lemma Umult_le_compat_left : forall x y z:U, x <= y -> x * z <= y * z.
Hint Resolve Umult_le_compat_left.
Lemma Umult_le_compat : forall x y z t, x <= y -> z <= t -> x * z <= y * t.
Hint Immediate Umult_le_compat.
Definition UMult : U -m> U -m> U := mon2 Umult.
Lemma Umult_eq_compat_left : forall x y z:U, x == y -> (x * z) == (y * z).
Hint Resolve Umult_eq_compat_left.
Lemma Umult_eq_compat_right : forall x y z:U, x == y -> (z * x) == (z * y).
Hint Resolve Umult_eq_compat_left Umult_eq_compat_right.
Definition UMult_simpl : forall x y, UMult x y = x*y.
Save.
Instance Umult_continuous2 : continuous2 (mon2 Umult).
Save.
Hint Resolve Umult_continuous2.
Lemma Umult_lub_eq : forall f g : nat -m> U,
lub f * lub g == lub ((UMult @2 f) g).
Lemma Umultk_lub_eq : forall (k:U) (f : nat -m> U),
k * lub f == lub (UMult k @ f).
Add Morphism Umult with signature Oeq ==> Oeq ==> Oeq
as Umult_eq_compat.
Qed.
Hint Immediate Umult_eq_compat.
Instance Uinv_mon : monotonic (o1:=Iord U) Uinv.
Save.
Definition UInv : U --m> U := mon (o1:=Iord U) Uinv.
Definition UInv_simpl : forall x, UInv x = [1-]x.
Save.
Lemma Ule_eq_compat :
forall x1 x2 : U, x1 == x2 -> forall x3 x4 : U, x3 == x4 -> x1 <= x3 -> x2 <= x4.
Lemma Ult_class : forall x y, class ( x < y ).
Hint Resolve Ult_class.
Lemma Ult_notle_equiv : forall x y:U, x < y <-> ~ (y <= x).
Lemma notUle_lt : forall x y:U, ~ (y <= x) -> x < y.
Hint Immediate notUle_lt.
Lemma notUlt_le : forall x y, ~ x < y -> y <= x.
Hint Immediate notUlt_le.
Lemma notUle_le : forall x y:U, ~ (y <= x) -> x <= y.
Hint Immediate notUle_le.
Lemma Ule_zero_eq : forall x:U, x <= 0 -> x == 0.
Lemma Uge_one_eq : forall x:U, 1 <= x -> x == 1.
Hint Immediate Ule_zero_eq Uge_one_eq.
Lemma Ult_neq_zero : forall x, ~ 0 == x -> 0 < x.
Lemma Ult_neq_one : forall x, ~ 1 == x -> x < 1.
Hint Resolve Ule_total Ult_neq_zero Ult_neq_one.
Lemma not_Ult_eq_zero : forall x, ~ 0 < x -> 0 == x.
Lemma not_Ult_eq_one : forall x, ~ x < 1 -> 1 == x.
Hint Immediate not_Ult_eq_zero not_Ult_eq_one.
Lemma Ule_lt_orc_eq : forall x y, x <= y -> orc (x < y) (x == y).
Hint Resolve Ule_lt_orc_eq.
Lemma Udiff_lt_orc : forall x y, ~ x == y -> orc (x < y) (y < x).
Hint Resolve Udiff_lt_orc.
Lemma Uplus_pos_elim : forall x y,
0 < x + y -> orc (0 < x) (0 < y).
Lemma Udistr_plus_left : forall x y z, y <= [1-] z -> x * (y + z) == x * y + x * z.
Lemma Udistr_inv_left : forall x y, [1-](x * y) == (x * ([1-] y)) + [1-] x.
Hint Resolve Uinv_eq_compat Udistr_plus_left Udistr_inv_left.
Lemma Uplus_perm2 : forall x y z:U, x + (y + z) == y + (x + z).
Lemma Umult_perm2 : forall x y z:U, x * (y * z) == y * (x * z).
Lemma Uplus_perm3 : forall x y z : U, (x + (y + z)) == z + (x + y).
Lemma Umult_perm3 : forall x y z : U, (x * (y * z)) == z * (x * y).
Hint Resolve Uplus_perm2 Umult_perm2 Uplus_perm3 Umult_perm3.
Lemma Uinv_simpl : forall x y : U, [1-] x == [1-] y -> x == y.
Hint Immediate Uinv_simpl.
Lemma Umult_decomp : forall x y, x == x * y + x * [1-]y.
Hint Resolve Umult_decomp.
Lemma Umult_one_right : forall x:U, x * 1 == x.
Hint Resolve Umult_one_right.
Lemma Umult_one_right_eq : forall x y:U, y == 1 -> x * y == x.
Hint Resolve Umult_one_right_eq.
Lemma Umult_one_left_eq : forall x y:U, x == 1 -> x * y == y.
Hint Resolve Umult_one_left_eq.
Lemma Udistr_plus_left_le : forall x y z : U, x * (y + z) <= x * y + x * z.
Lemma Uplus_eq_simpl_right :
forall x y z:U, z <= [1-] x -> z <= [1-] y -> (x + z) == (y + z) -> x == y.
Lemma Ule_plus_right : forall x y, x <= x + y.
Lemma Ule_plus_left : forall x y, y <= x + y.
Hint Resolve Ule_plus_right Ule_plus_left.
Lemma Ule_mult_right : forall x y, x * y <= x .
Lemma Ule_mult_left : forall x y, x * y <= y.
Hint Resolve Ule_mult_right Ule_mult_left.
Lemma Uinv_le_perm_right : forall x y:U, x <= [1-] y -> y <= [1-] x.
Hint Immediate Uinv_le_perm_right.
Lemma Uinv_le_perm_left : forall x y:U, [1-] x <= y -> [1-] y <= x.
Hint Immediate Uinv_le_perm_left.
Lemma Uinv_le_simpl : forall x y:U, [1-] x <= [1-] y -> y <= x.
Hint Immediate Uinv_le_simpl.
Lemma Uinv_double_le_simpl_right : forall x y, x<=y -> x <= [1-][1-]y.
Hint Resolve Uinv_double_le_simpl_right.
Lemma Uinv_double_le_simpl_left : forall x y, x<=y -> [1-][1-]x <= y.
Hint Resolve Uinv_double_le_simpl_left.
Lemma Uinv_eq_perm_left : forall x y:U, x == [1-] y -> [1-] x == y.
Hint Immediate Uinv_eq_perm_left.
Lemma Uinv_eq_perm_right : forall x y:U, [1-] x == y -> x == [1-] y.
Hint Immediate Uinv_eq_perm_right.
Lemma Uinv_eq : forall x y:U, x == [1-] y <-> [1-] x == y.
Hint Resolve Uinv_eq.
Lemma Uinv_eq_simpl : forall x y:U, [1-] x == [1-] y -> x == y.
Hint Immediate Uinv_eq_simpl.
Lemma Uinv_double_eq_simpl_right : forall x y, x==y -> x == [1-][1-]y.
Hint Resolve Uinv_double_eq_simpl_right.
Lemma Uinv_double_eq_simpl_left : forall x y, x==y -> [1-][1-]x == y.
Hint Resolve Uinv_double_eq_simpl_left.
Lemma Uinv_plus_right : forall x y, y <= [1-] x -> [1-] (x + y) + y == [1-] x.
Hint Resolve Uinv_plus_right.
Lemma Uplus_eq_simpl_left :
forall x y z:U, x <= [1-] y -> x <= [1-] z -> (x + y) == (x + z) -> y == z.
Lemma Uplus_eq_zero_left : forall x y:U, (x <= [1-] y)-> (x + y) == y -> x == 0.
Lemma Uplus_le_zero_left : forall x y:U, x <= [1-] y -> (x + y) <= y -> x == 0.
Lemma Uplus_le_zero_right : forall x y:U, x <= [1-] y -> (x + y) <= x -> y == 0.
Lemma Uinv_le_trans : forall x y z t, x <= [1-] y -> z <= x -> t <= y -> z <= [1-] t.
Lemma Uinv_plus_left_le : forall x y, [1-]y <= [1-](x+y) + x.
Lemma Uinv_plus_right_le : forall x y, [1-]x <= [1-](x+y) + y.
Hint Resolve Uinv_plus_left_le Uinv_plus_right_le.
Lemma neq_sym : forall x y:U, ~ x==y -> ~ y==x.
Hint Immediate neq_sym.
Lemma Uinv_neq_compat : forall x y, ~ x == y -> ~ [1-] x == [1-] y.
Lemma Uinv_neq_simpl : forall x y, ~ [1-] x == [1-] y-> ~ x == y.
Hint Resolve Uinv_neq_compat.
Hint Immediate Uinv_neq_simpl.
Lemma Uinv_neq_left : forall x y, ~ x == [1-] y -> ~ [1-] x == y.
Lemma Uinv_neq_right : forall x y, ~ [1-] x == y -> ~x == [1-] y.
Hint Immediate Uinv_neq_left Uinv_neq_right.
Lemma Ult_0_1 : (0 < 1).
Hint Resolve Ult_0_1.
Lemma Ule_neq_zero : forall (x y:U), ~ 0 == x -> x <= y -> ~ 0 == y.
Lemma Uplus_neq_zero_left : forall x y, ~ 0 == x -> ~ 0 == x+y.
Lemma Uplus_neq_zero_right : forall x y, ~ 0 == y -> ~ 0 == x+y.
Lemma Uplus_le_simpl_left : forall x y z : U, z <= [1-] x -> z + x <= z + y -> x <= y.
Lemma Uplus_lt_compat_left : forall x y z:U, z <= [1-] y -> x < y -> (x + z) < (y + z).
Lemma Uplus_lt_compat_right : forall x y z:U, z <= [1-] y -> x < y -> (z + x) < (z + y).
Hint Resolve Uplus_lt_compat_right Uplus_lt_compat_left.
Lemma Uplus_one_le : forall x y, x + y == 1 -> [1-] y <= x.
Hint Immediate Uplus_one_le.
Lemma Uplus_one : forall x y, [1-] x <= y -> x + y == 1.
Hint Resolve Uplus_one.
Lemma Uplus_lt_Uinv_lt : forall x y, x + y < 1 -> x < [1-] y.
Hint Resolve Uplus_lt_Uinv_lt.
Lemma Uplus_one_lt : forall x y, x < [1-] y -> x + y < 1.
Hint Immediate Uplus_one_lt.
Lemma Uplus_lt_Uinv : forall x y, x + y < 1 -> x <= [1-] y.
Hint Immediate Uplus_lt_Uinv_lt.
Lemma Uplus_Uinv_one_lt : forall x y, x < y -> x + [1-]y < 1.
Hint Immediate Uplus_Uinv_one_lt.
Lemma Uinv_lt_perm_right : forall x y, x < [1-]y -> y < [1-]x.
Hint Immediate Uinv_lt_perm_right.
Lemma Uinv_lt_perm_left : forall x y, [1-]x < y -> [1-]y < x.
Hint Immediate Uinv_lt_perm_left.
Lemma Uplus_lt_compat_left_lt : forall x y z:U, z < [1-] x -> x < y -> (x + z) < (y + z).
Lemma Uplus_lt_compat_right_lt : forall x y z:U, z < [1-] x -> x < y -> (z + x) < (z + y).
Lemma Uplus_le_lt_compat_lt :
forall x y z t:U, z < [1-] x -> x <= y -> z < t -> (x + z) < (y + t).
Lemma Uplus_lt_le_compat_lt :
forall x y z t:U, z < [1-] x -> x < y -> z <= t -> (x + z) < (y + t).
Lemma Uplus_le_lt_compat :
forall x y z t:U, t <= [1-] y -> x <= y -> z < t -> (x + z) < (y + t).
Lemma Uplus_lt_le_compat :
forall x y z t:U, t <= [1-] y -> x < y -> z <= t -> (x + z) < (y + t).
Hint Immediate Uplus_le_lt_compat_lt Uplus_lt_le_compat_lt Uplus_le_lt_compat Uplus_lt_le_compat.
Lemma Uplus_lt_compat :
forall x y z t:U, t <= [1-] y -> x < y -> z < t -> (x + z) < (y + t).
Hint Immediate Uplus_lt_compat.
Lemma Uplus_lt_compat_lt :
forall x y z t:U, z < [1-] x -> x < y -> z < t -> (x + z) < (y + t).
Hint Immediate Uplus_lt_compat_lt.
Lemma Ult_plus_left : forall x y z : U, x < y -> x < y + z.
Lemma Ult_plus_right : forall x y z : U, x < z -> x < y + z.
Hint Immediate Ult_plus_left Ult_plus_right.
Lemma Uplus_lt_simpl_left : forall x y z:U, z + x < z + y -> x < y.
Lemma Uplus_lt_simpl_right : forall x y z:U, (x + z) < (y + z) -> x < y.
Lemma Uplus_eq_zero : forall x, x < 1 -> (x + x) == x -> x == 0.
Lemma Umult_zero_left : forall x, 0 * x == 0.
Hint Resolve Umult_zero_left.
Lemma Umult_zero_right : forall x, (x * 0) == 0.
Hint Resolve Uplus_eq_zero Umult_zero_right.
Lemma Umult_zero_left_eq : forall x y, x == 0 -> x * y == 0.
Lemma Umult_zero_right_eq : forall x y, y == 0 -> x * y == 0.
Lemma Umult_zero_eq : forall x y z, x == 0 -> x * y == x * z.
Lemma Umult_le_simpl_right : forall x y z, ~ 0 == z -> (x * z) <= (y * z) -> x <= y.
Hint Resolve Umult_le_simpl_right.
Lemma Umult_simpl_right : forall x y z, ~ 0 == z -> (x * z) == (y * z) -> x == y.
Lemma Umult_simpl_left : forall x y z, ~ 0 == x -> (x * y) == (x * z) -> y == z.
Lemma Umult_lt_compat_left : forall x y z, ~ 0 == z -> x < y -> (x * z) < (y * z).
Lemma Umult_lt_compat_right : forall x y z, ~ 0 == z -> x < y -> (z * x) < (z * y).
Lemma Umult_lt_simpl_right : forall x y z, ~ 0 == z -> (x * z) < (y * z) -> x < y.
Lemma Umult_lt_simpl_left : forall x y z, ~ 0 == z -> (z * x) < (z * y) -> x < y.
Hint Resolve Umult_lt_compat_left Umult_lt_compat_right.
Lemma Umult_zero_simpl_right : forall x y, 0 == x * y -> ~ 0 == x -> 0 == y.
Lemma Umult_zero_simpl_left : forall x y, 0 == x * y -> ~ 0 == y -> 0 == x.
Lemma Umult_neq_zero : forall x y, ~ 0 == x -> ~ 0 == y -> ~ 0 == x*y.
Hint Resolve Umult_neq_zero.
Lemma Umult_lt_zero : forall x y, 0 < x -> 0 < y -> 0 < x*y.
Hint Resolve Umult_lt_zero.
Lemma Umult_lt_compat : forall x y z t, x < y -> z < t -> x * z < y * t.
Lemma Uplus_one_right : forall x, x + 1 == 1.
Lemma Uplus_one_left : forall x:U, 1 + x == 1.
Hint Resolve Uplus_one_right Uplus_one_left.
Lemma Uinv_mult_simpl : forall x y z t, x <= [1-] y -> (x * z) <= [1-] (y * t).
Hint Resolve Uinv_mult_simpl.
Lemma Umult_inv_plus : forall x y, x * [1-] y + y == x + y * [1-] x.
Hint Resolve Umult_inv_plus.
Lemma Umult_inv_plus_le : forall x y z, y <= z -> x * [1-] y + y <= x * [1-] z + z.
Hint Resolve Umult_inv_plus_le.
Lemma Uinv_lt_compat : forall x y : U, x < y -> [1-] y < [1-] x.
Hint Resolve Uinv_lt_compat.
Lemma Uinv_lt_simpl : forall x y : U, [1-] y < [1-] x -> x < y.
Hint Immediate Uinv_lt_simpl.
Lemma Ult_inv_Uplus : forall x y, x < [1-] y -> x + y < 1.
Hint Immediate Uplus_lt_Uinv Uinv_lt_perm_left Uinv_lt_perm_right Ult_inv_Uplus.
Lemma Uinv_lt_one : forall x, 0 < x -> [1-]x < 1.
Lemma Uinv_lt_zero : forall x, x < 1 -> 0 < [1-]x.
Hint Resolve Uinv_lt_one Uinv_lt_zero.
Lemma orc_inv_plus_one : forall x y, orc (x<=[1-]y) (x+y==1).
Lemma Umult_lt_right : forall p q, p <1 -> 0 < q -> p * q < q.
Lemma Umult_lt_left : forall p q, 0 < p -> q < 1 -> p * q < p.
Hint Resolve Umult_lt_right Umult_lt_left.
Fixpoint Uexp (x:U) (n:nat) {struct n} : U :=
match n with 0 => 1 | (S p) => x * Uexp x p end.
Infix "^" := Uexp : U_scope.
Lemma Uexp_1 : forall x, x^1 == x.
Lemma Uexp_0 : forall x, x^0 == 1.
Lemma Uexp_zero : forall n, (0<n)%nat -> 0^n == 0.
Lemma Uexp_one : forall n, 1^n == 1.
Lemma Uexp_le_compat_right :
forall x n m, (n<=m)%nat -> x^m <= x^n.
Lemma Uexp_le_compat_left : forall x y n, x <= y -> x^n <= y^n.
Hint Resolve Uexp_le_compat_left Uexp_le_compat_right.
Lemma Uexp_le_compat : forall x y (n m:nat),
x <= y -> n <= m -> x^m <= y^n.
Instance Uexp_mon2 : monotonic2 (o1:=Iord U) (o3:=Iord U) Uexp.
Save.
Definition UExp : U --m> (nat -m-> U) := mon2 Uexp.
Add Morphism Uexp with signature Oeq ==> eq ==> Oeq as Uexp_eq_compat.
Save.
Lemma Uexp_inv_S : forall x n, ([1-]x^(S n)) == x * ([1-]x^n)+[1-]x.
Lemma Uexp_lt_compat : forall p q n, (O<n)%nat -> p<q -> (p^n<q^n).
Hint Resolve Uexp_lt_compat.
Lemma Uexp_lt_zero : forall p n, (0<p) -> (0<p^n).
Hint Resolve Uexp_lt_zero.
Lemma Uexp_lt_one : forall p n, (0<n)%nat -> p<1 -> (p^n<1).
Hint Resolve Uexp_lt_one.
Lemma Uexp_lt_antimon: forall p n m,
(n<m)%nat-> 0 < p -> p < 1 -> p^m < p^n.
Hint Resolve Uexp_lt_antimon.
match n with 0 => 1 | (S p) => x * Uexp x p end.
Infix "^" := Uexp : U_scope.
Lemma Uexp_1 : forall x, x^1 == x.
Lemma Uexp_0 : forall x, x^0 == 1.
Lemma Uexp_zero : forall n, (0<n)%nat -> 0^n == 0.
Lemma Uexp_one : forall n, 1^n == 1.
Lemma Uexp_le_compat_right :
forall x n m, (n<=m)%nat -> x^m <= x^n.
Lemma Uexp_le_compat_left : forall x y n, x <= y -> x^n <= y^n.
Hint Resolve Uexp_le_compat_left Uexp_le_compat_right.
Lemma Uexp_le_compat : forall x y (n m:nat),
x <= y -> n <= m -> x^m <= y^n.
Instance Uexp_mon2 : monotonic2 (o1:=Iord U) (o3:=Iord U) Uexp.
Save.
Definition UExp : U --m> (nat -m-> U) := mon2 Uexp.
Add Morphism Uexp with signature Oeq ==> eq ==> Oeq as Uexp_eq_compat.
Save.
Lemma Uexp_inv_S : forall x n, ([1-]x^(S n)) == x * ([1-]x^n)+[1-]x.
Lemma Uexp_lt_compat : forall p q n, (O<n)%nat -> p<q -> (p^n<q^n).
Hint Resolve Uexp_lt_compat.
Lemma Uexp_lt_zero : forall p n, (0<p) -> (0<p^n).
Hint Resolve Uexp_lt_zero.
Lemma Uexp_lt_one : forall p n, (0<n)%nat -> p<1 -> (p^n<1).
Hint Resolve Uexp_lt_one.
Lemma Uexp_lt_antimon: forall p n m,
(n<m)%nat-> 0 < p -> p < 1 -> p^m < p^n.
Hint Resolve Uexp_lt_antimon.
Lemma Udiv_mult : forall x y, ~ 0 == y -> x <= y -> (x/y) * y == x.
Hint Resolve Udiv_mult.
Lemma Umult_div_le : forall x y, y * (x / y) <= x.
Hint Resolve Umult_div_le.
Lemma Udiv_mult_le : forall x y, (x/y) * y <= x.
Hint Resolve Udiv_mult_le.
Lemma Udiv_le_compat_left : forall x y z, x <= y -> x/z <= y/z.
Hint Resolve Udiv_le_compat_left.
Lemma Udiv_eq_compat_left : forall x y z, x == y -> x/z == y/z.
Hint Resolve Udiv_eq_compat_left.
Lemma Umult_div_le_left : forall x y z, ~ 0==y -> x*y <= z -> x <= z/y.
Lemma Udiv_le_compat_right : forall x y z, ~ 0==y -> y <= z -> x/z <= x/y.
Hint Resolve Udiv_le_compat_right.
Lemma Udiv_eq_compat_right : forall x y z, y == z -> x/z == x/y.
Hint Resolve Udiv_eq_compat_right.
Add Morphism Udiv with signature Oeq ==> Oeq ==> Oeq as Udiv_eq_compat.
Save.
Add Morphism Udiv with signature Ole ++> Oeq ==> Ole as Udiv_le_compat.
Save.
Lemma Umult_div_eq : forall x y z, ~ 0 == y -> x * y == z -> x == z/y.
Lemma Umult_div_le_right : forall x y z, x <= y * z -> x/z <= y.
Lemma Udiv_le : forall x y, ~ 0 == y -> x <= x/y.
Lemma Udiv_zero : forall x, 0/x == 0.
Hint Resolve Udiv_zero.
Lemma Udiv_zero_eq : forall x y, 0 == x -> x/y == 0.
Hint Resolve Udiv_zero_eq.
Lemma Udiv_one : forall x, x/1 == x.
Hint Resolve Udiv_one.
Lemma Udiv_refl : forall x, ~ 0 == x -> x/x == 1.
Hint Resolve Udiv_refl.
Lemma Umult_div_assoc : forall x y z, y <= z-> (x * y) / z == x * (y/z).
Lemma Udiv_mult_assoc : forall x y z, x <= y * z -> x/(y * z) == (x/y)/z.
Lemma Udiv_inv : forall x y, ~ 0 == y -> [1-](x/y) <= ([1-]x)/y.
Lemma Uplus_div_inv : forall x y z, x+y <= z -> x<=[1-]y -> x/z <= [1-](y/z).
Hint Resolve Uplus_div_inv.
Lemma Udiv_plus_le : forall x y z, x/z + y/z <= (x+y)/z.
Hint Resolve Udiv_plus_le.
Lemma Udiv_plus : forall x y z, (x+y)/z == x/z + y/z.
Hint Resolve Udiv_plus.
Lemma Umult_div_simpl_r : forall x y, ~ 0 == y -> (x * y) / y == x.
Hint Resolve Umult_div_simpl_r.
Lemma Umult_div_simpl_l : forall x y, ~ 0 == x -> (x * y) / x == y.
Hint Resolve Umult_div_simpl_l.
Instance Udiv_mon : forall k, monotonic (fun x => (x/k)).
Save.
Definition UDiv (k:U) : U -m> U := mon (fun x => (x/k)).
Lemma UDiv_simpl : forall (k:U) x, UDiv k x = x/k.
Definition and properties of x & y
A conjonction operation which coincides with min and mult on 0 and 1, see Morgan & McIverDefinition Uesp (x y:U) := [1-] ([1-] x + [1-] y).
Infix "&" := Uesp (left associativity, at level 40) : U_scope.
Lemma Uinv_plus_esp : forall x y, [1-] (x + y) == [1-] x & [1-] y.
Hint Resolve Uinv_plus_esp.
Lemma Uinv_esp_plus : forall x y, [1-] (x & y) == [1-] x + [1-] y.
Hint Resolve Uinv_esp_plus.
Lemma Uesp_sym : forall x y : U, x & y == y & x.
Lemma Uesp_one_right : forall x : U, x & 1 == x.
Lemma Uesp_one_left : forall x : U, 1 & x == x.
Lemma Uesp_zero : forall x y, x <= [1-] y -> x & y == 0.
Hint Resolve Uesp_sym Uesp_one_right Uesp_one_left Uesp_zero.
Lemma Uesp_zero_right : forall x : U, x & 0 == 0.
Lemma Uesp_zero_left : forall x : U, 0 & x == 0.
Hint Resolve Uesp_zero_right Uesp_zero_left.
Add Morphism Uesp with signature Oeq ==> Oeq ==> Oeq as Uesp_eq_compat.
Save.
Lemma Uesp_le_compat : forall x y z t, x <= y -> z <=t -> x & z <= y &t .
Hint Immediate Uesp_le_compat Uesp_eq_compat.
Lemma Uesp_assoc : forall x y z, x & (y & z) == x & y & z.
Hint Resolve Uesp_assoc.
Lemma Uesp_zero_one_mult_left : forall x y, orc (x == 0) (x == 1) -> x & y == x * y.
Lemma Uesp_zero_one_mult_right : forall x y, orc (y == 0) (y == 1) -> x & y == x * y.
Hint Resolve Uesp_zero_one_mult_left Uesp_zero_one_mult_right.
Instance Uesp_mon : monotonic2 Uesp.
Save.
Definition UEsp : U -m> U -m> U := mon2 Uesp.
Lemma UEsp_simpl : forall x y, UEsp x y = x & y.
Lemma Uesp_le_left : forall x y, x & y <= x.
Lemma Uesp_le_right : forall x y, x & y <= y.
Hint Resolve Uesp_le_left Uesp_le_right.
Lemma Uesp_plus_inv : forall x y, [1-] y <= x -> x == x & y + [1-] y.
Hint Resolve Uesp_plus_inv.
Lemma Uesp_le_plus_inv : forall x y, x <= x & y + [1-] y.
Hint Resolve Uesp_le_plus_inv.
Lemma Uplus_inv_le_esp : forall x y z, x <= y + ([1-] z) -> x & z <= y.
Hint Immediate Uplus_inv_le_esp.
Lemma Ult_esp_left : forall x y z, x < z -> x & y < z.
Lemma Ult_esp_right : forall x y z, y < z -> x & y < z.
Hint Immediate Ult_esp_left Ult_esp_right.
Lemma Uesp_lt_compat_left : forall x y z, [1-]x <= z -> x < y -> x & z < y & z.
Hint Resolve Uesp_lt_compat_left.
Lemma Uesp_lt_compat_right : forall x y z, [1-]x <= y -> y < z -> x & y < x & z.
Hint Resolve Uesp_lt_compat_left.
Lemma Uesp_le_one_right : forall x y, [1-]x <= y -> (x <= x & y) -> y == 1.
Lemma Uesp_eq_one_right : forall x y, [1-]x <= y -> (x == x & y) -> y == 1.
Lemma Uesp_le_one_left : forall x y, [1-]x <= y -> y <= x & y -> x == 1.
Definition Uminus (x y:U) := [1-] ([1-] x + y).
Infix "-" := Uminus : U_scope.
Lemma Uminus_le_compat_left : forall x y z, x <= y -> x - z <= y - z.
Lemma Uminus_le_compat_right : forall x y z, y <= z -> x - z <= x - y.
Hint Resolve Uminus_le_compat_left Uminus_le_compat_right.
Lemma Uminus_le_compat : forall x y z t, x <= y -> t <= z -> x - z <= y - t.
Hint Immediate Uminus_le_compat.
Add Morphism Uminus with signature Oeq ==> Oeq ==> Oeq as Uminus_eq_compat.
Save.
Hint Immediate Uminus_eq_compat.
Lemma Uminus_zero_right : forall x, x - 0 == x.
Lemma Uminus_one_left : forall x, 1 - x == [1-] x.
Lemma Uminus_le_zero : forall x y, x <= y -> x - y == 0.
Hint Resolve Uminus_zero_right Uminus_one_left Uminus_le_zero.
Lemma Uminus_zero_left : forall x, 0 - x == 0.
Hint Resolve Uminus_zero_left.
Lemma Uminus_one_right : forall x, x - 1 == 0.
Hint Resolve Uminus_one_right.
Lemma Uminus_eq : forall x, x - x == 0.
Hint Resolve Uminus_eq.
Lemma Uminus_le_left : forall x y, x - y <= x.
Hint Resolve Uminus_le_left.
Lemma Uminus_le_inv : forall x y, x - y <= [1-]y.
Hint Resolve Uminus_le_inv.
Lemma Uminus_plus_simpl : forall x y, y <= x -> (x - y) + y == x.
Lemma Uminus_plus_zero : forall x y, x <= y -> (x - y) + y == y.
Hint Resolve Uminus_plus_simpl Uminus_plus_zero.
Lemma Uminus_plus_le : forall x y, x <= (x - y) + y.
Hint Resolve Uminus_plus_le.
Lemma Uesp_minus_distr_left : forall x y z, (x & y) - z == (x - z) & y.
Lemma Uesp_minus_distr_right : forall x y z, (x & y) - z == x & (y - z).
Hint Resolve Uesp_minus_distr_left Uesp_minus_distr_right.
Lemma Uesp_minus_distr : forall x y z t, (x & y) - (z + t) == (x - z) & (y - t).
Hint Resolve Uesp_minus_distr.
Lemma Uminus_esp_simpl_left : forall x y, [1-]x <= y -> x - (x & y) == [1-]y.
Lemma Uplus_esp_simpl : forall x y, (x - (x & y)) + y == x + y.
Hint Resolve Uminus_esp_simpl_left Uplus_esp_simpl.
Lemma Uplus_esp_simpl_right : forall x y, x + (y - (x & y)) == x + y.
Hint Resolve Uplus_esp_simpl_right.
Lemma Uminus_esp_le_inv : forall x y, x - (x & y) <= [1-]y.
Hint Resolve Uminus_esp_le_inv.
Lemma Uplus_esp_inv_simpl : forall x y, x <= [1-]y -> (x + y) & [1-]y == x.
Hint Resolve Uplus_esp_inv_simpl.
Lemma Uplus_inv_esp_simpl : forall x y, x <= y -> (x + [1-]y) & y == x.
Hint Resolve Uplus_inv_esp_simpl.
Definition max (x y : U) : U := (x - y) + y.
Lemma max_eq_left : forall x y : U, y <= x -> max x y == x.
Lemma max_eq_right : forall x y : U, x <= y -> max x y == y.
Hint Resolve max_eq_left max_eq_right.
Lemma max_eq_case : forall x y : U, orc (max x y == x) (max x y == y).
Add Morphism max with signature Oeq ==> Oeq ==> Oeq as max_eq_compat.
Save.
Lemma max_le_right : forall x y : U, x <= max x y.
Lemma max_le_left : forall x y : U, y <= max x y.
Hint Resolve max_le_right max_le_left.
Lemma max_le : forall x y z : U, x <= z -> y <= z -> max x y <= z.
Lemma max_le_compat : forall x y z t: U, x <= y -> z <= t -> max x z <= max y t.
Hint Immediate max_le_compat.
Lemma max_idem : forall x, max x x == x.
Hint Resolve max_idem.
Lemma max_sym_le : forall x y, max x y <= max y x.
Hint Resolve max_sym_le.
Lemma max_sym : forall x y, max x y == max y x.
Hint Resolve max_sym.
Lemma max_assoc : forall x y z, max x (max y z) == max (max x y) z.
Hint Resolve max_assoc.
Lemma max_0 : forall x, max 0 x == x.
Hint Resolve max_0.
Instance max_mon : monotonic2 max.
Save.
Definition Max : U -m> U -m> U := mon2 max.
Lemma max_eq_mult : forall k x y, max (k*x) (k*y) == k * max x y.
Lemma max_eq_plus_cte_right : forall x y k, max (x+k) (y+k) == (max x y) + k.
Hint Resolve max_eq_mult max_eq_plus_cte_right.
Definition min (x y : U) : U := [1-] ((y - x) + [1-]y).
Lemma min_eq_left : forall x y : U, x <= y -> min x y == x.
Lemma min_eq_right : forall x y : U, y <= x -> min x y == y.
Hint Resolve min_eq_right min_eq_left.
Lemma min_eq_case : forall x y : U, orc (min x y == x) (min x y == y).
Add Morphism min with signature Oeq ==> Oeq ==> Oeq as min_eq_compat.
Save.
Hint Immediate min_eq_compat.
Lemma min_le_right : forall x y : U, min x y <=x.
Lemma min_le_left : forall x y : U, min x y <= y.
Hint Resolve min_le_right min_le_left.
Lemma min_le : forall x y z : U, z <= x -> z <= y -> z <= min x y.
Lemma Uinv_min_max : forall x y, [1-](min x y)==max ([1-]x) ([1-]y).
Lemma Uinv_max_min : forall x y, [1-](max x y)==min ([1-]x) ([1-]y).
Lemma min_idem : forall x, min x x == x.
Lemma min_mult : forall x y k,
min (k * x) (k * y) == k * (min x y).
Hint Resolve min_mult.
Lemma min_plus : forall x1 x2 y1 y2,
(min x1 x2) + (min y1 y2) <= min (x1+y1) (x2+y2).
Hint Resolve min_plus.
Lemma min_plus_cte : forall x y k, min (x + k) (y + k) == (min x y) + k.
Hint Resolve min_plus_cte.
Lemma min_le_compat : forall x1 y1 x2 y2,
x1<=y1 -> x2 <=y2 -> min x1 x2 <= min y1 y2.
Hint Immediate min_le_compat.
Lemma min_sym_le : forall x y, min x y <= min y x.
Hint Resolve min_sym_le.
Lemma min_sym : forall x y, min x y == min y x.
Hint Resolve min_sym.
Lemma min_assoc : forall x y z, min x (min y z) == min (min x y) z.
Hint Resolve min_assoc.
Lemma min_0 : forall x, min 0 x == 0.
Hint Resolve min_0.
Instance min_mon2 : monotonic2 min.
Save.
Definition Min : U -m> U -m> U := mon2 min.
Lemma Min_simpl : forall x y, Min x y = min x y.
Lemma incr_decomp_aux : forall f g : nat -m> U,
forall n1 n2, (forall m, ~ ((n1<=m)%nat /\ f n1 <= g m))
-> (forall m, ~((n2<=m)%nat /\ g n2 <= f m)) -> (n1<=n2)%nat -> False.
Lemma incr_decomp : forall f g: nat -m> U,
orc (forall n, exc (fun m => (n<=m)%nat /\ f n <= g m))
(forall n, exc (fun m => (n<=m)%nat /\ g n <= f m)).
Lemma Uplus_minus_simpl_right : forall x y, y <= [1-] x -> (x + y) - y == x.
Hint Resolve Uplus_minus_simpl_right.
Lemma Uplus_minus_simpl_left : forall x y, y <= [1-] x -> (x + y) - x == y.
Lemma Uminus_assoc_left : forall x y z, (x - y) - z == x - (y + z).
Hint Resolve Uminus_assoc_left.
Lemma Uminus_perm : forall x y z, (x - y) - z == (x - z) - y.
Hint Resolve Uminus_perm.
Lemma Uminus_le_perm_left : forall x y z, y <= x -> x - y <= z -> x <= z + y.
Lemma Uplus_le_perm_left : forall x y z, x <= y + z -> x - y <= z.
Lemma Uminus_eq_perm_left : forall x y z, y <= x -> x - y == z -> x == z + y.
Lemma Uplus_eq_perm_left : forall x y z, y <= [1-] z -> x == y + z -> x - y == z.
Hint Resolve Uminus_le_perm_left Uminus_eq_perm_left.
Hint Resolve Uplus_le_perm_left Uplus_eq_perm_left.
Lemma Uminus_le_perm_right : forall x y z, z <= y -> x <= y - z -> x + z <= y.
Lemma Uplus_le_perm_right : forall x y z, z <= [1-] x -> x + z <= y -> x <= y - z.
Hint Resolve Uminus_le_perm_right Uplus_le_perm_right.
Lemma Uminus_le_perm : forall x y z, z <= y -> x <= [1-] z -> x <= y - z -> z <= y - x.
Hint Resolve Uminus_le_perm.
Lemma Uminus_eq_perm_right : forall x y z, z <= y -> x == y - z -> x + z == y.
Hint Resolve Uminus_eq_perm_right.
Lemma Uminus_plus_perm : forall x y z, y <= x -> z <= [1-]x -> (x - y) + z == (x + z) - y.
Lemma Uminus_zero_le : forall x y, x - y == 0 -> x <= y.
Lemma Uminus_lt_non_zero : forall x y, x < y -> ~ 0 == y - x.
Hint Immediate Uminus_zero_le Uminus_lt_non_zero.
Lemma Ult_le_nth_minus : forall x y, x < y -> exc (fun n => x <= y - [1/]1+n).
Lemma Uinv_plus_minus_left : forall x y, [1-](x + y) == [1-]x - y.
Lemma Uinv_plus_minus_right : forall x y, [1-](x + y) == [1-]y - x.
Hint Resolve Uinv_plus_minus_left Uinv_plus_minus_right.
Lemma Ult_le_nth_plus : forall x y, x < y -> exc (fun n : nat => x + [1/]1+n <= y).
Lemma Uminus_distr_left : forall x y z, (x - y) * z == (x * z) - (y * z).
Hint Resolve Uminus_distr_left.
Lemma Uminus_distr_right : forall x y z, x * (y - z) == (x * y) - (x * z).
Hint Resolve Uminus_distr_right.
Lemma Uminus_assoc_right : forall x y z, y <= x -> z <= y -> x - (y - z) == (x - y) + z.
Lemma Uplus_minus_assoc_right : forall x y z,
y <= [1-]x -> z <= y -> x + (y - z) == (x + y) - z.
Hint Resolve Uplus_minus_assoc_right.
Lemma Uplus_minus_assoc_le : forall x y z, (x + y) - z <= x + (y - z).
Hint Resolve Uplus_minus_assoc_le.
Lemma Udiv_minus : forall x y z, ~0 == z -> x <= z -> (x - y) / z == x/z - y/z.
Lemma Umult_inv_minus : forall x y, x * [1-]y == x - x * y.
Hint Resolve Umult_inv_minus.
Lemma Uinv_mult_minus : forall x y, ([1-]x) * y == y - x * y.
Hint Resolve Uinv_mult_minus.
Lemma Uminus_plus_perm_right : forall x y z, y <= x -> y <= z -> (x - y) + z == x + (z - y).
Hint Resolve Uminus_plus_perm_right.
Lemma Uminus_plus_simpl_mid :
forall x y z, z <= x -> y <= z -> x - y == (x - z) + (z - y).
Hint Resolve Uminus_plus_simpl_mid.
Hint Resolve Uplus_minus_simpl_right.
Lemma Uplus_minus_simpl_left : forall x y, y <= [1-] x -> (x + y) - x == y.
Lemma Uminus_assoc_left : forall x y z, (x - y) - z == x - (y + z).
Hint Resolve Uminus_assoc_left.
Lemma Uminus_perm : forall x y z, (x - y) - z == (x - z) - y.
Hint Resolve Uminus_perm.
Lemma Uminus_le_perm_left : forall x y z, y <= x -> x - y <= z -> x <= z + y.
Lemma Uplus_le_perm_left : forall x y z, x <= y + z -> x - y <= z.
Lemma Uminus_eq_perm_left : forall x y z, y <= x -> x - y == z -> x == z + y.
Lemma Uplus_eq_perm_left : forall x y z, y <= [1-] z -> x == y + z -> x - y == z.
Hint Resolve Uminus_le_perm_left Uminus_eq_perm_left.
Hint Resolve Uplus_le_perm_left Uplus_eq_perm_left.
Lemma Uminus_le_perm_right : forall x y z, z <= y -> x <= y - z -> x + z <= y.
Lemma Uplus_le_perm_right : forall x y z, z <= [1-] x -> x + z <= y -> x <= y - z.
Hint Resolve Uminus_le_perm_right Uplus_le_perm_right.
Lemma Uminus_le_perm : forall x y z, z <= y -> x <= [1-] z -> x <= y - z -> z <= y - x.
Hint Resolve Uminus_le_perm.
Lemma Uminus_eq_perm_right : forall x y z, z <= y -> x == y - z -> x + z == y.
Hint Resolve Uminus_eq_perm_right.
Lemma Uminus_plus_perm : forall x y z, y <= x -> z <= [1-]x -> (x - y) + z == (x + z) - y.
Lemma Uminus_zero_le : forall x y, x - y == 0 -> x <= y.
Lemma Uminus_lt_non_zero : forall x y, x < y -> ~ 0 == y - x.
Hint Immediate Uminus_zero_le Uminus_lt_non_zero.
Lemma Ult_le_nth_minus : forall x y, x < y -> exc (fun n => x <= y - [1/]1+n).
Lemma Uinv_plus_minus_left : forall x y, [1-](x + y) == [1-]x - y.
Lemma Uinv_plus_minus_right : forall x y, [1-](x + y) == [1-]y - x.
Hint Resolve Uinv_plus_minus_left Uinv_plus_minus_right.
Lemma Ult_le_nth_plus : forall x y, x < y -> exc (fun n : nat => x + [1/]1+n <= y).
Lemma Uminus_distr_left : forall x y z, (x - y) * z == (x * z) - (y * z).
Hint Resolve Uminus_distr_left.
Lemma Uminus_distr_right : forall x y z, x * (y - z) == (x * y) - (x * z).
Hint Resolve Uminus_distr_right.
Lemma Uminus_assoc_right : forall x y z, y <= x -> z <= y -> x - (y - z) == (x - y) + z.
Lemma Uplus_minus_assoc_right : forall x y z,
y <= [1-]x -> z <= y -> x + (y - z) == (x + y) - z.
Hint Resolve Uplus_minus_assoc_right.
Lemma Uplus_minus_assoc_le : forall x y z, (x + y) - z <= x + (y - z).
Hint Resolve Uplus_minus_assoc_le.
Lemma Udiv_minus : forall x y z, ~0 == z -> x <= z -> (x - y) / z == x/z - y/z.
Lemma Umult_inv_minus : forall x y, x * [1-]y == x - x * y.
Hint Resolve Umult_inv_minus.
Lemma Uinv_mult_minus : forall x y, ([1-]x) * y == y - x * y.
Hint Resolve Uinv_mult_minus.
Lemma Uminus_plus_perm_right : forall x y z, y <= x -> y <= z -> (x - y) + z == x + (z - y).
Hint Resolve Uminus_plus_perm_right.
Lemma Uminus_plus_simpl_mid :
forall x y z, z <= x -> y <= z -> x - y == (x - z) + (z - y).
Hint Resolve Uminus_plus_simpl_mid.
- triangular inequality
Lemma Uminus_triangular : forall x y z, x - y <= (x - z) + (z - y).
Hint Resolve Uminus_triangular.
Lemma Uesp_plus_right_perm : forall x y z,
x <= [1-] y -> y <= [1-] z -> x & (y + z) == (x + y) & z.
Hint Resolve Uesp_plus_right_perm.
Lemma Uplus_esp_assoc : forall x y z,
x <= [1-]y -> [1-]z <= y -> x + (y & z) == (x + y) & z.
Hint Resolve Uplus_esp_assoc.
Lemma Uesp_plus_left_perm : forall x y z,
[1-]x <= y -> [1-]z <= y -> x & y <= [1-] z -> (x & y) + z == x + (y & z).
Hint Resolve Uesp_plus_left_perm.
Lemma Uesp_plus_left_perm_le : forall x y z,
[1-]x <= y -> [1-]z <= y -> (x & y) + z <= x + (y & z).
Hint Resolve Uesp_plus_left_perm_le.
Lemma Uesp_plus_assoc : forall x y z,
[1-]x <= y -> y <= [1-]z -> x & (y + z) == (x & y) + z.
Hint Resolve Uesp_plus_assoc.
Lemma Uminus_assoc_right_perm : forall x y z,
x <= [1-] z -> z <= y -> x - (y - z) == x + z - y.
Hint Resolve Uminus_assoc_right_perm.
Lemma Uminus_lt_left : forall x y, ~ 0 == x -> ~ 0 == y -> x - y < x.
Hint Resolve Uminus_lt_left.
Lemma Uesp_mult_le :
forall x y z, [1-]x <= y -> x * z <= [1-](y * z)
-> (x & y) * z == x * z + y * z - z.
Hint Resolve Uesp_mult_le.
Lemma Uesp_mult_ge :
forall x y z, [1-]x <= y -> [1-](x * z) <= y * z
-> (x & y) * z == (x * z) & (y * z) + [1-]z.
Hint Resolve Uesp_mult_ge.
Definition sigma : (nat -> U) -> nat -m> U.
Defined.
Lemma sigma_0 : forall (f : nat -> U), sigma f O == 0.
Lemma sigma_S : forall (f :nat -> U) (n:nat), sigma f (S n) = (f n) + (sigma f n).
Lemma sigma_1 : forall (f : nat -> U), sigma f (S 0) == f O.
Lemma sigma_incr : forall (f : nat -> U) (n m:nat), (n <= m)%nat -> sigma f n <= sigma f m.
Hint Resolve sigma_incr.
Lemma sigma_eq_compat : forall (f g: nat -> U) (n:nat),
(forall k, (k < n)%nat -> f k == g k) -> sigma f n == sigma g n.
Lemma sigma_le_compat : forall (f g: nat -> U) (n:nat),
(forall k, (k < n)%nat -> f k <= g k) -> sigma f n <= sigma g n.
Lemma sigma_S_lift : forall (f :nat -> U) (n:nat),
sigma f (S n) == (f O) + (sigma (fun k => f (S k)) n).
Lemma sigma_plus_lift : forall (f :nat -> U) (n m:nat),
sigma f (n+m)%nat == sigma f n + sigma (fun k => f (n+k)%nat) m.
Lemma sigma_zero : forall f n,
(forall k, (k<n)%nat -> f k == 0) -> sigma f n == 0.
Lemma sigma_not_zero : forall f n k, (k<n)%nat -> 0 < f k -> 0 < sigma f n.
Lemma sigma_zero_elim : forall f n,
(sigma f n) == 0 -> forall k, (k<n)%nat -> f k == 0.
Hint Resolve sigma_eq_compat sigma_le_compat sigma_zero.
Lemma sigma_le : forall f n k, (k<n)%nat -> f k <= sigma f n.
Hint Resolve sigma_le.
Lemma sigma_minus_decr : forall f n, (forall k, f (S k) <= f k) ->
sigma (fun k => f k - f (S k)) n == f O - f n.
Lemma sigma_minus_incr : forall f n, (forall k, f k <= f (S k)) ->
sigma (fun k => f (S k) - f k) n == f n - f O.
Definition prod (alpha : nat -> U) (n:nat) := compn Umult 1 alpha n.
Lemma prod_0 : forall (f : nat -> U), prod f 0 = 1.
Lemma prod_S : forall (f :nat -> U) (n:nat), prod f (S n) = (f n) * (prod f n).
Lemma prod_1 : forall (f : nat -> U), prod f (S 0) == f O.
Lemma prod_S_lift : forall (f :nat -> U) (n:nat),
prod f (S n) == (f O) * (prod (fun k => f (S k)) n).
Lemma prod_decr : forall (f : nat -> U) (n m:nat), (n <= m)%nat -> prod f m <= prod f n.
Hint Resolve prod_decr.
Lemma prod_eq_compat : forall (f g: nat -> U) (n:nat),
(forall k, (k < n)%nat -> f k == g k) -> (prod f n) == (prod g n).
Lemma prod_le_compat : forall (f g: nat -> U) (n:nat),
(forall k, (k < n)%nat -> f k <= g k) -> prod f n <= prod g n.
Lemma prod_zero : forall f n k, (k<n)%nat -> f k ==0 -> prod f n==0.
Lemma prod_not_zero : forall f n,
(forall k, (k<n)%nat -> 0 < f k) -> 0 < prod f n.
Lemma prod_zero_elim : forall f n,
prod f n == 0 -> exc (fun k => (k<n)%nat /\ f k ==0).
Hint Resolve prod_eq_compat prod_le_compat prod_not_zero.
Lemma prod_le : forall f n k, (k<n)%nat -> prod f n <= f k.
Lemma prod_minus : forall f n, prod f n - prod f (S n) == ([1-]f n) * prod f n.
Definition Prod : (nat -> U) -> nat -m-> U.
Defined.
Lemma Prod_simpl : forall f n, Prod f n = prod f n.
Hint Resolve Prod_simpl.
Lemma Unth_eq_compat : forall n m, n = m -> [1/]1+n == [1/]1+m.
Hint Resolve Unth_eq_compat.
Lemma Unth_zero : [1/]1+0 == 1.
Notation "½" := (Unth 1).
Lemma Unth_one : ½ == [1-] ½.
Hint Resolve Unth_zero Unth_one.
Lemma Unth_one_plus : ½ + ½ == 1.
Hint Resolve Unth_one_plus.
Lemma Unth_one_refl : forall t, ½ * t + ½ * t == t.
Lemma Unth_not_null : forall n, ~ (0 == [1/]1+n).
Hint Resolve Unth_not_null.
Lemma Unth_lt_zero : forall n, 0 < [1/]1+n.
Hint Resolve Unth_lt_zero.
Lemma Unth_inv_lt_one : forall n, [1-][1/]1+n<1.
Hint Resolve Unth_inv_lt_one.
Lemma Unth_not_one : forall n, ~ (1 == [1-][1/]1+n).
Hint Resolve Unth_not_one.
Lemma Unth_prop_sigma : forall n, [1/]1+n == [1-] (sigma (fun k => [1/]1+n) n).
Hint Resolve Unth_prop_sigma.
Lemma Unth_sigma_n : forall n : nat, ~ (1 == sigma (fun k => [1/]1+n) n).
Lemma Unth_sigma_Sn : forall n : nat, 1 == sigma (fun k => [1/]1+n) (S n).
Hint Resolve Unth_sigma_n Unth_sigma_Sn.
Lemma Unth_decr : forall n m, (n < m)%nat -> [1/]1+m < [1/]1+n.
Hint Resolve Unth_decr.
Lemma Unth_decr_S : forall n, [1/]1+(S n) < [1/]1+n.
Hint Resolve Unth_decr_S.
Lemma Unth_le_compat :
forall n m, (n <= m)%nat -> [1/]1+m <= [1/]1+n.
Hint Resolve Unth_le_compat.
Lemma Unth_le_equiv :
forall n m, [1/]1+n <= [1/]1+m <-> (m <= n)%nat.
Lemma Unth_eq_equiv :
forall n m, [1/]1+n == [1/]1+m <-> (m = n)%nat.
Lemma Unth_le_half : forall n, [1/]1+(S n) <= ½.
Hint Resolve Unth_le_half.
Lemma Unth_lt_one : forall n, [1/]1+(S n) < 1.
Hint Resolve Unth_lt_one.
Definition mean (x y:U) := ½ * x + ½ * y.
Lemma mean_eq : forall x:U, mean x x ==x.
Lemma mean_le_compat_right : forall x y z, y <= z -> mean x y <= mean x z.
Lemma mean_le_compat_left : forall x y z, x <= y -> mean x z <= mean y z.
Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.
Lemma mean_lt_compat_right : forall x y z, y < z -> mean x y < mean x z.
Lemma mean_lt_compat_left : forall x y z, x < y -> mean x z < mean y z.
Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.
Hint Resolve mean_lt_compat_left mean_lt_compat_right.
Lemma mean_le_up : forall x y, x <= y -> mean x y <= y.
Lemma mean_le_down : forall x y, x <= y -> x <= mean x y.
Lemma mean_lt_up : forall x y, x < y -> mean x y < y.
Lemma mean_lt_down : forall x y, x < y -> x < mean x y.
Hint Resolve mean_le_up mean_le_down mean_lt_up mean_lt_down.
Lemma mean_eq : forall x:U, mean x x ==x.
Lemma mean_le_compat_right : forall x y z, y <= z -> mean x y <= mean x z.
Lemma mean_le_compat_left : forall x y z, x <= y -> mean x z <= mean y z.
Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.
Lemma mean_lt_compat_right : forall x y z, y < z -> mean x y < mean x z.
Lemma mean_lt_compat_left : forall x y z, x < y -> mean x z < mean y z.
Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.
Hint Resolve mean_lt_compat_left mean_lt_compat_right.
Lemma mean_le_up : forall x y, x <= y -> mean x y <= y.
Lemma mean_le_down : forall x y, x <= y -> x <= mean x y.
Lemma mean_lt_up : forall x y, x < y -> mean x y < y.
Lemma mean_lt_down : forall x y, x < y -> x < mean x y.
Hint Resolve mean_le_up mean_le_down mean_lt_up mean_lt_down.
Lemma le_half_inv : forall x, x <= ½ -> x <= [1-] x.
Hint Immediate le_half_inv.
Lemma ge_half_inv : forall x, ½ <= x -> [1-] x <= x.
Hint Immediate ge_half_inv.
Lemma Uinv_le_half_left : forall x, x <= ½ -> ½ <= [1-] x.
Lemma Uinv_le_half_right : forall x, ½ <= x -> [1-] x <= ½.
Hint Resolve Uinv_le_half_left Uinv_le_half_right.
Lemma half_twice : forall x, x <= ½ -> ½ * (x + x) == x.
Lemma half_twice_le : forall x, ½ * (x + x) <= x.
Lemma Uinv_half : forall x, ½ * ([1-] x) + ½ == [1-] ( ½ * x ).
Lemma Uinv_half_plus : forall x, [1-]x + ½ * x == [1-] ( ½ * x ).
Lemma half_esp :
forall x, (½ <= x) -> (½) * (x & x) + ½ == x.
Lemma half_esp_le : forall x, x <= ½ * (x & x) + ½.
Hint Resolve half_esp_le.
Lemma half_le : forall x y, y <= [1-] y -> x <= y + y -> (½) * x <= y.
Lemma half_Unth_le: forall n, ½ * ([1/]1+n) <= [1/]1+(S n).
Hint Resolve half_le half_Unth_le.
Lemma half_exp : forall n, ½^n == ½^(S n) + ½^(S n).
Definition diff (x y:U) := (x - y) + (y - x).
Lemma diff_eq : forall x, diff x x == 0.
Hint Resolve diff_eq.
Lemma diff_sym : forall x y, diff x y == diff y x.
Hint Resolve diff_sym.
Lemma diff_zero : forall x, diff x 0 == x.
Hint Resolve diff_zero.
Add Morphism diff with signature Oeq ==> Oeq ==> Oeq as diff_eq_compat.
Qed.
Hint Immediate diff_eq_compat.
Lemma diff_plus_ok : forall x y, x - y <= [1-](y - x).
Hint Resolve diff_plus_ok.
Lemma diff_Uminus : forall x y, x <= y -> diff x y == y - x.
Lemma diff_Uplus_le : forall x y, x <= diff x y + y.
Hint Resolve diff_Uplus_le.
Lemma diff_triangular : forall x y z, diff x y <= diff x z + diff y z.
Hint Resolve diff_triangular.
Lemma Ule_lt_lim : forall x y, (forall t, t < x -> t <= y) -> x <= y.
Lemma Ule_nth_lim : forall x y, (forall p, x <= y + [1/]1+p) -> x <= y.
Lemma Ule_nth_lim : forall x y, (forall p, x <= y + [1/]1+p) -> x <= y.
Lemma lub_un : mlub (cte nat 1) == 1.
Hint Resolve lub_un.
Lemma UPlusk_eq : forall k, UPlus k == mon (Uplus k).
Lemma UMultk_eq : forall k, UMult k == mon (Umult k).
Lemma UPlus_continuous_right : forall k, continuous (UPlus k).
Hint Resolve UPlus_continuous_right.
Lemma UPlus_continuous_left : continuous UPlus.
Hint Resolve UPlus_continuous_left.
Lemma UMult_continuous_right : forall k, continuous (UMult k).
Hint Resolve UMult_continuous_right.
Lemma UMult_continuous_left : continuous UMult.
Hint Resolve UMult_continuous_left.
Lemma lub_eq_plus_cte_left : forall (f:nat -m> U) (k:U), lub ((UPlus k) @ f) == k + lub f.
Hint Resolve lub_eq_plus_cte_left.
Lemma lub_eq_mult : forall (k:U) (f:nat -m> U), lub ((UMult k) @ f) == k * lub f.
Hint Resolve lub_eq_mult.
Lemma lub_eq_plus_cte_right : forall (f : nat -m> U) (k:U),
lub ((mshift UPlus k) @ f) == lub f + k.
Hint Resolve lub_eq_plus_cte_right.
Lemma min_lub_le : forall f g : nat -m> U,
lub ((Min @2 f) g) <= min (lub f) (lub g).
Lemma min_lub_le_incr_aux : forall f g : nat -m> U,
(forall n, exc (fun m => (n<=m)%nat /\ f n <= g m))
-> min (lub f) (lub g) <= lub ((Min @2 f) g).
Lemma min_lub_le_incr : forall f g : nat -m> U,
min (lub f) (lub g) <= lub ((Min @2 f) g).
Lemma min_continuous2 : continuous2 Min.
Hint Resolve min_continuous2.
Lemma lub_eq_esp_right :
forall (f : nat -m> U) (k : U), lub ((mshift UEsp k) @ f) == lub f & k.
Hint Resolve lub_eq_esp_right.
Lemma Udiv_continuous : forall (k:U), continuous (UDiv k).
Hint Resolve Udiv_continuous.
Definition glb (f:nat -m-> U) := [1-](lub (UInv @ f)).
Lemma glb_le: forall (f : nat -m-> U) (n : nat), glb f <= (f n).
Lemma le_glb: forall (f : nat -m-> U) (x:U),
(forall n : nat, x <= f n) -> x <= glb f.
Hint Resolve glb_le le_glb.
Definition Uopp : cpo (o:=Iord U) U.
Defined.
Lemma Uopp_lub_simpl
: forall h : nat -m-> U, lub (cpo:=Uopp) h = glb h.
Lemma Uopp_mon_seq : forall f:nat -m-> U,
forall n m:nat, (n <= m)%nat -> f m <= f n.
Hint Resolve Uopp_mon_seq.
Infinite product: Π(i=0..∞) f i
Properties of glb
Lemma glb_le_compat:
forall f g : nat -m-> U, (forall x, f x <= g x) -> glb f <= glb g.
Hint Resolve glb_le_compat.
Lemma glb_eq_compat:
forall f g : nat -m-> U, f == g -> glb f == glb g.
Hint Resolve glb_eq_compat.
Lemma glb_cte: forall c : U, glb (mon (cte nat (o1:=(Iord U)) c)) == c.
Hint Resolve glb_cte.
Lemma glb_eq_plus_cte_right:
forall (f : nat -m-> U) (k : U), glb (Imon (mshift UPlus k) @ f) == glb f + k.
Hint Resolve glb_eq_plus_cte_right.
Lemma glb_eq_plus_cte_left:
forall (f : nat -m-> U) (k : U), glb (Imon (UPlus k) @ f) == k + glb f.
Hint Resolve glb_eq_plus_cte_left.
Lemma glb_eq_mult:
forall (k : U) (f : nat -m-> U), glb (Imon (UMult k) @ f) == k * glb f.
Lemma Imon2_plus_continuous
: continuous2 (c1:=Uopp) (c2:=Uopp) (c3:=Uopp) (imon2 Uplus).
Hint Resolve Imon2_plus_continuous.
Lemma Uinv_continuous : continuous (c1:=Uopp) UInv.
Lemma Uinv_lub_eq : forall f : nat -m-> U, [1-](lub (cpo:=Uopp) f) == lub (UInv@f).
Lemma Uinvopp_mon : monotonic (o2:= Iord U) Uinv.
Hint Resolve Uinvopp_mon.
Definition UInvopp : U -m-> U
:= mon (o2:= Iord U) Uinv (fmonotonic:=Uinvopp_mon).
Lemma UInvopp_simpl : forall x, UInvopp x = [1-]x.
Lemma Uinvopp_continuous : continuous (c2:=Uopp) UInvopp.
Lemma Uinvopp_lub_eq
: forall f : nat -m> U, [1-](lub f) == lub (cpo:=Uopp) (UInvopp@f).
Hint Resolve Uinv_continuous Uinvopp_continuous.
Instance Uminus_mon2 : monotonic2 (o2:=Iord U) Uminus.
Save.
Definition UMinus : U -m> U --m> U := mon2 Uminus.
Lemma UMinus_simpl : forall x y, UMinus x y = x - y.
Lemma Uminus_continuous2 : continuous2 (c2:=Uopp) UMinus.
Hint Resolve Uminus_continuous2.
Lemma glb_le_esp : forall f g :nat -m-> U, (glb f) & (glb g) <= glb ((imon2 Uesp @2 f) g).
Hint Resolve glb_le_esp.
Lemma Uesp_min : forall a1 a2 b1 b2, min a1 b1 & min a2 b2 <= min (a1 & a2) (b1 & b2).
Defining lubs of arbitrary sequences
Fixpoint seq_max (f:nat -> U) (n:nat) : U := match n with
O => f O | S p => max (seq_max f p) (f (S p)) end.
Lemma seq_max_incr : forall f n, seq_max f n <= seq_max f (S n).
Hint Resolve seq_max_incr.
Lemma seq_max_le : forall f n, f n <= seq_max f n.
Hint Resolve seq_max_le.
Instance seq_max_mon : forall (f:nat -> U), monotonic (seq_max f).
Save.
Definition sMax (f:nat -> U) : nat -m> U := mon (seq_max f).
Lemma sMax_mult : forall k (f:nat->U), sMax (fun n => k * f n) == UMult k @ sMax f.
Lemma sMax_plus_cte_right : forall k (f:nat-> U),
sMax (fun n => f n + k) == mshift UPlus k @ sMax f.
Definition Ulub (f:nat -> U) := lub (sMax f).
Lemma le_Ulub : forall f n, f n <= Ulub f.
Lemma Ulub_le : forall f x, (forall n, f n <= x) -> Ulub f <= x.
Hint Resolve le_Ulub Ulub_le.
Lemma Ulub_le_compat : forall f g : nat->U, f <= g -> Ulub f <= Ulub g.
Hint Resolve Ulub_le_compat.
Add Morphism Ulub with signature Oeq ==> Oeq as Ulub_eq_compat.
Save.
Hint Resolve Ulub_eq_compat.
Lemma Ulub_eq_mult : forall k (f:nat->U), Ulub (fun n => k * f n)== k * Ulub f.
Lemma Ulub_eq_plus_cte_right : forall (f:nat->U) k, Ulub (fun n => f n + k)== Ulub f + k.
Hint Resolve Ulub_eq_mult Ulub_eq_plus_cte_right.
Lemma Ulub_eq_esp_right :
forall (f : nat -> U) (k : U), Ulub (fun n => f n & k) == Ulub f & k.
Hint Resolve lub_eq_esp_right.
Lemma Ulub_le_plus : forall f g, Ulub (fun n => f n + g n) <= Ulub f + Ulub g.
Hint Resolve Ulub_le_plus.
Definition Uglb (f:nat -> U) :U := [1-]Ulub (fun n => [1-](f n)).
Lemma Uglb_le: forall (f : nat -> U) (n : nat), Uglb f <= f n.
Lemma le_Uglb: forall (f : nat -> U) (x:U),
(forall n : nat, x <= f n) -> x <= Uglb f.
Hint Resolve Uglb_le le_Uglb.
Lemma Uglb_le_compat : forall f g : nat -> U, f <= g -> Uglb f <= Uglb g.
Hint Resolve Uglb_le_compat.
Add Morphism Uglb with signature Oeq ==> Oeq as Uglb_eq_compat.
Save.
Hint Resolve Uglb_eq_compat.
Lemma Uglb_eq_plus_cte_right:
forall (f : nat -> U) (k : U), Uglb (fun n => f n + k) == Uglb f + k.
Hint Resolve Uglb_eq_plus_cte_right.
Lemma Uglb_eq_mult:
forall (k : U) (f : nat -> U), Uglb (fun n => k * f n) == k * Uglb f.
Hint Resolve Uglb_eq_mult Uglb_eq_plus_cte_right.
Lemma Uglb_le_plus : forall f g, Uglb f + Uglb g <= Uglb (fun n => f n + g n).
Hint Resolve Uglb_le_plus.
Lemma Ulub_lub : forall f:nat -m> U, Ulub f == lub f.
Hint Resolve Ulub_lub.
Lemma Uglb_glb : forall f:nat -m-> U, Uglb f == glb f.
Hint Resolve Uglb_glb.
Lemma Uglb_glb_mon : forall (f:nat -> U) {Hf:monotonic (o2:=Iord U) f}, Uglb f == glb (mon f).
Hint Resolve @Uglb_glb_mon.
Lemma lub_le_plus : forall (f g : nat -m> U), lub ((UPlus @2 f) g) <= lub f + lub g.
Hint Resolve lub_le_plus.
Lemma glb_le_plus : forall (f g:nat -m-> U) , glb f + glb g <= glb ((Imon2 UPlus @2 f) g).
Hint Resolve glb_le_plus.
Lemma lub_eq_plus : forall f g : nat -m> U, lub ((UPlus @2 f) g) == lub f + lub g.
Hint Resolve lub_eq_plus.
Lemma glb_mon : forall f : nat -m> U, Uglb f == f O.
Lemma lub_inv : forall (f g : nat -m> U), (forall n, f n <= [1-] g n) -> lub f <= [1-] (lub g).
Lemma glb_lift_left : forall (f:nat -m-> U) n,
glb f == glb (mon (seq_lift_left f n)).
Hint Resolve glb_lift_left.
Lemma Ulub_mon : forall f : nat -m-> U, Ulub f == f O.
Lemma lub_glb_le : forall (f:nat -m> U) (g:nat -m-> U),
(forall n, f n <= g n) -> lub f <= glb g.
Lemma lub_lub_inv_le : forall f g :nat -m> U,
(forall n, f n <= [1-]g n) -> lub f <= [1-] lub g.
Lemma Uplus_opp_continuous_right :
forall k, continuous (c1:=Uopp) (c2:=Uopp) (Imon (UPlus k)).
Lemma Uplus_opp_continuous_left :
continuous (c1:=Uopp) (c2:=fmon_cpo (o:=Iord U) (c:=Uopp))(Imon2 UPlus).
Hint Resolve Uplus_opp_continuous_right Uplus_opp_continuous_left.
Instance Uplusopp_continuous2 : continuous2 (c1:=Uopp) (c2:=Uopp) (c3:=Uopp) (Imon2 UPlus).
Save.
Lemma Uplusopp_lub_eq : forall (f g : nat -m-> U),
lub (cpo:=Uopp) f + lub (cpo:=Uopp) g == lub (cpo:=Uopp) ((Imon2 UPlus @2 f) g).
Lemma glb_eq_plus : forall (f g : nat -m-> U), glb ((Imon2 UPlus @2 f) g) == glb f + glb g.
Hint Resolve glb_eq_plus.
Instance UEsp_continuous2 : continuous2 UEsp.
Save.
Lemma Uesp_lub_eq : forall f g : nat -m> U, lub f & lub g == lub ((UEsp @2 f) g).
Instance sigma_mon :monotonic sigma.
Save.
Definition Sigma : (nat -> U) -m> nat-m> U
:= mon sigma (fmonotonic:=sigma_mon).
Lemma Sigma_simpl : forall f, Sigma f = sigma f.
Lemma sigma_continuous1 : continuous Sigma.
Lemma sigma_lub1 : forall (f : nat -m> (nat -> U)) n,
sigma (lub f) n == lub ((mshift Sigma n) @ f).
Definition MF (A:Type) : Type := A -> U.
Definition MFcpo (A:Type) : cpo (MF A) := fcpo cpoU.
Definition MFopp (A:Type) : cpo (o:=Iord (A -> U)) (MF A).
Defined.
Lemma MFopp_lub_eq : forall (A:Type) (h:nat-m-> MF A),
lub (cpo:=MFopp A) h == fun x => glb (Iord_app x @ h).
Lemma fle_intro : forall (A:Type) (f g : MF A), (forall x, f x <= g x) -> f <= g.
Hint Resolve fle_intro.
Lemma feq_intro : forall (A:Type) (f g : MF A), (forall x, f x == g x) -> f == g.
Hint Resolve feq_intro.
Definition fplus (A:Type) (f g : MF A) : MF A :=
fun x => f x + g x.
Definition fmult (A:Type) (k:U) (f : MF A) : MF A :=
fun x => k * f x.
Definition finv (A:Type) (f : MF A) : MF A :=
fun x => [1-] f x.
Definition fzero (A:Type) : MF A :=
fun x => 0.
Definition fdiv (A:Type) (k:U) (f : MF A) : MF A :=
fun x => (f x) / k.
Definition flub (A:Type) (f : nat -m> MF A) : MF A := lub f.
Lemma fplus_simpl : forall (A:Type)(f g : MF A) (x : A),
fplus f g x = f x + g x.
Lemma fplus_def : forall (A:Type)(f g : MF A),
fplus f g = fun x => f x + g x.
Lemma fmult_simpl : forall (A:Type)(k:U) (f : MF A) (x : A),
fmult k f x = k * f x.
Lemma fmult_def : forall (A:Type)(k:U) (f : MF A),
fmult k f = fun x => k * f x.
Lemma fdiv_simpl : forall (A:Type)(k:U) (f : MF A) (x : A),
fdiv k f x = f x / k.
Lemma fdiv_def : forall (A:Type)(k:U) (f : MF A),
fdiv k f = fun x => f x / k.
Implicit Arguments fzero [].
Lemma fzero_simpl : forall (A:Type)(x : A), fzero A x = 0.
Lemma fzero_def : forall (A:Type), fzero A = fun x:A => 0.
Lemma finv_simpl : forall (A:Type)(f : MF A) (x : A), finv f x = [1-]f x.
Lemma finv_def : forall (A:Type)(f : MF A), finv f = fun x => [1-](f x).
Lemma flub_simpl : forall (A:Type)(f:nat -m> MF A) (x:A),
(flub f) x = lub (f <o> x).
Lemma flub_def : forall (A:Type)(f:nat -m> MF A),
(flub f) = fun x => lub (f <o> x).
Hint Resolve fplus_simpl fmult_simpl fzero_simpl finv_simpl flub_simpl.
Definition fone (A:Type) : MF A := fun x => 1.
Implicit Arguments fone [].
Lemma fone_simpl : forall (A:Type) (x:A), fone A x = 1.
Lemma fone_def : forall (A:Type), fone A = fun (x:A) => 1.
Definition fcte (A:Type) (k:U): MF A := fun x => k.
Implicit Arguments fcte [].
Lemma fcte_simpl : forall (A:Type) (k:U) (x:A), fcte A k x = k.
Lemma fcte_def : forall (A:Type) (k:U), fcte A k = fun (x:A) => k.
Definition fminus (A:Type) (f g :MF A) : MF A := fun x => f x - g x.
Lemma fminus_simpl : forall (A:Type) (f g: MF A) (x:A), fminus f g x = f x - g x.
Lemma fminus_def : forall (A:Type) (f g: MF A), fminus f g = fun x => f x - g x.
Definition fesp (A:Type) (f g :MF A) : MF A := fun x => f x & g x.
Lemma fesp_simpl : forall (A:Type) (f g: MF A) (x:A), fesp f g x = f x & g x.
Lemma fesp_def : forall (A:Type) (f g: MF A) , fesp f g = fun x => f x & g x.
Definition fconj (A:Type)(f g:MF A) : MF A := fun x => f x * g x.
Lemma fconj_simpl : forall (A:Type) (f g: MF A) (x:A), fconj f g x = f x * g x.
Lemma fconj_def : forall (A:Type) (f g: MF A), fconj f g = fun x => f x * g x.
Lemma MF_lub_simpl : forall (A:Type) (f : nat -m> MF A) (x:A),
lub f x = lub (f <o>x).
Hint Resolve MF_lub_simpl.
Lemma MF_lub_def : forall (A:Type) (f : nat -m> MF A),
lub f = fun x => lub (f <o>x).
Lemma fplus_eq_compat : forall A (f1 f2 g1 g2:MF A),
f1==f2 -> g1==g2 -> fplus f1 g1 == fplus f2 g2.
Add Parametric Morphism (A:Type) : (@fplus A)
with signature Oeq ==> Oeq ==> Oeq
as fplus_feq_compat_morph.
Save.
Instance fplus_mon2 : forall A, monotonic2 (fplus (A:=A)).
Save.
Hint Resolve fplus_mon2.
Lemma fplus_le_compat : forall A (f1 f2 g1 g2:MF A),
f1<=f2 -> g1<=g2 -> fplus f1 g1 <= fplus f2 g2.
Add Parametric Morphism A : (@fplus A) with signature Ole ++> Ole ++> Ole
as fplus_fle_compat_morph.
Save.
Lemma finv_eq_compat : forall A (f g:MF A), f==g -> finv f == finv g.
Add Parametric Morphism A : (@finv A) with signature Oeq ==> Oeq
as finv_feq_compat_morph.
Save.
Instance finv_mon : forall A, monotonic (o2:=Iord (MF A)) (finv (A:=A)).
Save.
Hint Resolve finv_mon.
Lemma finv_le_compat : forall A (f g:MF A), f <= g -> finv g <= finv f.
Add Parametric Morphism A: (@finv A)
with signature Ole --> Ole as finv_fle_compat_morph.
Save.
Lemma fmult_eq_compat : forall A k1 k2 (f1 f2:MF A),
k1 == k2 -> f1 == f2 -> fmult k1 f1 == fmult k2 f2.
Add Parametric Morphism A : (@fmult A)
with signature Oeq ==> Oeq ==> Oeq as fmult_feq_compat_morph.
Save.
Instance fmult_mon2 : forall A, monotonic2 (fmult (A:=A)).
Save.
Hint Resolve fmult_mon2.
Lemma fmult_le_compat : forall A k1 k2 (f1 f2:MF A),
k1 <= k2 -> f1 <= f2 -> fmult k1 f1 <= fmult k2 f2.
Add Parametric Morphism A : (@fmult A)
with signature Ole ++> Ole ++> Ole as fmult_fle_compat_morph.
Save.
Lemma fminus_eq_compat : forall A (f1 f2 g1 g2:MF A),
f1 == f2 -> g1 == g2 -> fminus f1 g1 == fminus f2 g2.
Add Parametric Morphism A : (@fminus A)
with signature Oeq ==> Oeq ==> Oeq as fminus_feq_compat_morph.
Save.
Instance fminus_mon2 : forall A, monotonic2 (o2:=Iord (MF A)) (fminus (A:=A)).
Save.
Hint Resolve fminus_mon2.
Lemma fminus_le_compat : forall A (f1 f2 g1 g2:MF A),
f1 <= f2 -> g2 <= g1 -> fminus f1 g1 <= fminus f2 g2.
Add Parametric Morphism A : (@fminus A)
with signature Ole ++> Ole --> Ole as fminus_fle_compat_morph.
Save.
Lemma fesp_eq_compat : forall A (f1 f2 g1 g2:MF A),
f1==f2 -> g1==g2 -> fesp f1 g1 == fesp f2 g2.
Add Parametric Morphism A : (@fesp A) with signature Oeq ==> Oeq ==> Oeq as fesp_feq_compat_morph.
Save.
Instance fesp_mon2 : forall A, monotonic2 (fesp (A:=A)).
Save.
Hint Resolve fesp_mon2.
Lemma fesp_le_compat : forall A (f1 f2 g1 g2:MF A),
f1<=f2 -> g1<=g2 -> fesp f1 g1 <= fesp f2 g2.
Add Parametric Morphism A : (@fesp A)
with signature Ole ++> Ole ++> Ole as fesp_fle_compat_morph.
Save.
Lemma fconj_eq_compat : forall A (f1 f2 g1 g2:MF A),
f1==f2 -> g1==g2 -> fconj f1 g1 == fconj f2 g2.
Add Parametric Morphism A : (@fconj A)
with signature Oeq ==> Oeq ==> Oeq
as fconj_feq_compat_morph.
Save.
Instance fconj_mon2 : forall A, monotonic2 (fconj (A:=A)).
Save.
Hint Resolve fconj_mon2.
Lemma fconj_le_compat : forall A (f1 f2 g1 g2:MF A),
f1 <= f2 -> g1 <= g2 -> fconj f1 g1 <= fconj f2 g2.
Add Parametric Morphism A : (@fconj A) with signature Ole ++> Ole ++> Ole
as fconj_fle_compat_morph.
Save.
Hint Immediate fplus_le_compat fplus_eq_compat fesp_le_compat fesp_eq_compat
fmult_le_compat fmult_eq_compat fminus_le_compat fminus_eq_compat
fconj_eq_compat.
Hint Resolve finv_eq_compat.
Lemma fle_fplus_left : forall (A:Type) (f g : MF A), f <= fplus f g.
Lemma fle_fplus_right : forall (A:Type) (f g : MF A), g <= fplus f g.
Lemma fle_fmult : forall (A:Type) (k:U)(f : MF A), fmult k f <= f.
Lemma fle_zero : forall (A:Type) (f : MF A), fzero A <= f.
Lemma fle_one : forall (A:Type) (f : MF A), f <= fone A.
Lemma feq_finv_finv : forall (A:Type) (f : MF A), finv (finv f) == f.
Lemma fle_fesp_left : forall (A:Type) (f g : MF A), fesp f g <= f.
Lemma fle_fesp_right : forall (A:Type) (f g : MF A), fesp f g <= g.
Lemma fle_fconj_left : forall (A:Type) (f g : MF A), fconj f g <= f.
Lemma fle_fconj_right : forall (A:Type) (f g : MF A), fconj f g <= g.
Lemma fconj_decomp : forall A (f g : MF A),
f == fplus (fconj f g) (fconj f (finv g)).
Hint Resolve fconj_decomp.
Definition fplusok (A:Type) (f g : MF A) := f <= finv g.
Hint Unfold fplusok.
Lemma fplusok_sym : forall (A:Type) (f g : MF A) , fplusok f g -> fplusok g f.
Hint Immediate fplusok_sym.
Lemma fplusok_inv : forall (A:Type) (f : MF A) , fplusok f (finv f).
Hint Resolve fplusok_inv.
Lemma fplusok_le_compat : forall (A:Type)(f1 f2 g1 g2:MF A),
fplusok f2 g2 -> f1 <= f2 -> g1 <= g2 -> fplusok f1 g1.
Hint Resolve fle_fplus_left fle_fplus_right fle_zero fle_one feq_finv_finv finv_le_compat
fle_fmult fle_fesp_left fle_fesp_right fle_fconj_left fle_fconj_right.
Lemma fconj_fplusok : forall (A:Type)(f g h:MF A),
fplusok g h -> fplusok (fconj f g) (fconj f h).
Hint Resolve fconj_fplusok.
Definition Fconj A : MF A -m> MF A -m> MF A := mon2 (fconj (A:=A)).
Lemma Fconj_simpl : forall A f g, Fconj A f g = fconj f g.
Lemma fconj_sym : forall A (f g : MF A), fconj f g == fconj g f.
Hint Resolve fconj_sym.
Lemma Fconj_sym : forall A (f g : MF A), Fconj A f g == Fconj A g f.
Hint Resolve Fconj_sym.
Lemma lub_MF_simpl : forall A (h : nat -m> MF A) (x:A), lub h x = lub (h <o> x).
Instance fconj_continuous2 A : continuous2 (Fconj A).
Save.
Definition Fmult A : U -m> MF A -m> MF A := mon2 (fmult (A:=A)).
Lemma Fmult_simpl : forall A k f, Fmult A k f = fmult k f.
Lemma Fmult_simpl2 : forall A k f x, Fmult A k f x = k * (f x).
Lemma fmult_continuous2 : forall A, continuous2 (Fmult A).
Lemma Umult_sym_cst:
forall A : Type,
forall (k : U) (f : MF A), (fun x : A => f x * k) == (fun x : A => k * f x).
Section FixDef.
Variable A :Type.
Variable F : MF A -m> MF A.
Definition mufix : MF A := fixp F.
Definition G : MF A --m-> MF A := Imon F.
Definition nufix : MF A := fixp (c:=MFopp A) G.
Lemma mufix_inv : forall f : MF A, F f <= f -> mufix <= f.
Hint Resolve mufix_inv.
Lemma nufix_inv : forall f :MF A, f <= F f -> f <= nufix.
Hint Resolve nufix_inv.
Lemma mufix_le : mufix <= F mufix.
Hint Resolve mufix_le.
Lemma nufix_sup : F nufix <= nufix.
Hint Resolve nufix_sup.
Lemma mufix_eq : continuous F -> mufix == F mufix.
Hint Resolve mufix_eq.
Lemma nufix_eq : continuous (c1:=MFopp A) (c2:=MFopp A) G -> nufix == F nufix.
Hint Resolve nufix_eq.
End FixDef.
Hint Resolve mufix_le mufix_eq nufix_sup nufix_eq.
Definition Fcte (A:Type) (f:MF A) : MF A -m> MF A := mon (cte (MF A) f).
Lemma mufix_cte : forall (A:Type) (f:MF A), mufix (Fcte f) == f.
Lemma nufix_cte : forall (A:Type) (f:MF A), nufix (Fcte f) == f.
Hint Resolve mufix_cte nufix_cte.
Variable A :Type.
Variable F : MF A -m> MF A.
Definition mufix : MF A := fixp F.
Definition G : MF A --m-> MF A := Imon F.
Definition nufix : MF A := fixp (c:=MFopp A) G.
Lemma mufix_inv : forall f : MF A, F f <= f -> mufix <= f.
Hint Resolve mufix_inv.
Lemma nufix_inv : forall f :MF A, f <= F f -> f <= nufix.
Hint Resolve nufix_inv.
Lemma mufix_le : mufix <= F mufix.
Hint Resolve mufix_le.
Lemma nufix_sup : F nufix <= nufix.
Hint Resolve nufix_sup.
Lemma mufix_eq : continuous F -> mufix == F mufix.
Hint Resolve mufix_eq.
Lemma nufix_eq : continuous (c1:=MFopp A) (c2:=MFopp A) G -> nufix == F nufix.
Hint Resolve nufix_eq.
End FixDef.
Hint Resolve mufix_le mufix_eq nufix_sup nufix_eq.
Definition Fcte (A:Type) (f:MF A) : MF A -m> MF A := mon (cte (MF A) f).
Lemma mufix_cte : forall (A:Type) (f:MF A), mufix (Fcte f) == f.
Lemma nufix_cte : forall (A:Type) (f:MF A), nufix (Fcte f) == f.
Hint Resolve mufix_cte nufix_cte.
Lemma Uinv_bary :
forall a b x y : U, a <= [1-]b ->
[1-] (a * x + b * y) == a * [1-] x + b * [1-] y + [1-] (a + b).
Hint Resolve Uinv_bary.
Lemma Uinv_bary_le :
forall a b x y : U, a <= [1-]b -> a * [1-] x + b * [1-] y <= [1-] (a * x + b * y).
Hint Resolve Uinv_bary_le.
Lemma Uinv_bary_eq : forall a b x y : U, a == [1-]b ->
[1-] (a * x + b * y) == a * [1-] x + b * [1-] y.
Hint Resolve Uinv_bary_eq.
Lemma bary_refl_eq : forall a b x, a == [1-]b -> a * x + b * x == x.
Hint Resolve bary_refl_eq.
Lemma bary_refl_feq : forall A a b (f:A -> U) ,
a == [1-]b -> (fun x => a * f x + b * f x) == f.
Hint Resolve bary_refl_feq.
Lemma bary_le_left : forall a b x y, [1-]b <= a -> x <= y -> x <= a * x + b * y.
Lemma bary_le_right : forall a b x y, a <= [1-]b -> x <= y -> a * x + b * y <= y.
Hint Resolve bary_le_left bary_le_right.
Lemma bary_up_eq : forall a b x y : U, a == [1-]b -> x <= y -> a * x + b * y == x + b * (y - x).
Lemma bary_up_le : forall a b x y : U, a <= [1-]b -> a * x + b * y <= x + b * (y - x).
Lemma bary_anti_mon : forall a b a' b' x y : U,
a == [1-]b -> a' == [1-]b' -> a <= a' -> x <= y -> a' * x + b' * y <= a * x + b * y.
Hint Resolve bary_anti_mon.
Lemma bary_Uminus_left :
forall a b x y : U, a <= [1-]b -> (a * x + b * y) - x <= b * (y - x).
Lemma bary_Uminus_left_eq :
forall a b x y : U, a == [1-]b -> x <= y -> (a * x + b * y) - x == b * (y - x).
Lemma Uminus_bary_left
: forall a b x y : U, [1-]a <= b -> x - (a * x + b * y) <= b * (x - y).
Lemma Uminus_bary_left_eq
: forall a b x y : U, a == [1-]b -> y <= x -> x - (a * x + b * y) == b * (x - y).
Hint Resolve bary_up_eq bary_up_le bary_Uminus_left Uminus_bary_left bary_Uminus_left_eq Uminus_bary_left_eq.
Lemma bary_le_simpl_right
: forall a b x y : U, a == [1-]b -> ~ 0 == a -> a * x + b * y <= y -> x <= y.
Lemma bary_le_simpl_left
: forall a b x y : U, a == [1-]b -> ~ 0 == b -> x <= a * x + b * y -> x <= y.
Lemma diff_bary_left_eq
: forall a b x y : U, a == [1-]b -> diff x (a * x + b * y) == b * diff x y.
Hint Resolve diff_bary_left_eq.
Lemma Uinv_half_bary :
forall x y : U, [1-] (½ * x + ½ * y) == ½ * [1-] x + ½ * [1-] y.
Hint Resolve Uinv_half_bary.
Lemma Uinv_Umult : forall x y, [1-]x * [1-]y == [1-](x-x*y+y).
Hint Resolve Uinv_Umult.
Lemma sigma_plus : forall (f g : nat -> U) (n:nat),
sigma (fun k => (f k) + (g k)) n == sigma f n + sigma g n.
Definition retract (f : nat -> U) (n : nat) := forall k, (k < n)%nat -> f k <= [1-] (sigma f k).
Lemma retract_class : forall f n, class (retract f n).
Hint Resolve retract_class.
Lemma retract0 : forall (f : nat -> U), retract f 0.
Lemma retract_pred : forall (f : nat -> U) (n : nat), retract f (S n) -> retract f n.
Lemma retractS: forall (f : nat -> U) (n : nat), retract f (S n) -> f n <= [1-] (sigma f n).
Hint Immediate retract_pred retractS.
Lemma retractS_inv :
forall (f : nat -> U) (n : nat), retract f (S n) -> sigma f n <= [1-] f n.
Hint Immediate retractS_inv.
Lemma retractS_intro: forall (f : nat -> U) (n : nat),
retract f n -> f n <= [1-] (sigma f n) -> retract f (S n).
Hint Resolve retract0 retractS_intro.
Lemma retract_lt : forall (f : nat -> U) (n : nat), sigma f n < 1 -> retract f n.
Lemma retract_unif :
forall (f : nat -> U) (n : nat),
(forall k, (k<=n)%nat -> f k <= [1/]1+n) -> retract f (S n).
Hint Resolve retract_unif.
Lemma retract_unif_Nnth :
forall (f : nat -> U) (n : nat),
(forall k : nat, (k <= n)%nat -> f k <= [1/]n) -> retract f n.
Hint Resolve retract_unif_Nnth.
Lemma sigma_mult :
forall (f : nat -> U) n c, retract f n -> sigma (fun k => c * (f k)) n == c * (sigma f n).
Hint Resolve sigma_mult.
Lemma sigma_mult_perm :
forall (f : nat -> U) n c1 c2, retract (fun k => c1 * (f k)) n -> retract (fun k => c2 * (f k)) n
-> c1 * (sigma (fun k => c2 * (f k)) n) == c2 * (sigma (fun k => c1 * (f k)) n).
Hint Resolve sigma_mult_perm.
Lemma sigma_prod_maj : forall (f g : nat -> U) n,
sigma (fun k => (f k) * (g k)) n <= sigma f n.
Hint Resolve sigma_prod_maj.
Lemma sigma_prod_le : forall (f g : nat -> U) (c:U), (forall k, (f k) <= c)
-> forall n, retract g n -> sigma (fun k => (f k) * (g k)) n <= c * (sigma g n).
Lemma sigma_prod_ge : forall (f g : nat -> U) (c:U), (forall k, c <= (f k))
-> forall n, (retract g n) -> c * (sigma g n) <= (sigma (fun k => (f k) * (g k)) n).
Hint Resolve sigma_prod_maj sigma_prod_le sigma_prod_ge.
Lemma sigma_inv : forall (f g : nat -> U) (n:nat), (retract f n) ->
[1-] (sigma (fun k => f k * g k) n) == (sigma (fun k => f k * [1-] (g k)) n) + [1-] (sigma f n).
Lemma sigma_inv_simpl : forall (n:nat) (f: nat -> U),
sigma (fun i => [1/]1+n * [1-] (f i)) (S n) == [1-] sigma (fun i => [1/]1+n * (f i)) (S n).
Fixpoint Nmult (n: nat) (x : U) {struct n} : U :=
match n with O => 0 | (S O) => x | S p => x + (Nmult p x) end.
match n with O => 0 | (S O) => x | S p => x + (Nmult p x) end.
Definition Nmult_def (n: nat) (x : U) :=
match n with O => True | S p => x <= [1/]1+p end.
Lemma Nmult_def_O : forall x, Nmult_def O x.
Hint Resolve Nmult_def_O.
Lemma Nmult_def_1 : forall x, Nmult_def (S O) x.
Hint Resolve Nmult_def_1.
Lemma Nmult_def_intro : forall n x , x <= [1/]1+n -> Nmult_def (S n) x.
Hint Resolve Nmult_def_intro.
Lemma Nmult_def_Unth_le : forall n m, (n <= S m)%nat -> Nmult_def n ([1/]1+m).
Hint Resolve Nmult_def_Unth_le.
Lemma Nmult_def_le : forall n m x, (n <= S m)%nat -> x <= [1/]1+m -> Nmult_def n x.
Hint Resolve Nmult_def_le.
Lemma Nmult_def_Unth: forall n , Nmult_def (S n) ([1/]1+n).
Hint Resolve Nmult_def_Unth.
Lemma Nmult_def_Nnth : forall n, Nmult_def n ([1/]n).
Hint Resolve Nmult_def_Nnth.
Lemma Nmult_def_pred : forall n x, Nmult_def (S n) x -> Nmult_def n x.
Hint Immediate Nmult_def_pred.
Lemma Nmult_defS : forall n x, Nmult_def (S n) x -> x <= [1/]1+n.
Hint Immediate Nmult_defS.
Lemma Nmult_def_class : forall n p, class (Nmult_def n p).
Hint Resolve Nmult_def_class.
Infix "*/" := Nmult (at level 60) : U_scope.
Add Morphism Nmult_def with signature eq ==> Oeq ==> iff as Nmult_def_eq_compat.
Save.
Lemma Nmult_def_zero : forall n, Nmult_def n 0.
Hint Resolve Nmult_def_zero.
match n with O => True | S p => x <= [1/]1+p end.
Lemma Nmult_def_O : forall x, Nmult_def O x.
Hint Resolve Nmult_def_O.
Lemma Nmult_def_1 : forall x, Nmult_def (S O) x.
Hint Resolve Nmult_def_1.
Lemma Nmult_def_intro : forall n x , x <= [1/]1+n -> Nmult_def (S n) x.
Hint Resolve Nmult_def_intro.
Lemma Nmult_def_Unth_le : forall n m, (n <= S m)%nat -> Nmult_def n ([1/]1+m).
Hint Resolve Nmult_def_Unth_le.
Lemma Nmult_def_le : forall n m x, (n <= S m)%nat -> x <= [1/]1+m -> Nmult_def n x.
Hint Resolve Nmult_def_le.
Lemma Nmult_def_Unth: forall n , Nmult_def (S n) ([1/]1+n).
Hint Resolve Nmult_def_Unth.
Lemma Nmult_def_Nnth : forall n, Nmult_def n ([1/]n).
Hint Resolve Nmult_def_Nnth.
Lemma Nmult_def_pred : forall n x, Nmult_def (S n) x -> Nmult_def n x.
Hint Immediate Nmult_def_pred.
Lemma Nmult_defS : forall n x, Nmult_def (S n) x -> x <= [1/]1+n.
Hint Immediate Nmult_defS.
Lemma Nmult_def_class : forall n p, class (Nmult_def n p).
Hint Resolve Nmult_def_class.
Infix "*/" := Nmult (at level 60) : U_scope.
Add Morphism Nmult_def with signature eq ==> Oeq ==> iff as Nmult_def_eq_compat.
Save.
Lemma Nmult_def_zero : forall n, Nmult_def n 0.
Hint Resolve Nmult_def_zero.
Lemma Nmult_0 : forall (x:U), O */ x = 0.
Lemma Nmult_1 : forall (x:U), (S O) */ x = x.
Lemma Nmult_zero : forall n, n */ 0 == 0.
Lemma Nmult_SS : forall (n:nat) (x:U), S (S n) */ x = x + (S n */ x).
Lemma Nmult_2 : forall (x:U), 2 */ x = x + x.
Lemma Nmult_S : forall (n:nat) (x:U), S n */ x == x + (n */ x).
Hint Resolve Nmult_0 Nmult_zero Nmult_1 Nmult_SS Nmult_2 Nmult_S.
Add Morphism Nmult with signature eq ==> Oeq ==> Oeq as Nmult_eq_compat.
Save.
Hint Immediate Nmult_eq_compat.
Lemma Nmult_eq_compat_left : forall (n:nat) (x y:U), x == y -> n */ x == n */ y.
Lemma Nmult_eq_compat_right : forall (n m:nat) (x:U), (n = m)%nat -> n */ x == m */ x.
Hint Resolve Nmult_eq_compat_right.
Lemma Nmult_le_compat_right : forall n x y, x <= y -> n */ x <= n */ y.
Lemma Nmult_le_compat_left : forall n m x, (n <= m)%nat -> n */ x <= m */ x.
Hint Resolve Nmult_eq_compat_right Nmult_le_compat_right Nmult_le_compat_left.
Lemma Nmult_le_compat : forall (n m:nat) x y, n <= m -> x <= y -> n */ x <= m */ y.
Hint Immediate Nmult_le_compat.
Instance Nmult_mon2 : monotonic2 Nmult.
Save.
Definition NMult : nat -m> U -m> U :=mon2 Nmult.
Lemma Nmult_sigma : forall (n:nat) (x:U), n */ x == sigma (fun k => x) n.
Hint Resolve Nmult_sigma.
Lemma Nmult_Unth_prop : forall n:nat, [1/]1+n == [1-] (n*/ ([1/]1+n)).
Hint Resolve Nmult_Unth_prop.
Lemma Nmult_n_Unth: forall n:nat, n */ [1/]1+n == [1-] ([1/]1+n).
Lemma Nmult_Sn_Unth: forall n:nat, S n */ [1/]1+n == 1.
Hint Resolve Nmult_n_Unth Nmult_Sn_Unth.
Lemma Nmult_ge_Sn_Unth: forall n k, (S n <= k)%nat -> k */ [1/]1+n == 1.
Lemma Nmult_n_Nnth : forall n : nat, (0 < n)%nat -> n */ [1/]n == 1.
Hint Resolve Nmult_n_Nnth.
Lemma Nnth_S : forall n, [1/](S n) == [1/]1+n.
Lemma Nmult_le_n_Unth: forall n k, (k <= n)%nat -> k */ [1/]1+n <= [1-] ([1/]1+n).
Hint Resolve Nmult_ge_Sn_Unth Nmult_le_n_Unth.
Lemma Nmult_def_inv : forall n x, Nmult_def (S n) x -> n */ x <= [1-] x.
Hint Resolve Nmult_def_inv.
Lemma Nmult_Umult_assoc_left : forall n x y, Nmult_def n x -> n */ (x*y) == (n */ x) *y.
Hint Resolve Nmult_Umult_assoc_left.
Lemma Nmult_Umult_assoc_right : forall n x y, Nmult_def n y -> n */ (x*y) == x * (n */ y).
Hint Resolve Nmult_Umult_assoc_right.
Lemma plus_Nmult_distr : forall n m x, (n + m) */ x== (n */ x) + (m */ x).
Lemma Nmult_Uplus_distr : forall n x y, n */ (x + y) == (n */ x) + (n */ y).
Lemma Nmult_mult_assoc : forall n m x, (n * m) */ x == n */ (m */ x).
Lemma Nmult_Unth_simpl_left : forall n x, (S n) */ ([1/]1+n * x) == x.
Lemma Nmult_Unth_simpl_right : forall n x, (S n) */ (x * [1/]1+n) == x.
Hint Resolve Nmult_Umult_assoc_right plus_Nmult_distr Nmult_Uplus_distr
Nmult_mult_assoc Nmult_Unth_simpl_left Nmult_Unth_simpl_right.
Lemma Uinv_Nmult : forall k n, [1-] (k */ [1/]1+n) == ((S n) - k) */ [1/]1+n.
Lemma Nmult_neq_zero : forall n x, ~0==x -> ~0==S n */ x.
Hint Resolve Nmult_neq_zero.
Lemma Nmult_le_simpl : forall (n:nat) (x y:U),
Nmult_def (S n) x -> Nmult_def (S n) y -> (S n */ x) <= (S n */ y) -> x <= y.
Lemma Nmult_Unth_le : forall (n1 n2 m1 m2:nat),
(n2 * S n1<= m2 * S m1)%nat -> n2 */ [1/]1+m1 <= m2 */ [1/]1+n1.
Lemma Nmult_Unth_eq :
forall (n1 n2 m1 m2:nat),
(n2 * S n1= m2 * S m1)%nat -> n2 */ [1/]1+m1 == m2 */ [1/]1+n1.
Hint Resolve Nmult_Unth_le Nmult_Unth_eq.
Lemma Nmult_Unth_factor :
forall (n m1 m2:nat),
(n * S m2= S m1)%nat -> n */ [1/]1+m1 == [1/]1+m2.
Hint Resolve Nmult_Unth_factor.
Lemma Unth_eq : forall n p, n */ p == [1-]p -> p == [1/]1+n.
Lemma mult_Nmult_Umult : forall n m x y,
Nmult_def n x -> Nmult_def m y -> (n*m)%nat */ (x*y) == (n*/x)*(m*/y).
Hint Resolve mult_Nmult_Umult.
Lemma minus_Nmult_distr : forall n m x,
Nmult_def n x -> (n - m) */ x== (n */ x) - (m */ x).
Lemma Nmult_Uminus_distr : forall n x y,
Nmult_def n x -> n */ (x - y) == (n */ x) - (n */ y).
Hint Resolve minus_Nmult_distr Nmult_Uminus_distr.
Lemma Umult_Unth : forall n m, [1/]1+n * [1/]1+m == [1/]1+(n+m+n*m).
Hint Resolve Umult_Unth.
Lemma Umult_Nnth : forall n m,
(0 < n)%nat -> (0 < m)%nat -> [1/]n * [1/]m == [1/](n*m)%nat.
Hint Resolve Umult_Nnth.
Lemma Nnth_le_compat : forall n m, (n <= m)%nat -> [1/]m <= [1/]n.
Hint Resolve Nnth_le_compat.
Lemma Nnth_le_equiv : forall n m, (0 < n)%nat -> (0 < m)%nat -> ([1/]n <= [1/]m <-> m <= n).
Lemma Nnth_eq_equiv : forall n m, (0 < n)%nat -> (0 < m)%nat -> ([1/]n == [1/]m <-> m = n).
Lemma half_Unth_eq : forall n, ½ * [1/]1+n == [1/]1+(2*n+1).
Lemma twice_half : forall p, [1/]1+(2 * p + 1) + [1/]1+(2 * p + 1) == [1/]1+p.
Lemma Nmult_def_lt : forall n x, n */ x < 1 -> Nmult_def n x.
Hint Immediate Nmult_def_lt.
Lemma Nmult_lt_simpl : forall n x y, n */ x < n */ y -> x < y.
Lemma Nmult_lt_compat :
forall n x y, (0 < n)%nat -> n */ x < 1 -> x < y -> n */ x < n */ y.
Hint Resolve Nmult_lt_compat.
Lemma Nmult_def_lt_compat :
forall n x y, (0 < n)%nat -> Nmult_def n y -> x < y -> n */ x < n */ y.
Hint Resolve Nmult_def_lt_compat.
Definition B2U :MF bool := fun (b:bool) => if b then 1 else 0.
Definition NB2U :MF bool := fun (b:bool) => if b then 0 else 1.
Lemma B2Uinv : NB2U == finv B2U.
Lemma NB2Uinv : B2U == finv NB2U.
Hint Resolve B2Uinv NB2Uinv.
Lemma Umult_B2U_andb : forall x y, (B2U x) * (B2U y) == B2U (andb x y).
Lemma Uplus_B2U_orb : forall x y, (B2U x) + (B2U y) == B2U (orb x y).
Definition pmin (p:U) (n:nat) := p - ( ½ ^ n ).
Add Morphism pmin with signature Oeq ==> eq ==> Oeq as pmin_eq_compat.
Save.
Lemma pmin_esp_S : forall p n, pmin (p & p) n == pmin p (S n) & pmin p (S n).
Lemma pmin_esp_le : forall p n, pmin p (S n) <= ½ * (pmin (p & p) n) + ½.
Lemma pmin_plus_eq : forall p n, p <= ½ -> pmin p (S n) == ½ * (pmin (p + p) n).
Lemma pmin_0 : forall p:U, pmin p O == 0.
Lemma pmin_le : forall (p:U) (n:nat), p - ([1/]1+n) <= pmin p n.
Hint Resolve pmin_0 pmin_le.
Lemma pmin_le_compat : forall p (n m : nat), n <= m -> pmin p n <= pmin p m.
Hint Resolve pmin_le_compat.
Instance pmin_mon : forall p, monotonic (pmin p).
Save.
Definition Pmin (p:U) :nat -m> U := mon (pmin p).
Lemma le_p_lim_pmin : forall p, p <= lub (Pmin p).
Lemma le_lim_pmin_p : forall p, lub (Pmin p) <= p.
Hint Resolve le_p_lim_pmin le_lim_pmin_p.
Lemma eq_lim_pmin_p : forall p, lub (Pmin p) == p.
Hint Resolve eq_lim_pmin_p.
Lemma pmin_esp_le : forall p n, pmin p (S n) <= ½ * (pmin (p & p) n) + ½.
Lemma pmin_plus_eq : forall p n, p <= ½ -> pmin p (S n) == ½ * (pmin (p + p) n).
Lemma pmin_0 : forall p:U, pmin p O == 0.
Lemma pmin_le : forall (p:U) (n:nat), p - ([1/]1+n) <= pmin p n.
Hint Resolve pmin_0 pmin_le.
Lemma pmin_le_compat : forall p (n m : nat), n <= m -> pmin p n <= pmin p m.
Hint Resolve pmin_le_compat.
Instance pmin_mon : forall p, monotonic (pmin p).
Save.
Definition Pmin (p:U) :nat -m> U := mon (pmin p).
Lemma le_p_lim_pmin : forall p, p <= lub (Pmin p).
Lemma le_lim_pmin_p : forall p, lub (Pmin p) <= p.
Hint Resolve le_p_lim_pmin le_lim_pmin_p.
Lemma eq_lim_pmin_p : forall p, lub (Pmin p) == p.
Hint Resolve eq_lim_pmin_p.
Particular case where p = 1
Definition U1min := Pmin 1.
Lemma eq_lim_U1min : lub U1min == 1.
Lemma U1min_S : forall n, U1min (S n) == ½*(U1min n) + ½.
Lemma U1min_0 : U1min O == 0.
Hint Resolve eq_lim_U1min U1min_S U1min_0.
Lemma glb_half_exp : glb (UExp ½) == 0.
Hint Resolve glb_half_exp.
Lemma Ule_lt_half_exp : forall x y, (forall p, x <= y + ½^p) -> x <= y.
Lemma half_exp_le_half : forall p, ½^(S p) <= ½.
Hint Resolve half_exp_le_half.
Lemma twice_half_exp : forall p, ½^(S p) + ½^(S p) == ½^p.
Hint Resolve twice_half_exp.
Fixpoint exp2 (n:nat) : nat :=
match n with O => (1%nat) | S p => (2 * (exp2 p))%nat end.
Lemma exp2_pos : forall n, (O < exp2 n)%nat.
Hint Resolve exp2_pos.
Lemma S_pred_exp2 : forall n, S (pred (exp2 n))=exp2 n.
Hint Resolve S_pred_exp2.
Notation "k /2^ p" := (k */ (½)^p) (at level 35, no associativity).
Lemma Unth_half : forall n, (O<n)%nat -> [1/]1+(pred (n+n)) == ½ * [1/]1+pred n.
Lemma Unth_exp2 : forall p, ½^p == [1/]1+pred (exp2 p).
Hint Resolve Unth_exp2.
Lemma Nmult_exp2 : forall p, (exp2 p)/2^p == 1.
Hint Resolve Nmult_exp2.
Section Sequence.
Variable k : U.
Hypothesis kless1 : k < 1.
Lemma Ult_one_inv_zero : ~ 0 == [1-]k.
Hint Resolve Ult_one_inv_zero.
Lemma Umult_simpl_zero : forall x, x <= k * x -> x == 0.
Lemma Umult_simpl_one : forall x, k * x + [1-]k <= x -> x == 1.
Lemma bary_le_compat : forall k' x y, x <= y -> k <= k' -> k' * x + [1-]k' * y <= k * x + [1-]k * y.
Lemma bary_one_le_compat : forall k' x, k <= k' -> k' * x + [1-]k' <= k * x + [1-]k.
Lemma glb_exp_0 : glb (UExp k) == 0.
Instance Uinvexp_mon : monotonic (fun n => [1-]k ^ n).
Save.
Lemma lub_inv_exp_1 : mlub (fun n => [1-]k ^ n) == 1.
End Sequence.
Hint Resolve glb_exp_0 lub_inv_exp_1 bary_one_le_compat bary_le_compat.
match n with O => (1%nat) | S p => (2 * (exp2 p))%nat end.
Lemma exp2_pos : forall n, (O < exp2 n)%nat.
Hint Resolve exp2_pos.
Lemma S_pred_exp2 : forall n, S (pred (exp2 n))=exp2 n.
Hint Resolve S_pred_exp2.
Notation "k /2^ p" := (k */ (½)^p) (at level 35, no associativity).
Lemma Unth_half : forall n, (O<n)%nat -> [1/]1+(pred (n+n)) == ½ * [1/]1+pred n.
Lemma Unth_exp2 : forall p, ½^p == [1/]1+pred (exp2 p).
Hint Resolve Unth_exp2.
Lemma Nmult_exp2 : forall p, (exp2 p)/2^p == 1.
Hint Resolve Nmult_exp2.
Section Sequence.
Variable k : U.
Hypothesis kless1 : k < 1.
Lemma Ult_one_inv_zero : ~ 0 == [1-]k.
Hint Resolve Ult_one_inv_zero.
Lemma Umult_simpl_zero : forall x, x <= k * x -> x == 0.
Lemma Umult_simpl_one : forall x, k * x + [1-]k <= x -> x == 1.
Lemma bary_le_compat : forall k' x y, x <= y -> k <= k' -> k' * x + [1-]k' * y <= k * x + [1-]k * y.
Lemma bary_one_le_compat : forall k' x, k <= k' -> k' * x + [1-]k' <= k * x + [1-]k.
Lemma glb_exp_0 : glb (UExp k) == 0.
Instance Uinvexp_mon : monotonic (fun n => [1-]k ^ n).
Save.
Lemma lub_inv_exp_1 : mlub (fun n => [1-]k ^ n) == 1.
End Sequence.
Hint Resolve glb_exp_0 lub_inv_exp_1 bary_one_le_compat bary_le_compat.
Ltac Usimpl := match goal with
|- context [(Uplus 0 ?x)] => setoid_rewrite (Uplus_zero_left x)
| |- context [(Uplus ?x 0)] => setoid_rewrite (Uplus_zero_right x)
| |- context [(Uplus 1 ?x)] => setoid_rewrite (Uplus_one_left x)
| |- context [(Uplus ?x 1)] => setoid_rewrite (Uplus_one_right x)
| |- context [(Umult 0 ?x)] => setoid_rewrite (Umult_zero_left x)
| |- context [(Umult ?x 0)] => setoid_rewrite (Umult_zero_right x)
| |- context [(Umult 1 ?x)] => setoid_rewrite (Umult_one_left x)
| |- context [(Umult ?x 1)] => setoid_rewrite (Umult_one_right x)
| |- context [(Uesp 0 ?x)] => setoid_rewrite (Uesp_zero_left x)
| |- context [(Uesp ?x 0)] => setoid_rewrite (Uesp_zero_right x)
| |- context [(Uesp 1 ?x)] => setoid_rewrite (Uesp_one_left x)
| |- context [(Uesp ?x 1)] => setoid_rewrite (Uesp_one_right x)
| |- context [(Uminus 0 ?x)] => setoid_rewrite (Uminus_zero_left x)
| |- context [(Uminus ?x 0)] => setoid_rewrite (Uminus_zero_right x)
| |- context [(Uminus ?x 1)] => setoid_rewrite (Uminus_one_right x)
| |- context [(Uminus ?x ?x)] => setoid_rewrite (Uminus_eq x)
| |- context [½ + ½] => setoid_rewrite Unth_one_plus
| |- context [(½ * ?x + ½ * ?x)] => setoid_rewrite (Unth_one_refl x)
| |- context [[1-]½] => setoid_rewrite <- Unth_one
| |- context [([1-] ([1-] ?x))] => setoid_rewrite (Uinv_inv x)
| |- context [ ?x + ([1-] ?x)] => setoid_rewrite (Uinv_opp_right x)
| |- context [ ([1-]?x) + ?x ] => setoid_rewrite (Uinv_opp_left x)
| |- context [([1-] 1)] => setoid_rewrite Uinv_one
| |- context [([1-] 0)] => setoid_rewrite Uinv_zero
| |- context [([1/]1+O)] => setoid_rewrite Unth_zero
| |- context [(0/?x)] => setoid_rewrite (Udiv_zero x)
| |- context [(?x/1)] => setoid_rewrite (Udiv_one x)
| |- context [(?x/0)] => setoid_rewrite (Udiv_by_zero x); [idtac|reflexivity]
| |- context [?x^O] => setoid_rewrite (Uexp_0 x)
| |- context [?x^(S O)] => setoid_rewrite (Uexp_1 x)
| |- context [0^(?n)] => setoid_rewrite Uexp_zero; [idtac|omega]
| |- context [U1^(?n)] => setoid_rewrite Uexp_one
| |- context [(Nmult 0 ?x)] => setoid_rewrite Nmult_0
| |- context [(Nmult 1 ?x)] => setoid_rewrite Nmult_1
| |- context [(Nmult ?n 0)] => setoid_rewrite Nmult_zero
| |- context [(sigma ?f O)] => setoid_rewrite sigma_0
| |- context [(sigma ?f (S O))] => setoid_rewrite sigma_1
| |- (Ole (Uplus ?x ?y) (Uplus ?x ?z)) => apply Uplus_le_compat_right
| |- (Ole (Uplus ?x ?z) (Uplus ?y ?z)) => apply Uplus_le_compat_left
| |- (Ole (Uplus ?x ?z) (Uplus ?z ?y)) => setoid_rewrite (Uplus_sym z y);
apply Uplus_le_compat_left
| |- (Ole (Uplus ?x ?y) (Uplus ?z ?x)) => setoid_rewrite (Uplus_sym x y);
apply Uplus_le_compat_left
| |- (Ole (Uinv ?y) (Uinv ?x)) => apply Uinv_le_compat
| |- (Ole (Uminus ?x ?y) (Uminus ?x ?z)) => apply Uminus_le_compat_right
| |- (Ole (Uminus ?x ?z) (Uminus ?y ?z)) => apply Uminus_le_compat_left
| |- ((Uinv ?x) == (Uinv ?y)) => apply Uinv_eq_compat
| |- ((Uplus ?x ?y) == (Uplus ?x ?z)) => apply Uplus_eq_compat_right
| |- ((Uplus ?x ?z) == (Uplus ?y ?z)) => apply Uplus_eq_compat_left
| |- ((Uplus ?x ?z) == (Uplus ?z ?y)) => setoid_rewrite (Uplus_sym z y);
apply Uplus_eq_compat_left
| |- ((Uplus ?x ?y) == (Uplus ?z ?x)) => setoid_rewrite (Uplus_sym x y);
apply Uplus_eq_compat_left
| |- ((Uminus ?x ?y) == (Uplus ?x ?z)) => apply Uminus_eq_compat;[apply Oeq_refl|idtac]
| |- ((Uminus ?x ?z) == (Uplus ?y ?z)) => apply Uminus_eq_compat;[idtac|apply Oeq_refl]
| |- (Ole (Umult ?x ?y) (Umult ?x ?z)) => apply Umult_le_compat_right
| |- (Ole (Umult ?x ?z) (Umult ?y ?z)) => apply Umult_le_compat_left
| |- (Ole (Umult ?x ?z) (Umult ?z ?y)) => setoid_rewrite (Umult_sym z y);
apply Umult_le_compat_left
| |- (Ole (Umult ?x ?y) (Umult ?z ?x)) => setoid_rewrite (Umult_sym x y);
apply Umult_le_compat_left
| |- ((Umult ?x ?y) == (Umult ?x ?z)) => apply Umult_eq_compat_right
| |- ((Umult ?x ?z) == (Umult ?y ?z)) => apply Umult_eq_compat_left
| |- ((Umult ?x ?z) == (Umult ?z ?y)) => setoid_rewrite (Umult_sym z y);
apply Umult_eq_compat_left
| |- ((Umult ?x ?y) == (Umult ?z ?x)) => setoid_rewrite (Umult_sym x y);
apply Umult_eq_compat_left
end.
Ltac Ucompute1 :=
first [rewrite Uplus_zero_left |
rewrite Uplus_zero_right |
rewrite Uplus_one_left |
rewrite Uplus_one_right |
rewrite Umult_zero_left |
rewrite Umult_zero_right |
rewrite Umult_one_left |
rewrite Umult_one_right |
rewrite Uesp_zero_left |
rewrite Uesp_zero_right |
rewrite Uesp_one_left |
rewrite Uesp_one_right |
rewrite Uminus_zero_left |
rewrite Uminus_zero_right |
rewrite Uminus_one_right |
rewrite Uinv_inv |
rewrite Uinv_opp_right |
rewrite Uinv_opp_left |
rewrite Uinv_one |
rewrite Uinv_zero |
rewrite Unth_zero |
rewrite Uexp_0 |
rewrite Uexp_1 |
(rewrite Uexp_zero; [idtac|omega]) |
rewrite Uexp_one |
rewrite Nmult_0 |
rewrite Nmult_1 |
rewrite Nmult_zero |
rewrite sigma_0 |
rewrite sigma_1
].
Ltac Ucompute :=
first [setoid_rewrite Uplus_zero_left |
setoid_rewrite Uplus_zero_right |
setoid_rewrite Uplus_one_left |
setoid_rewrite Uplus_one_right |
setoid_rewrite Umult_zero_left |
setoid_rewrite Umult_zero_right |
setoid_rewrite Umult_one_left |
setoid_rewrite Umult_one_right |
setoid_rewrite Uesp_zero_left |
setoid_rewrite Uesp_zero_right |
setoid_rewrite Uesp_one_left |
setoid_rewrite Uesp_one_right |
setoid_rewrite Uminus_zero_left |
setoid_rewrite Uminus_zero_right |
setoid_rewrite Uminus_one_right |
setoid_rewrite Uinv_inv |
setoid_rewrite Uinv_opp_right |
setoid_rewrite Uinv_opp_left |
setoid_rewrite Uinv_one |
setoid_rewrite Uinv_zero |
setoid_rewrite Unth_zero |
setoid_rewrite Uexp_0 |
setoid_rewrite Uexp_1 |
(setoid_rewrite Uexp_zero; [idtac|omega]) |
setoid_rewrite Uexp_one |
setoid_rewrite Nmult_0 |
setoid_rewrite Nmult_1 |
setoid_rewrite Nmult_zero |
setoid_rewrite sigma_0 |
setoid_rewrite sigma_1
].
Properties of current values
Notation "[1/3]" := (Unth 2%nat).
Notation "¼" := (Unth 3%nat).
Notation "[1/8]" := (Unth 7).
Notation "¾" := (Uinv ¼).
Lemma half_square : ½*½==¼.
Lemma half_cube : ½*½*½==[1/8].
Lemma three_quarter_decomp : ¾==½+¼.
Hint Resolve half_square half_cube three_quarter_decomp.
Lemma half_dec_mult
: forall p, p <= ½ -> (½+p) * (½-p) == ¼ - (p * p).
Lemma half_Ult_Umult_Uinv :
forall p, p < ½ -> p * [1-]p < ¼.
Hint Resolve half_Ult_Umult_Uinv.
Lemma half_Ule_Umult_Uinv :
forall p, p <= ½ -> p * [1-]p <= ¼.
Hint Resolve half_Ule_Umult_Uinv.
Lemma Ult_Umult_Uinv :
forall p, ~ p == ½ -> p * [1-]p < ¼.
Lemma Ule_Umult_Uinv : forall p, p * [1-]p <= ¼.
Notation "¼" := (Unth 3%nat).
Notation "[1/8]" := (Unth 7).
Notation "¾" := (Uinv ¼).
Lemma half_square : ½*½==¼.
Lemma half_cube : ½*½*½==[1/8].
Lemma three_quarter_decomp : ¾==½+¼.
Hint Resolve half_square half_cube three_quarter_decomp.
Lemma half_dec_mult
: forall p, p <= ½ -> (½+p) * (½-p) == ¼ - (p * p).
Lemma half_Ult_Umult_Uinv :
forall p, p < ½ -> p * [1-]p < ¼.
Hint Resolve half_Ult_Umult_Uinv.
Lemma half_Ule_Umult_Uinv :
forall p, p <= ½ -> p * [1-]p <= ¼.
Hint Resolve half_Ule_Umult_Uinv.
Lemma Ult_Umult_Uinv :
forall p, ~ p == ½ -> p * [1-]p < ¼.
Lemma Ule_Umult_Uinv : forall p, p * [1-]p <= ¼.
Equality is not true, even for monotonic sequences fot instance n/m
Lemma Ulub_Uglb_exch_le : forall f : nat -> nat -> U,
Ulub (fun n => Uglb (fun m => f n m)) <= Uglb (fun m => Ulub (fun n => f n m)).
Definition fsup (f:nat -> U) (n:nat) := Ulub (fun k => f (n+k)%nat).
Definition finf (f:nat -> U) (n:nat) := Uglb (fun k => f (n+k)%nat).
Lemma fsup_incr : forall (f:nat -> U) n, fsup f (S n) <= fsup f n.
Hint Resolve fsup_incr.
Lemma finf_incr : forall (f:nat -> U) n, finf f n <= finf f (S n).
Hint Resolve finf_incr.
Instance fsup_mon : forall f, monotonic (o2:=Iord U) (fsup f).
Save.
Instance finf_mon : forall f, monotonic (finf f).
Save.
Definition Fsup (f:nat -> U) : nat -m-> U := mon (fsup f).
Definition Finf (f:nat -> U) : nat -m> U := mon (finf f).
Lemma fn_fsup : forall f n, f n <= fsup f n.
Hint Resolve fn_fsup.
Lemma finf_fn : forall f n, finf f n <= f n.
Hint Resolve finf_fn.
Definition limsup f := glb (Fsup f).
Definition liminf f := lub (Finf f).
Lemma le_liminf_sup : forall f, liminf f <= limsup f.
Hint Resolve le_liminf_sup.
Definition has_lim f := limsup f <= liminf f.
Lemma eq_liminf_sup : forall f, has_lim f-> liminf f == limsup f.
Definition cauchy f := forall (p:nat), exc (fun M:nat => forall n m,
(M <= n)%nat -> (M <= m)%nat -> f n <= f m + ½^p).
Definition is_limit f (l:U) := forall (p:nat), exc (fun M:nat => forall n,
(M <= n)%nat -> f n <= l + ½^p /\ l <= f n + ½^p).
Lemma cauchy_lim : forall f, cauchy f -> is_limit f (limsup f).
Lemma has_limit_cauchy : forall f l, is_limit f l -> cauchy f.
Lemma limit_le_unique : forall f l1 l2, is_limit f l1 -> is_limit f l2 -> l1 <= l2.
Lemma limit_unique : forall f l1 l2, is_limit f l1 -> is_limit f l2 -> l1 == l2.
Hint Resolve limit_unique.
Lemma has_limit_compute : forall f l, is_limit f l -> is_limit f (limsup f).
Lemma limsup_eq_mult : forall k (f : nat -> U),
limsup (fun n => k * f n) == k * limsup f.
Lemma liminf_eq_mult : forall k (f : nat -> U),
liminf (fun n => k * f n) == k * liminf f.
Lemma limsup_eq_plus_cte_right : forall k (f : nat -> U),
limsup (fun n => (f n) + k) == limsup f + k.
Lemma liminf_eq_plus_cte_right : forall k (f : nat -> U),
liminf (fun n => (f n) + k) == liminf f + k.
Lemma limsup_le_plus : forall (f g: nat -> U),
limsup (fun x => f x + g x) <= limsup f + limsup g.
Lemma liminf_le_plus : forall (f g: nat -> U),
liminf f + liminf g <= liminf (fun x => f x + g x).
Hint Resolve liminf_le_plus limsup_le_plus.
Lemma limsup_le_compat : forall f g : nat -> U, f <= g -> limsup f <= limsup g.
Lemma liminf_le_compat : forall f g : nat -> U, f <= g -> liminf f <= liminf g.
Hint Resolve limsup_le_compat liminf_le_compat.
Lemma limsup_eq_compat : forall f g : nat -> U, f == g -> limsup f == limsup g.
Lemma liminf_eq_compat : forall f g : nat -> U, f == g -> liminf f == liminf g.
Hint Resolve liminf_eq_compat limsup_eq_compat.
Lemma limsup_inv : forall f : nat -> U, limsup (fun x => [1-]f x) == [1-] liminf f.
Lemma liminf_inv : forall f : nat -> U, liminf (fun x => [1-]f x) == [1-] limsup f.
Hint Resolve limsup_inv liminf_inv.
Lemma liminf_incr : forall f:nat -m> U, liminf f == lub f.
Lemma limsup_incr : forall f:nat -m> U, limsup f == lub f.
Lemma has_limit_incr : forall f:nat -m> U, has_lim f.
Lemma liminf_decr : forall f:nat -m-> U, liminf f == glb f.
Lemma limsup_decr : forall f:nat -m-> U, limsup f == glb f.
Lemma has_limit_decr : forall f:nat -m-> U, has_lim f.
Lemma has_limit_sum : forall f g: nat -> U, has_lim f -> has_lim g -> has_lim (fun x => f x + g x).
Lemma has_limit_inv : forall f : nat -> U, has_lim f -> has_lim (fun x => [1-]f x).
Lemma has_limit_cte : forall c, has_lim (fun n => c).
Lemma limsup_incr : forall f:nat -m> U, limsup f == lub f.
Lemma has_limit_incr : forall f:nat -m> U, has_lim f.
Lemma liminf_decr : forall f:nat -m-> U, liminf f == glb f.
Lemma limsup_decr : forall f:nat -m-> U, limsup f == glb f.
Lemma has_limit_decr : forall f:nat -m-> U, has_lim f.
Lemma has_limit_sum : forall f g: nat -> U, has_lim f -> has_lim g -> has_lim (fun x => f x + g x).
Lemma has_limit_inv : forall f : nat -> U, has_lim f -> has_lim (fun x => [1-]f x).
Lemma has_limit_cte : forall c, has_lim (fun n => c).
Definition serie (f : nat -> U) : U := lub (sigma f).
Lemma serie_le_compat : forall (f g: nat -> U),
(forall k, f k <= g k) -> serie f <= serie g.
Lemma serie_eq_compat : forall (f g: nat -> U),
(forall k, f k == g k) -> serie f == serie g.
Lemma serie_sigma_lift : forall (f :nat -> U) (n:nat),
serie f == sigma f n + serie (fun k => f (n + k)%nat).
Lemma serie_sigma_decomp : forall (f g:nat -> U) (n:nat),
(forall k, g k = f (n + k)%nat) ->
serie f == sigma f n + serie g.
Lemma serie_lift_le : forall (f :nat -> U) (n:nat),
serie (fun k => f (n + k)%nat) <= serie f.
Hint Resolve serie_lift_le.
Lemma serie_decomp_le : forall (f g:nat -> U) (n:nat),
(forall k, g k <= f (n + k)%nat) ->
serie g <= serie f.
Lemma serie_S_lift : forall (f :nat -> U),
serie f == f O + serie (fun k => f (S k)).
Lemma serie_zero : forall f, (forall k, f k ==0) -> serie f ==0.
Lemma serie_not_zero : forall f k, 0 < f k -> 0 < serie f.
Lemma serie_zero_elim : forall f, serie f == 0 -> forall k, f k ==0.
Hint Resolve serie_eq_compat serie_le_compat serie_zero.
Lemma serie_le : forall f k, f k <= serie f.
Lemma serie_minus_incr : forall f :nat -m> U, serie (fun k => f (S k) - f k) == lub f - f O.
Lemma serie_minus_decr : forall f : nat -m-> U,
serie (fun k => f k - f (S k)) == f O - glb f.
Lemma serie_plus : forall (f g : nat -> U),
serie (fun k => (f k) + (g k)) == serie f + serie g.
series and lub
Lemma serie_glb_pos : forall f : nat -> U, 0 < Uglb f -> serie f == 1.
Lemma serie_glb_0 : forall f : nat -> U, serie f < 1 -> Uglb f == 0.
Hint Immediate serie_glb_0.
Definition wretract (f : nat -> U) := forall k, f k <= [1-] (sigma f k).
Lemma retract_wretract : forall f, (forall n, retract f n) -> wretract f.
Lemma wretract_retract : forall f, wretract f -> forall n, retract f n.
Hint Resolve wretract_retract.
Lemma wretract_lt : forall (f : nat -> U), (forall (n : nat), sigma f n < 1) -> wretract f.
Hint Immediate wretract_lt.
Lemma wretract_lt_serie : forall (f : nat -> U), serie f < 1 -> wretract f.
Hint Immediate wretract_lt_serie.
Lemma retract_zero_wretract :
forall f n, retract f n -> (forall k, (n <= k)%nat -> f k == 0) -> wretract f.
Lemma wretract_le : forall f g : nat -> U, f <= g -> wretract g -> wretract f.
Lemma wretract_lift : forall f n, wretract f ->
sigma f n <= [1-] serie (fun k => f (n + k)%nat).
Hint Resolve wretract_lift.
Lemma serie_mult :
forall (f : nat -> U) c, wretract f -> serie (fun k => c * f k) == c * serie f.
Hint Resolve serie_mult.
Lemma serie_prod_maj : forall (f g : nat -> U),
serie (fun k => f k * g k) <= serie f.
Hint Resolve serie_prod_maj.
Lemma serie_prod_le : forall (f g : nat -> U) (c:U), (forall k, f k <= c)
-> wretract g -> serie (fun k => f k * g k) <= c * serie g.
Lemma serie_prod_ge : forall (f g : nat -> U) (c:U), (forall k, c <= (f k))
-> wretract g -> c * serie g <= serie (fun k => f k * g k).
Hint Resolve serie_prod_le serie_prod_ge.
Lemma serie_inv_le : forall (f g : nat -> U), wretract f ->
serie (fun k => f k * [1-] (g k)) <= [1-] (serie (fun k => f k * g k)).
Lemma serie_half : forall f, serie f < 1
-> exc (fun n => serie (fun k => f (n + k)%nat) <= ½ * serie f).
Lemma serie_half_exp : forall f m, serie f < 1
-> exc (fun n => serie (fun k => f (n + k)%nat) <= ½^m).
Definition Serie : (nat -> U) -m> U.
Defined.
Lemma Serie_simpl : forall f, Serie f = serie f.
Lemma serie_continuous : continuous Serie.
Definition fun_cte n (a:U) : nat -> U
:= fun p => if eq_nat_dec p n then a else 0.
Lemma fun_cte_eq : forall n a, fun_cte n a n = a.
Lemma fun_cte_zero : forall n a p, p <> n -> fun_cte n a p = 0.
Lemma sigma_cte_eq : forall n a p, (n < p)%nat -> sigma (fun_cte n a) p == a.
Hint Resolve sigma_cte_eq.
Lemma serie_cte_eq : forall n a, serie (fun_cte n a) == a.
Section PartialPermutationSerieLe.
Variables f g : nat -> U.
Variable s : nat -> nat -> Prop.
Hypothesis s_dec : forall i j, {s i j}+{~s i j}.
Hypothesis s_inj : forall i j k : nat, s i k -> s j k -> i = j.
Hypothesis s_dom : forall i, ~ f i == 0 -> exists j, s i j.
Hypothesis f_g_perm : forall i j, s i j -> f i == g j.
Lemma serie_perm_rel_le : serie f <= serie g.
End PartialPermutationSerieLe.
Section PartialPermutationSerieEq.
Variables f g : nat -> U.
Variable s : nat -> nat -> Prop.
Hypothesis s_dec : forall i j, {s i j}+{~s i j}.
Hypothesis s_fun : forall i j k : nat, s i j -> s i k -> j = k.
Hypothesis s_inj : forall i j k : nat, s i k -> s j k -> i = j.
Hypothesis s_surj : forall j, ~ g j == 0 -> exists i, s i j.
Hypothesis s_dom : forall i, ~ f i == 0 -> exists j, s i j.
Hypothesis f_g_perm : forall i j, s i j -> f i == g j.
Lemma serie_perm_rel_eq : serie f == serie g.
End PartialPermutationSerieEq.
Section PermutationSerie.
Variable s : nat -> nat.
Hypothesis s_inj : forall i j : nat, s i = s j -> i = j.
Hypothesis s_surj : forall j, exists i, s i = j.
Variable f : nat -> U.
Lemma serie_perm_le : serie (fun i => f (s i)) <= serie f.
Lemma serie_perm_eq : serie f == serie (fun i => f (s i)).
End PermutationSerie.
Hint Resolve serie_perm_eq serie_perm_le.
Section SerieProdRel.
Variable f : nat -> U.
Variable g : nat -> nat -> U.
Variable s : nat -> nat -> nat -> Prop.
Hypothesis s_dec : forall k n m, {s k n m}+{~ s k n m}.
Hypothesis s_fun1 : forall k n1 m1 n2 m2, s k n1 m1 -> s k n2 m2 -> n1 = n2.
Hypothesis s_fun2 : forall k n1 m1 n2 m2, s k n1 m1 -> s k n2 m2 -> m1 = m2.
Hypothesis s_inj : forall k1 k2 n m, s k1 n m -> s k2 n m -> k1 = k2.
Hypothesis s_surj : forall n m, ~ g n m == 0 -> exists k, s k n m.
Hypothesis f_g_perm : forall k n m, s k n m -> f k == g n m.
Section SPR.
Hypothesis s_dom : forall k, ~ f k == 0 -> exists n, exists m, s k n m.
Lemma serie_le_rel_prod : serie f <= serie (fun n => serie (g n)).
End SPR.
Variable s_fst : nat -> nat.
Hypothesis s_fst_ex : forall k, exists m, s k (s_fst k) m.
Lemma s_dom : forall k, exists n, exists m, s k n m.
Hint Resolve s_dom.
Lemma serie_rel_prod_le : serie (fun n => serie (g n)) <= serie f.
Lemma serie_rel_prod_eq : serie f == serie (fun n => serie (g n)).
End SerieProdRel.
Section SerieProd.
Variable f : (nat * nat) -> U.
Variable s : nat -> nat * nat.
Variable s_inj : forall n m, s n = s m -> n = m.
Variable s_surj : forall m, exists n, s n = m.
Lemma serie_enum_prod_eq : serie (fun k => f (s k)) == serie (fun n => serie (fun m => f (n,m))).
End SerieProd.
Hint Resolve serie_enum_prod_eq.